EROS ( Extremely Reliable Operating System ) es un sistema operativo desarrollado a partir de 1991 por EROS Group, LLC., La Universidad Johns Hopkins y la Universidad de Pensilvania . Las características incluyen datos automáticos y persistencia de procesos , algo de soporte preliminar en tiempo real y seguridad basada en capacidades . EROS es puramente un sistema operativo de investigación y nunca se implementó en el mundo real. A partir de 2005 [actualizar], el desarrollo se ha detenido a favor de dos sistemas sucesores, CapROS y Coyotos .
Conceptos clave
El objetivo primordial del sistema EROS (y sus parientes) es proporcionar un fuerte apoyo a nivel del sistema operativo para la reestructuración eficiente de aplicaciones críticas en pequeños componentes de comunicación. Cada componente puede comunicarse con los demás solo a través de interfaces protegidas y está aislado del resto del sistema. Una "interfaz protegida", en este contexto, es aquella que es impuesta por la parte de nivel más bajo del sistema operativo (el kernel ). El kernel es la única parte del sistema que puede mover información de un proceso a otro. También tiene un control completo de la máquina y (si se construye correctamente) no se puede pasar por alto. En EROS, el mecanismo proporcionado por el kernel mediante el cual un componente nombra e invoca los servicios de otro son las capacidades que utilizan la comunicación entre procesos (IPC). Al hacer cumplir las interfaces protegidas por capacidad, el kernel asegura que todas las comunicaciones a un proceso lleguen a través de una interfaz exportada intencionalmente. También asegura que no sea posible una invocación a menos que el componente invocador tenga una capacidad válida para el invocador. La protección en los sistemas de capacidad se logra restringiendo la propagación de capacidades de un componente a otro, a menudo a través de una política de seguridad conocida como confinamiento .
Los sistemas de capacidad promueven naturalmente la estructura de software basada en componentes. Este enfoque organizacional es similar al concepto de lenguaje de programación de la programación orientada a objetos , pero ocurre con mayor granularidad y no incluye el concepto de herencia . Cuando el software se reestructura de esta manera, surgen varios beneficios:
- Los componentes individuales se estructuran de forma más natural como bucles de eventos . Ejemplos de sistemas que se estructuran comúnmente de esta manera incluyen sistemas de control de vuelo (ver también Consideraciones de software DO-178B en Certificación de equipos y sistemas de a bordo ) y sistemas de conmutación telefónica (ver conmutador 5ESS ). La programación impulsada por eventos se elige para estos sistemas principalmente por su simplicidad y robustez, que son atributos esenciales en los sistemas críticos para la vida y la misión.
- Los componentes se vuelven más pequeños y se pueden probar individualmente, lo que ayuda al implementador a identificar más fácilmente fallas y errores.
- El aislamiento de cada componente de los demás limita el alcance del daño que puede ocurrir cuando algo sale mal o el software se comporta mal.
En conjunto, estos beneficios conducen a sistemas considerablemente más robustos y seguros. El Plessey System 250 fue un sistema diseñado originalmente para su uso en conmutadores de telefonía, cuyo diseño basado en la capacidad se eligió específicamente por razones de robustez.
A diferencia de muchos sistemas anteriores, las capacidades son el único mecanismo para nombrar y usar recursos en EROS, lo que lo convierte en lo que a veces se denomina un sistema de capacidad pura . Por el contrario, IBM i es un ejemplo de un sistema de capacidad comercialmente exitoso, pero no es un sistema de capacidad pura.
Las arquitecturas de capacidad pura están respaldadas por modelos de seguridad matemáticos maduros y bien probados. Estos se han utilizado para demostrar formalmente que los sistemas basados en capacidades se pueden hacer seguros si se implementan correctamente. Se ha demostrado que la denominada "propiedad de seguridad" es decidible para sistemas de capacidad pura (ver Lipton ). El confinamiento, que es el bloque de construcción fundamental del aislamiento, ha sido verificado formalmente para ser ejecutado por sistemas de capacidad pura, [1] y se reduce a una implementación práctica por parte del "constructor" de EROS y la "fábrica" de KeyKOS. No existe una verificación comparable para ningún otro mecanismo de protección primitivo. Hay un resultado fundamental en la literatura que muestra que la "seguridad" es matemáticamente indecidible en el caso general (ver HRU , pero tenga en cuenta que, por supuesto, es demostrable para un conjunto ilimitado de casos restringidos [2] ). De mayor importancia práctica, se ha demostrado que la seguridad es falsa para todos los mecanismos de protección primitivos que se envían en los sistemas operativos de productos básicos actuales. La seguridad es una condición previa necesaria para la aplicación exitosa de cualquier política de seguridad. En términos prácticos, este resultado significa que, en principio, no es posible asegurar los sistemas de productos básicos actuales, pero es potencialmente posible asegurar los sistemas basados en la capacidad, siempre que se implementen con suficiente cuidado. Ni EROS ni KeyKOS han sido penetrados con éxito, y sus mecanismos de aislamiento nunca han sido derrotados con éxito por ningún atacante interno, pero no se sabe si las dos implementaciones fueron lo suficientemente cuidadosas. Uno de los objetivos del proyecto Coyotos es demostrar que el aislamiento y la seguridad de los componentes se ha logrado definitivamente mediante la aplicación de técnicas de verificación de software.
El sistema L4.sec, que es un sucesor de la familia de microkernel L4 , es un sistema basado en capacidades y ha sido significativamente influenciado por los resultados del proyecto EROS. La influencia es mutua, ya que el trabajo de EROS en la invocación de alto rendimiento fue fuertemente motivado por los éxitos de Jochen Liedtke con la familia de microkernel L4 .
Historia
El desarrollador principal de EROS fue Jonathan S. Shapiro. También es la fuerza impulsora detrás de Coyotos , que es un "paso evolutivo" [3] más allá del sistema operativo EROS.
El proyecto EROS comenzó en 1991 como una reconstrucción en sala limpia de un sistema anterior, KeyKOS . KeyKOS fue un sistema operativo desarrollado por Key Logic, Inc., y fue una continuación directa del trabajo en el anterior sistema GNOSIS (Gran Nuevo Sistema Operativo In the Sky) creado por Tymshare, Inc. Las circunstancias que rodearon la desaparición de Key Logic en 1991 hicieron que las licencias KeyKOS poco práctico. Dado que KeyKOS no se ejecutó en procesadores de productos básicos populares en ningún caso, se tomó la decisión de reconstruirlo a partir de la documentación disponible públicamente.
A fines de 1992, quedó claro que la arquitectura del procesador había cambiado significativamente desde la introducción de la idea de capacidad, y ya no era obvio que los sistemas estructurados por componentes fueran prácticos. Los sistemas basados en microkernel , que de manera similar favorecen un gran número de procesos e IPC, se enfrentaban a graves desafíos de rendimiento, y no estaba claro si estos podrían resolverse con éxito. La arquitectura x86 estaba emergiendo claramente como la arquitectura dominante, pero la costosa latencia de transición de usuario / supervisor en el 386 y el 486 presentaba serios desafíos para el aislamiento basado en procesos. El proyecto EROS se estaba convirtiendo en un esfuerzo de investigación y se trasladó a la Universidad de Pensilvania para convertirse en el foco de la investigación de tesis de Shapiro. En 1999, se había demostrado una implementación de alto rendimiento para el procesador Pentium que competía directamente en rendimiento con la familia de microkernel L4 , que es conocida por su velocidad excepcional en IPC. El mecanismo de confinamiento EROS había sido verificado formalmente, en el proceso creando un modelo formal general para sistemas de capacidad seguros.
En 2000, Shapiro se unió a la facultad de Ciencias de la Computación de la Universidad Johns Hopkins. En Hopkins, el objetivo era mostrar cómo utilizar las instalaciones proporcionadas por el kernel de EROS para construir servidores seguros y defendibles a nivel de aplicación. Financiado por la Agencia de Proyectos de Investigación Avanzada de Defensa y el Laboratorio de Investigación de la Fuerza Aérea , EROS se utilizó como base para un sistema de ventanas confiable, [4] una pila de red defendible de alto rendimiento, [5] y los inicios de un navegador web seguro . También se utilizó para explorar la eficacia de la comprobación estática ligera. [6] En 2003, se descubrieron algunos problemas de seguridad muy desafiantes [7] que son intrínsecos a cualquier arquitectura de sistema basada en primitivas IPC síncronas (especialmente EROS y L4). El trabajo en EROS se detuvo a favor de Coyotos, que resuelve estos problemas.
A partir de 2006[actualizar], EROS y sus sucesores son los únicos sistemas de capacidad ampliamente disponibles que se ejecutan en hardware básico.
Estado
El trabajo en EROS por parte del grupo original se ha detenido, pero hay dos sistemas sucesores. El sistema CapROS se está construyendo directamente a partir del código base de EROS, mientras que el sistema Coyotos es un sistema sucesor que aborda algunas de las deficiencias arquitectónicas de EROS y está explorando la posibilidad de un sistema operativo completamente verificado. Se espera que tanto CapROS como Coyotos se lancen en varias implementaciones comerciales.
Ver también
Referencias
- ^ Jonathan S. Shapiro; Samuel Weber (29 de octubre de 1999). "Verificación del mecanismo de confinamiento EROS" . Archivado desde el original el 3 de marzo de 2016.
- ^ Peter Lee. "Código de prueba" . Archivado desde el original el 22 de septiembre de 2006.
- ^ Jonathan Shapiro (2 de abril de 2006). "Diferencias entre Coyotos y EROS - Un resumen rápido" . Archivado desde el original el 31 de julio de 2012.
- ^ Jonathan S. Shapiro; John Vanderburgh; Eric Northup; David Chizmadia. "Diseño del EROS Trusted Window System" . Archivado desde el original el 3 de marzo de 2016.
- ^ Anshumal Sinha; Sandeep Sarat; Jonathan S. Shapiro. "Subsistemas de red recargados: un subsistema de red defendible de alto rendimiento" . Archivado desde el original el 3 de marzo de 2016.
- ^ Hao Chen; Jonathan S. Shapiro. "Uso de la comprobación estática integrada en la construcción para preservar las invariantes de corrección" (PDF) . Archivado desde el original (PDF) el 3 de marzo de 2016.
- ^ Jonathan S. Shapiro. "Vulnerabilidades en diseños de IPC síncronos" . Archivado desde el original el 3 de marzo de 2016.
Revistas
- RJ Lipton y L. Snyder. "Un algoritmo de tiempo lineal para decidir la seguridad del sujeto". Journal of the ACM , 24 (3): 455-464, 1977.
- Michael A. Harrison , WL Ruzzo y Jeffrey D. Ullman . "Protección en sistemas operativos". Comunicaciones de ACM . 19 (8): 461-471, agosto de 1976.
enlaces externos
- Página de inicio de Coyotos en Wayback Machine (archivada el 2 de septiembre de 2016)
- Página de inicio de EROS en Wayback Machine (archivada el 4 de marzo de 2016)
- Página de inicio de KeyKOS en Wayback Machine (archivada el 4 de enero de 2016)
- Página de inicio de Jonathan Shapiro
- CapROS