Un núcleo de separación es un tipo de núcleo de seguridad que se utiliza para simular un entorno distribuido. El concepto fue introducido por John Rushby en un artículo de 1981. [1] Rushby propuso el núcleo de separación como una solución a las dificultades y problemas que habían surgido en el desarrollo y verificación de núcleos de seguridad grandes y complejos que estaban destinados a "proporcionar un funcionamiento seguro de múltiples niveles en sistemas multiusuario de propósito general". Según Rushby, "la tarea de un núcleo de separación es crear un entorno que sea indistinguible del proporcionado por un sistema distribuido físicamente: debe aparecer como si cada régimen fuera una máquina separada y aislada y que la información solo puede fluir de una máquina a otra a lo largo de líneas de comunicación externas conocidas. Una de las propiedades que debemos probar de un núcleo de separación, por lo tanto, es que no existen canales para el flujo de información entre regímenes distintos de los proporcionados explícitamente".
Una variante del núcleo de separación, el núcleo de partición, ha ganado aceptación en la comunidad de la aviación comercial como una forma de consolidar múltiples funciones en un solo procesador, tal vez de criticidad mixta . Los fabricantes de aeronaves han utilizado productos de sistemas operativos comerciales en tiempo real de este género para aplicaciones de aviónica críticas para la seguridad.
En 2007, la Dirección de Seguridad de la Información de la Agencia de Seguridad Nacional de los Estados Unidos (NSA) publicó el Perfil de Protección del Núcleo de Separación (SKPP, por sus siglas en inglés), [2] una especificación de requisitos de seguridad para núcleos de separación adecuados para su uso en los entornos de amenazas más hostiles. El SKPP describe, en el lenguaje de Common Criteria [3] , una clase de productos modernos que proporcionan las propiedades fundamentales del núcleo de separación conceptual de Rushby. Define los requisitos funcionales y de seguridad para la construcción y evaluación de núcleos de separación, al tiempo que proporciona cierta libertad en las opciones disponibles para los desarrolladores.
El SKPP define el núcleo de separación como "mecanismos de hardware y/o firmware y/o software cuya función principal es establecer, aislar y separar múltiples particiones y controlar el flujo de información entre los sujetos y los recursos exportados asignados a esas particiones". Además, los requisitos funcionales básicos del núcleo de separación incluyen:
El núcleo de separación asigna todos los recursos exportados bajo su control en particiones. Las particiones están aisladas excepto por los flujos de información permitidos explícitamente. Las acciones de un sujeto en una partición están aisladas de (es decir, no pueden ser detectadas por o comunicadas a) sujetos en otra partición, a menos que se haya permitido ese flujo. Las particiones y los flujos se definen en los datos de configuración. Tenga en cuenta que "partición" y "sujeto" son abstracciones ortogonales. "Partición", como lo indica su génesis matemática, proporciona una agrupación de entidades del sistema en teoría de conjuntos, mientras que "sujeto" nos permite razonar sobre las entidades activas individuales de un sistema. Por lo tanto, una partición (una colección, que contiene cero o más elementos) no es un sujeto (un elemento activo), pero puede contener cero o más sujetos. [2] El núcleo de separación proporciona a sus programas de software alojados propiedades de control de flujo de información y particionamiento de alta seguridad que son a prueba de manipulaciones e ineludibles. Estas capacidades proporcionan una base confiable y configurable para una variedad de arquitecturas de sistemas. [2]
En 2011, la Dirección de Seguridad de la Información puso fin al SKPP. La NSA ya no certificará sistemas operativos específicos, incluidos los núcleos de separación, en relación con el SKPP, señalando que "la conformidad con este perfil de protección, por sí sola, no ofrece suficiente confianza en que la información de seguridad nacional esté protegida adecuadamente en el contexto de un sistema más amplio en el que se integra el producto conforme". [5]
El microkernel seL4 tiene una prueba formal de concepto de que puede configurarse como un kernel de separación. [6] La continuidad forzada de la información [7] junto con esto implica que es un ejemplo de nivel elevado de seguridad. El kernel de separación Muen [8] también es un kernel de separación de código abierto verificado formalmente para máquinas x86.