Se publicó un artículo científico en Communications of the ACM , octubre de 2018, Volumen 61, Número 10, pp. 68-77, doi: 10.1145 / 3230627

En febrero de 2017, un helicóptero despegó de la pista de aterrizaje del Boeing en Arizona con la misión habitual: volar alrededor de las colinas más cercanas. Voló de manera completamente autónoma. De acuerdo con los requisitos de seguridad de la Administración Federal de Aviación de EE. UU., El piloto no tocó los controles. Este no fue el primer vuelo autónomo AH-6, que la compañía llama El pequeño pájaro no tripulado (ULB). Él ha estado volando así durante muchos años. Sin embargo, esta vez en medio del vuelo, el helicóptero sufrió un ataque cibernético. La computadora de a bordo atacó el software malicioso de la videocámara, así como el virus entregado a través de la unidad flash infectada, que se insertó durante el mantenimiento. El ataque amenazó algunos subsistemas, pero no pudo afectar la operación segura de la aeronave.

Ideas clave

• La evidencia formal de la arquitectura de software de un microkernel verificado se puede escalar de manera económica a sistemas reales.
• Son posibles y deseables diferentes niveles de seguridad y confiabilidad dentro del mismo sistema. No es necesario garantizar la máxima fiabilidad de todo el código.
• Un rediseño y refactorización moderados es suficiente para elevar los sistemas existentes al nivel de código altamente confiable.

Se podría pensar que la aviación militar puede repeler fácilmente un ataque cibernético de este tipo. En realidad, el equipo de pentesters profesionales encargados por la agencia DARPA, como parte del programa de Sistemas de Seguridad Cibernética Militar (HACMS) para desarrollar sistemas informáticos militares altamente confiables, hackeó con éxito la primera versión del software ULB en 2013, que fue desarrollado originalmente para garantizar la seguridad del vuelo en lugar de la protección de los ciberataques. Los hackers tuvieron la oportunidad de estrellar un helicóptero o aterrizarlo en cualquier lugar que lo deseen. Por lo tanto, el riesgo de tales ataques con un pasajero a bordo difícilmente se puede sobreestimar, y un intento de piratería fallido en febrero de 2017 indica algunos cambios fundamentales en el software.

Este artículo explica estos cambios y la tecnología que los hizo posibles. Esta es una tecnología desarrollada como parte del programa HACMS destinado a garantizar el funcionamiento seguro de los sistemas críticos en un entorno cibernético hostil, en este caso, varios vehículos autónomos. La tecnología se basa en la verificación formal de software: son programas con pruebas matemáticas verificadas automáticamente que funcionan de acuerdo con sus especificaciones. Aunque el artículo no está dedicado a los métodos formales en sí, explica cómo usar la verificación de artefactos para proteger los sistemas reales en la práctica.

Quizás el resultado más impresionante de HACMS es que la tecnología se puede extender a los sistemas reales existentes, mejorando en gran medida su protección contra los ataques cibernéticos. Este proceso se llama "modernización de la seguridad sísmica", similar a las actualizaciones de edificios sísmicos. Además, la mayor parte de la reingeniería fue realizada por ingenieros de Boeing, en lugar de especialistas en verificación formal.


"Pájaro" durante un vuelo de prueba no tripulado

No todo el software del helicóptero se basa en modelos matemáticos y evidencia. El campo de la verificación formal aún no está listo para tal escala. Sin embargo, el programa HACMS ha demostrado que la aplicación estratégica de métodos formales a las partes más importantes del sistema general mejora enormemente la protección. El enfoque HACMS funciona para sistemas en los que la característica de seguridad deseada se puede lograr simplemente aplicando a nivel de arquitectura. Se basa en nuestro microkernel verificado sel4, del que hablaremos a continuación. Garantiza el aislamiento entre subsistemas, con la excepción de canales de comunicación claramente definidos que están sujetos a las políticas de seguridad del sistema. Este aislamiento está garantizado a nivel de arquitectura con el marco verificado de CAmkES para los componentes del sistema. Uso de lenguajes específicos de dominio de Galois Inc. CAmkES se integra con herramientas de análisis de arquitectura de Rockwell Collins y la Universidad de Minnesota, así como con componentes de software altamente confiables.

Los logros de HACMS se basan en el viejo amigo fiel de un ingeniero de software: la modularización. La innovación es que los métodos formales prueban la observabilidad de las interfaces y la encapsulación de los componentes internos del módulo. Esta adhesión garantizada a la modularidad permite a los ingenieros que no son expertos en métodos formales (como en Boeing) crear sistemas nuevos o incluso modernizar los existentes y lograr una alta estabilidad. Aunque las herramientas aún no proporcionan evidencia completa de la seguridad del sistema.

Verificación formal

La evidencia de la corrección matemática de los programas se remonta al menos a la década de 1960 , pero durante mucho tiempo sus beneficios reales para el desarrollo de software fueron limitados en alcance y profundidad. Sin embargo, en los últimos años ha habido una serie de avances impresionantes en la verificación formal a nivel de código de sistemas reales, desde el compilador C CompCert verificado hasta el microkernel seL4 verificado (vea los artículos científicos al respecto), el sistema de conferencia verificado CoCon , el compilador CakeML ML verificado, programas verificados para probar los teoremas de Milawa y Candle , el sistema de archivos FSCQ a prueba de fallos verificado, el sistema distribuido IronFleet verificado y el marco de kernel paralelo CertiKOS verificado, así como importantes teoremas matemáticos, incluidos los problemas de cuatro colores , la prueba automática de la hipótesis de Kepler y el teorema de Fe - Thompson en orden impar . Todos estos son sistemas reales. Por ejemplo, CompCert es un producto comercial, el microkernel seL4 se utiliza en aeronaves aeroespaciales y no tripuladas, como la plataforma de Internet de las cosas, y el sistema CoCon se ha utilizado en numerosas conferencias científicas grandes.

Estos proyectos de verificación requieren un esfuerzo considerable. Para que los métodos formales estén disponibles al público, estos esfuerzos deben reducirse. Aquí demostramos cómo una combinación estratégica de métodos formales e informales, la automatización parcial de métodos formales y un cuidadoso desarrollo de software para maximizar los beneficios de los componentes aislados nos han permitido aumentar significativamente la confiabilidad de los sistemas cuyo tamaño y complejidad general son órdenes de magnitud mayores que los mencionados anteriormente.

Tenga en cuenta que aplicamos la verificación formal principalmente para el código del que depende la seguridad del sistema. Pero hay otros beneficios. Por ejemplo, la evidencia de que el código es correcto hace suposiciones sobre el contexto en el que se ejecuta (por ejemplo, el comportamiento del hardware y la configuración del software). La verificación formal hace explícitos estos supuestos, lo que ayuda a los desarrolladores a centrarse en otras herramientas de verificación, como las pruebas. Además, en muchos casos, el sistema incluye código tanto verificado como no verificado. Durante las revisiones de código, las pruebas y la depuración, la verificación formal actúa como una lente, centrándose en el código del sistema crítico y no verificado.

seL4

Comencemos con la base para construir sistemas demostrablemente confiables: el núcleo del sistema operativo (SO). Esta es la parte más importante que garantiza la confiabilidad de todo el sistema de manera rentable.

El microkernel seL4 proporciona un conjunto mínimo de mecanismos formalmente verificados para implementar sistemas seguros. A diferencia de los núcleos estándar , es a propósito universal y, por lo tanto, adecuado para implementar una serie de políticas de seguridad y requisitos del sistema.

Uno de los objetivos principales del desarrollo de seL4 es proporcionar un fuerte aislamiento entre los componentes que desconfían mutuamente y que se ejecutan en la parte superior del núcleo. Admite su trabajo como hipervisor, por ejemplo, para sistemas operativos Linux completos, mientras los mantiene aislados de los componentes críticos para la seguridad que pueden funcionar juntos, como se muestra en la Figura 1. En particular, esta función permite a los desarrolladores de sistemas usar componentes heredados con componentes ocultos vulnerabilidades junto a componentes altamente confiables.


Fig. 1. Aislamiento y comunicaciones controladas en seL4

El núcleo seL4 ocupa una posición especial entre los micronúcleos de uso general. No solo proporciona un mejor rendimiento en su clase , sus 10,000 líneas de código C han sido sometidas a una verificación formal más rigurosa que cualquier otro software disponible públicamente en la historia humana en términos no solo de líneas de prueba, sino también de la solidez de las propiedades comprobadas. Se basa en la prueba de la "corrección funcional" de la implementación central en C. Asegura que cualquier comportamiento del núcleo se prediga por su especificación abstracta formal: consulte la aplicación en línea para obtener una idea de cómo se ve esta evidencia. Después de esta garantía, hemos agregado evidencia adicional que explicaremos después de la introducción a los mecanismos básicos del núcleo.

seL4 API

El núcleo seL4 proporciona un conjunto mínimo de mecanismos para implementar sistemas seguros: transmisiones, gestión de capacidades, espacios de direcciones virtuales, comunicación entre procesos (IPC), señalización y entrega de interrupciones.

El núcleo retiene su estado en los "objetos del núcleo". Por ejemplo, para cada subproceso en el sistema, hay un "objeto de flujo" que almacena información sobre el desprendimiento, la ejecución y el control de acceso. Los programas de espacio de usuario pueden referirse a los objetos del núcleo solo indirectamente a través de las llamadas "capacidades" o "capacidades", que combinan un enlace a un objeto con un conjunto de derechos de acceso a él. Por ejemplo, un hilo no puede iniciar o detener otro hilo si no tiene la "habilidad" para el objeto de hilo correspondiente.

Los hilos interactúan y se sincronizan enviando mensajes a través de "puntos finales" de comunicación entre procesos. Un hilo con la capacidad de enviar al punto final correspondiente puede enviar un mensaje a otro hilo que tiene la capacidad de recibir a este punto final. Los objetos de notificación proporcionan sincronización entre conjuntos de semáforos binarios. La traducción de direcciones virtuales está controlada por objetos del núcleo que representan directorios de páginas, tablas de páginas y objetos de marco o abstracciones sutiles sobre los objetos de arquitectura de procesador correspondientes. Cada secuencia tiene una cierta capacidad "VSpace", que apunta a la raíz del árbol de objetos de traducción de direcciones de secuencia. Las capacidades en sí son administradas por el núcleo y almacenadas en los objetos del núcleo "CNodes" ubicados en la estructura del gráfico, que asigna enlaces a objetos con derechos de acceso, de forma similar a la comparación de tablas de páginas virtuales con direcciones físicas en la memoria. Cada hilo tiene su propia capacidad para identificar el código CN raíz. El conjunto de capacidades disponibles desde esta raíz, lo llamamos "CSpace Stream". Las habilidades se pueden transferir a través de puntos finales con transferencia de trabajo, y también se pueden declarar compartidas usando CSpace común. La Figura 2 muestra estos objetos del núcleo.


Fig. 2. Objetos de kernel en un sistema seL4 con dos hilos que interactúan a través de un punto final

Evidencia de seguridad

Debido a su versatilidad, las API del núcleo seL4 son de bajo nivel y admiten arquitecturas de sistemas altamente dinámicas. Por lo tanto, la evidencia directa de estas API es difícil de obtener.

El concepto de alto nivel de las políticas de control de acceso se extrae de objetos individuales y capacidades del núcleo, capturando en su lugar la configuración de control de acceso del sistema utilizando un conjunto de "sujetos" abstractos (componentes) y los poderes que cada uno de ellos tiene sobre los demás (por ejemplo, para leer datos y enviar mensajes) . En el ejemplo de la fig. 2, los componentes A y B obtuvieron autoridad sobre el punto final.

Sewell y sus colegas han demostrado que las políticas de control de acceso seL4 aseguran que se respeten dos características básicas de seguridad: restricción de privilegios e integridad.

La restricción de autoridad significa que la política de control de acceso es una aproximación segura estática (sin cambios) de capacidades específicas y objetos del núcleo en el sistema para cualquier estado futuro. Esta propiedad implica que no importa cómo evolucione el sistema, ningún componente recibirá más autoridad de lo que predice la política de control de acceso. En la Figura 2, la política para el componente B no tiene acceso de escritura al componente A. Por lo tanto, el componente B nunca podrá obtener este acceso en el futuro. Esta propiedad implica que el razonamiento a nivel de política es una aproximación segura al razonamiento sobre el estado específico de control de acceso en el sistema.

La integridad significa que no importa lo que haga el componente, nunca podrá cambiar los datos en el sistema (incluidas las llamadas al sistema que pueda hacer) que claramente no está permitido cambiar la política de control de acceso. Por ejemplo, en la fig. 2, el único componente de la autoridad de A sobre otro componente es el derecho a enviar datos al punto final desde donde el componente B recibe información. Esto significa que el componente A solo puede cambiar su estado, el estado del hilo B y el estado del búfer de mensajes. No puede cambiar otras partes del sistema.

Un efecto secundario de la integridad es la confidencialidad, cuando un componente no puede leer la información de otro componente sin permiso : es una propiedad comprobada de la no interferencia no transitiva seL4. Es decir, en un sistema configurado correctamente (con restricciones más estrictas que solo la integridad), ninguno de los componentes puede, sin permiso, encontrar información sobre otro componente o su ejecución. La prueba expresa esta propiedad en términos de la política de flujo de información, que se puede extraer de la política de control de acceso utilizada en la prueba de integridad. La información solo se transmitirá cuando la política lo permita explícitamente. La prueba cubre flujos de información explícitos, así como posibles canales de almacenamiento ocultos en el núcleo. Pero los canales de sincronización están fuera de su área y deben procesarse por otros medios .

La evidencia adicional en seL4 incluye una extensión de la corrección funcional y, por lo tanto, teoremas de seguridad a un nivel binario para la arquitectura ARMv7 y un perfil de tiempo de ejecución en el peor de los casos para el núcleo ( 1 , 2 ), que es necesario para los sistemas en tiempo real. El núcleo seL4 está disponible para varias arquitecturas: ARMv6, ARMv7 ARMv7a, ARMv8, RISC-V, Intel x86 e Intel x64. Por el momento, ha pasado las pruebas de máquina en la arquitectura ARMv7 para toda la pila de verificación, así como en ARMv7a con extensiones de hipervisor para la corrección funcional.

Arquitectura de seguridad

La sección anterior describió los métodos de programación mediante los cuales el núcleo seL4 crea una base sólida para sistemas demostrablemente confiables. El núcleo forma una base informática confiable (TCB), un componente esencial del software que debe funcionar correctamente para garantizar la seguridad del sistema. En sistemas reales, esta base es mucho más amplia que solo un microkernel. Es necesario verificar una pila de software adicional para obtener el mismo nivel de confianza que para el núcleo. Sin embargo, hay clases de sistemas para los cuales no hay necesidad de dicha verificación: necesitan teoremas de aislamiento a nivel del núcleo para derivar ciertas propiedades de seguridad a nivel del sistema. Esta sección proporciona un ejemplo de dicho sistema.

Estos son sistemas en los que las arquitecturas de componentes ya han implementado una propiedad crítica, tal vez junto con varios componentes pequeños de confianza. Nuestro ejemplo es el software de control de vuelo quadcopter, un dispositivo de demostración en el programa HACMS mencionado anteriormente.

La Figura 3 muestra los principales componentes de hardware del quadrocopter. La arquitectura es intencionalmente más compleja que la requerida por el quadcopter, ya que se suponía que representaba a ULB y en este nivel de abstracción es similar a la arquitectura de ULB.


Fig. 3. Arquitectura de una aeronave autónoma.

La figura muestra dos computadoras principales: una computadora a bordo que interactúa con la estación terrestre y controla el software a bordo (por ejemplo, la cámara), y una computadora de navegación para controlar el vuelo del vehículo, leer los datos del sensor y controlar los motores. Las computadoras están conectadas a través de una red interna o bus CAN en un quadrocopter, Ethernet en ULB. El quadrocopter también tiene un punto WiFi sin protección, lo que permite demostrar métodos de protección adicionales.

En este ejemplo, considere una computadora a bordo. Para ello se deben cumplir cuatro propiedades básicas:

• autenticación adecuada de comandos desde la estación terrestre;
  
• privacidad de claves criptográficas;
  
• sin mensajes adicionales para la computadora de navegación;
  
• El software no confiable de otros sistemas integrados no puede afectar el vuelo del dispositivo.

La hipótesis de trabajo es que la cámara no es confiable, potencialmente comprometida o maliciosa, que sus controladores y software obsoleto están potencialmente comprometidos, así como cualquier canal de comunicación externo. En este ejemplo, asumimos una criptografía correcta y sólida, es decir, que la clave no puede ser recogida, y vamos más allá del alcance de la tarea de suprimir las comunicaciones de radio del enemigo con una estación terrestre.

La Figura 4 muestra cómo la arquitectura quadrocopter está diseñada para proporcionar estas propiedades. La máquina virtual (VM) de Linux sirve como contenedor para el software de dispositivo integrado, los controladores de cámara y los puntos de acceso WiFi. Aislamos el módulo de control de criptografía en su propio componente, con conexiones al bus CAN, el canal de la estación terrestre y la máquina virtual Linux para enviar datos a la estación terrestre. La tarea del componente criptográfico es transmitir (solo) mensajes autorizados a la computadora de a bordo a través de la interfaz CAN de la pila y enviar datos de diagnóstico a la estación terrestre. El componente de radio envía y recibe mensajes sin procesar que son cifrados y descifrados (con autenticación) por el componente criptográfico.


Fig.4. Arquitectura de computadora a bordo de quadcopter simplificada

Establecer las propiedades deseadas del sistema se reduce únicamente a las propiedades de aislamiento y al comportamiento de la arquitectura en términos de flujos de información, así como al comportamiento de un único componente criptográfico confiable. Suponiendo el comportamiento correcto de este componente, las claves no pueden verse comprometidas, ya que ningún otro componente tiene acceso a ellas. El canal entre Linux y el componente criptográfico en la Fig. 4 está destinado solo a mensajes y no da acceso a la memoria. Solo los mensajes autorizados pueden ingresar al bus CAN, porque el componente criptográfico es la única comunicación con el bus. El software no confiable y WiFi, como parte de la máquina virtual Linux, están encapsulados por el aislamiento de componentes y solo pueden interactuar con el resto del sistema a través de un componente criptográfico confiable.

Es fácil imaginar que dicho análisis de arquitectura se puede automatizar en gran medida al verificar modelos y herramientas de razonamiento mecánico de un nivel superior. Como se señaló para los sistemas MILS , los límites de los componentes en dicha arquitectura no solo son una herramienta conveniente para la partición y la gestión de código, sino que con el aislamiento forzado proporcionan límites efectivos para el razonamiento formal sobre el comportamiento del sistema. Sin embargo, todo depende de la aplicación adecuada de los límites de los componentes en tiempo de ejecución en la implementación final del sistema binario.

Los mecanismos discutidos anteriormente del núcleo seL4 son capaces de proporcionar dicha implementación, pero el nivel de abstracción de los mecanismos contrasta fuertemente con los bloques y flechas del esquema arquitectónico: una política de control de acceso aún más abstracta aún contiene muchos más detalles que el esquema de arquitectura. En un sistema real de este tamaño, el software crea decenas de miles de objetos y "habilidades" del núcleo, y los errores de configuración pueden conducir a violaciones de seguridad. Luego discutimos cómo no solo automatizamos la configuración y creación de dicho código, sino también cómo demostrar automáticamente el cumplimiento de los límites de la arquitectura.

Verificación de componentes

Como la evidencia de seguridad se simplifica con abstracciones formales de las políticas de seguridad, la abstracción también ayuda en el diseño del sistema. La plataforma componente de Camkes se ejecuta en abstracciones seL4 en la parte superior de los mecanismos del núcleo de bajo nivel, proporcionando primitivas de comunicación y descomponiendo el sistema en unidades funcionales, como se muestra en la Fig. 5. Utilizando esta plataforma, los arquitectos de sistemas pueden diseñar y construir sistemas basados ​​en seL4 en términos de componentes de alto nivel que interactúan entre sí y con dispositivos de hardware a través de conectores, como llamadas a procedimiento remoto (RPC), puertos de datos y eventos.


Fig. 5. Flujo de trabajo de CAmKES

Generación de código

Internamente, CAmkES implementa estas abstracciones utilizando objetos de kernel de bajo nivel en seL4. Cada componente contiene (al menos) una secuencia, CSpace y VSpace. Los conectores RPC usan objetos de punto final y CAmkES genera código intermedio para procesar mensajes y enviarlos a puntos finales IPC. Del mismo modo, el conector del puerto de datos se implementa a través de la memoria compartida (tramas comunes presentes en los espacios de direcciones de dos componentes) y, opcionalmente, puede limitar la dirección de la transferencia de datos. Finalmente, el conector de eventos se implementa utilizando el mecanismo de notificación seL4.

CAmkES también genera en capDL una especificación de bajo nivel de la configuración inicial de objetos y las capacidades del núcleo del sistema. Esta especificación se convierte en entrada para el inicializador seL4, quecomienza primero después de cargar y realiza las operaciones seL4 necesarias para crear una instancia e inicializar el sistema .

Por lo tanto, la plataforma componente genera código sin esfuerzo adicional por parte del desarrollador. La arquitectura de componentes describe un conjunto de bloques y flechas, y la tarea de implementación se reduce a simplemente completar los campos. La plataforma genera el resto, proporcionando la implementación de la arquitectura descrita.

En una plataforma con componentes tradicionales, el código generado ampliará la base informática confiable del sistema, ya que puede afectar la funcionalidad de los componentes. Sin embargo, CAmkES también genera evidencia.

Evidencia auto

Al generar el código "intermedio", CAmkES produce pruebas formales en Isabelle / HOL, realiza la validación durante la traducción y demuestra que el código "intermedio" generado obedece la especificación de alto nivel, y la especificación capDL generada es la especificación correcta de la descripción de CAmkES . También hemos demostrado que el inicializador seL4 configura correctamente el sistema en la configuración inicial requerida. Al mismo tiempo, automatizamos la mayor parte de la construcción del sistema sin expandir la base informática confiable.

Los desarrolladores rara vez miran la emisión de generadores de código; solo están interesados ​​en la funcionalidad y la lógica empresarial. También asumimos que la evidencia del código intermedio no necesita ser verificada, es decir, los desarrolladores pueden enfocarse en probar la exactitud de su propio código. Así como el encabezado CAmkES generado le da al desarrollador una API para el código generado, los operadores de lema de nivel superior producen una API como prueba. Los lemas describen el comportamiento esperado de los conectores. En el ejemplo de middleware RPC en la Figura 6 funciones generadas$$ proporciona una forma de llamar a una función remota$f$$$ en otro componente. Para guardar la abstracción, llame$g$$$ debería ser equivalente a llamar$f$$$$g$ . El sistema generado lemma asegura que $$del código RPC generado se comporta como una llamada directa$f$$$$g$ .


Fig. 6. Código RPC generado

Para el uso real de evidencia generada por el sistema, deben ser componibles con (casi) evidencia arbitraria provista por el usuario, como para una función$$ , y para contextos en los que$g$$$$g$ y $$$f$.Para lograr esta compostibilidad, la especificación del conector se parametriza a través de especificaciones proporcionadas por el usuario para funciones remotas. De esta manera, los ingenieros pueden razonar sobre su arquitectura al proporcionar especificaciones y evidencia para sus componentes, y confiar en las especificaciones para el código generado.

Hasta la fecha, hemos demostrado este proceso de principio a fin utilizando el conector especial CAmkES RPC ( 1 , 2 ). Dado que las plantillas para otros conectores (puertos de datos y eventos) son mucho más simples que los RPC, no será difícil expandir el generador de evidencia para admitir estos conectores, lo que le permitirá crear sistemas verificados más diversos.

Después del código de comunicación, CAmkES crea la configuración de control de acceso inicial para aplicar los límites de la arquitectura. Para probar que estas dos descripciones del sistema, capDL y CAmkES, coinciden entre sí, considere la descripción de CAmkES como una abstracción para la descripción de capDL. Usamos el marco previamente probado para derivar la autoridad de un objeto sobre otro objeto a partir de la descripción de capDL. Entonces aumentaremos la evidencia al nivel de la política. Además, hemos definido reglas para retirar la autoridad entre componentes en la descripción de CAmkES. Esta prueba garantiza que los objetos capDL representados como un gráfico de privilegios con objetos agrupados por componentes tengan los mismos límites entre grupos que en el gráfico de componentes CAmkES equivalente. Intuitivamente, esta correspondencia de límites significa que el análisis de la arquitectura de la política a partir de la descripción de CAmkES salvará la política de la descripción generada por capDL, que, a su vez, garantiza los requisitos de restricción de autoridad, integridad y confidencialidad, como se mencionó anteriormente.

Finalmente, para probar la correcta inicialización, CAmkES usa un inicializador universal que comienza como la primera tarea del usuario después de la carga. En seL4, esta primera (y única) tarea del usuario tiene acceso a toda la memoria disponible, usándola para crear objetos y "habilidades" de acuerdo con la descripción detallada de capDL, que acepta como entrada. Está comprobado queEl estado después de la ejecución del inicializador satisface el estado descrito en la especificación especificada . Esta prueba es válida para el modelo de inicializador exacto, pero aún no en el nivel de implementación. En comparación con la profundidad del resto de la cadena de evidencia, esta limitación puede parecer débil, pero ya es una evidencia más formal que la requerida en el nivel más alto (EAL7) de los criterios generales de evaluación de seguridad.

Actualización de seguridad sísmica

En la práctica, es difícil garantizar el desarrollo de un sistema desde cero por razones de seguridad; por lo tanto, la capacidad de actualizar el software antiguo es crucial para desarrollar sistemas seguros. Nuestro marco basado en seL4 admite un proceso iterativo que llamamos "actualizaciones de seguridad sísmica", ya que un arquitecto regular actualizará los edificios existentes para una mayor estabilidad sísmica. Ilustramos el proceso con el ejemplo de la adaptación gradual de la arquitectura de software existente de un helicóptero no tripulado, pasando del esquema de prueba tradicional a un sistema altamente confiable con teoremas respaldados por métodos formales. Aunque este ejemplo se basa en un proyecto ULB real, se simplifica aquí y no incluye todos los detalles.

La arquitectura original del helicóptero coincide con la arquitectura descrita en la Fig. 3. Su funcionalidad es proporcionada por dos computadoras separadas: la computadora de navegación controla el vuelo real y la computadora de a bordo realiza tareas de alto nivel (como comunicarse con una estación terrestre y navegar la imagen desde la cámara). La versión inicial de la computadora de a bordo era una aplicación monolítica para Linux. Durante el proceso de modernización, los ingenieros de Boeing aplicaron los métodos, herramientas y componentes proporcionados por los socios de HACMS.

Paso 1. Virtualización

El primer paso fue tomar el sistema como está y ejecutarlo en una máquina virtual encima de un hipervisor seguro (ver Figura 7). En la metáfora de la modernización sísmica, esto corresponde a colocar el sistema sobre una base más móvil. Una máquina virtual encima de seL4 en este sistema consta de un componente CAmkES, que incluye un monitor de máquina virtual (VMM) y un sistema operativo invitado, en este caso Linux. El núcleo proporciona abstracciones de hardware de virtualización, y VMM gestiona estas abstracciones para la máquina virtual. El núcleo seL4 limita no solo el sistema operativo invitado, sino también VMM, por lo que no necesita confiar en la implementación de VMM para proporcionar aislamiento forzado. Una falla de VMM dará como resultado una falla del sistema operativo invitado, pero no una falla de todo el sistema.


Fig. 7. Toda la funcionalidad en una máquina virtual.

Dependiendo de la configuración del sistema, la máquina virtual puede tener acceso a dispositivos a través de controladores paravirtualizados, controladores de paso o ambos. En el caso de los controladores de paso, los desarrolladores pueden usar el sistema MMU o IOMMU para evitar la violación de los límites de aislamiento por parte de los dispositivos de hardware y los controladores en el sistema invitado. Tenga en cuenta que simplemente iniciar el sistema en una máquina virtual no agrega beneficios adicionales de seguridad o confiabilidad. El paso 1 solo es necesario para prepararse para el paso 2.

Paso 2. Múltiples máquinas virtuales

El segundo paso de la modernización sísmica fortalece los muros existentes. En software, un desarrollador puede aumentar la seguridad y la confiabilidad dividiendo el sistema fuente en varios subsistemas, cada uno de los cuales consiste en una máquina virtual que solo ejecuta parte del código del sistema fuente. Cada combinación VM / VMM se realiza en un componente CAmkES separado, que introduce aislamiento entre diferentes subsistemas, no les permite influirse entre sí, y luego permite la coexistencia de diferentes niveles de seguridad.

En general, las secciones siguen la arquitectura de software existente, aunque si la arquitectura no es suficiente para un aislamiento efectivo, puede ser necesario un rediseño.

Como regla general, las secciones deben interactuar entre sí, por lo que en este punto también agregaremos canales de comunicación. Para garantizar la seguridad, es imperativo que estas interfaces sean estrechas, limitando la conexión entre particiones a solo lo que sea absolutamente necesario. Además, los protocolos de interfaz deben ser eficientes, con un número mínimo de mensajes o volumen de datos. Es crítico que seL4 le permita controlar y limitar el intercambio de memoria entre particiones para minimizar la cantidad de datos.

Además de las máquinas virtuales que representan los subsistemas del sistema fuente, también extraemos e implementamos componentes para cualquier recurso compartido (como una interfaz de red).

Puede repetir el paso 2 hasta que alcancemos el detalle deseado de las secciones. El detalle correcto es un compromiso entre la resistencia del aislamiento, por un lado, y el aumento de los gastos generales de comunicación y los costos de reconstrucción, por otro lado.

En nuestro ejemplo, tenemos tres secciones: una máquina virtual que implementa las funciones de comunicación de una estación terrestre que ejecuta Linux; otra máquina virtual que implementa funciones de navegación basadas en cámara (también ejecutando Linux); y un componente nativo de red compartida, como se muestra en la fig. 8)


Fig.8. Funcionalidad dividida en varias máquinas virtuales.

Paso 3. Componentes nativos

Cuando un sistema se descompone en secciones separadas de una máquina virtual, algunas o todas las secciones individuales se pueden volver a implementar como componentes nativos, en lugar de máquinas virtuales. Esto reducirá significativamente la superficie de ataque para la misma funcionalidad. Una ventaja adicional de convertir un componente en código de máquina es reducir la carga y aumentar la productividad, eliminando el SO huésped y la sobrecarga de la ejecución del código y la comunicación VMM.

Los componentes nativos también aumentan el potencial para aplicar la verificación formal y otros métodos para aumentar la confiabilidad de un componente. Las opciones son diferentes: desde la verificación funcional completa del código nativo hasta la generación conjunta de código y evidencia, verificación del modelo, uso de lenguajes de programación de tipo seguro, análisis estático o pruebas rigurosas tradicionales de una base de código más pequeña.

Gracias al aislamiento proporcionado por seL4 y la arquitectura de componentes, es posible trabajar juntos en un sistema de componentes con diferentes niveles de confiabilidad. En este caso, los componentes de baja confiabilidad no reducen la confiabilidad general del sistema, y ​​los desarrolladores se benefician del hecho de que no necesita gastar esfuerzo para verificar este código.

En nuestro ejemplo, analizaremos la máquina virtual para el canal de comunicación entre la computadora de a bordo y la estación terrestre en módulos nativos. En los componentes nativos, se implementan las funciones de comunicación, criptografía y control (mission-manager). Dejaremos la cámara y WiFi en la máquina virtual como un componente obsoleto poco confiable (ver Fig. 9). Esta separación se ha convertido en un compromiso entre los esfuerzos para rehacer subsistemas y los beneficios de usar componentes nativos en términos de rendimiento y confiabilidad.


Fig. 9. Funcionalidad implementada en componentes nativos

Paso 4. Fiabilidad del sistema en su conjunto.

Una vez recibidos todos los módulos necesarios, daremos el paso final: análisis de todo el sistema en su conjunto basado en la fiabilidad de la arquitectura y los componentes individuales.

Dentro del marco de HACMS, la comunicación, la criptografía y un módulo de control se implementan en el lenguaje orientado a objetos de seguridad probada tipo Ivory , con asignación de una cantidad fija de memoria en el montón. Sin verificación adicional, Ivory no nos da garantías de corrección funcional, pero da confianza en la tolerancia a fallas y la confiabilidad de emergencia. Dado el aislamiento de los componentes, creemos que estas garantías permanecen en presencia de componentes poco confiables (como la máquina virtual de la cámara).

El componente de red se implementa en el código C estándar, que consiste en el código de usuario para la plataforma y el código de la biblioteca existente. Su nivel de confiabilidad corresponde al nivel obtenido a través de la implementación cuidadosa de código conocido. La confiabilidad se puede mejorar sin muchos gastos mediante el uso de métodos como la síntesis de controladores , así como el uso de lenguajes de tipo seguro como Ivory. En un análisis general de la seguridad del sistema, cualquier compromiso de un componente de red solo afectará a los paquetes de red. Dado que el tráfico está encriptado, dicho ataque no pondrá en peligro la condición de las especificaciones que solo los comandos autorizados ingresan a la computadora a bordo.

La máquina virtual de la videocámara es la parte más débil del sistema, ya que se ejecuta en el sistema Linux y se supone que contiene vulnerabilidades. Pero la VM está aislada, por lo que si los atacantes la rompen, no podrán moverse a otros componentes. Lo peor que puede hacer un atacante es enviar los datos incorrectos al componente de control. Como en el quadrocopter, este componente verifica los datos recibidos de la cámara. Y resistió con éxito el ciberataque mencionado al principio del artículo. Fue un ataque de "caja blanca", donde el equipo de Pentesters tuvo acceso a todo el código y la documentación, así como a todos los canales de comunicación externos. Se le otorgó intencionalmente acceso de root a la máquina virtual de la cámara, simulando un ataque exitoso a un software obsoleto. La contención del ataque y la capacidad de defenderse contra este escenario muy poderoso se convirtió en una prueba digna de nuestros requisitos de seguridad y la identificación de cualquier supuesto perdido, problemas de interfaz u otros problemas de seguridad que el equipo de investigación podría no reconocer.

Limitaciones y trabajo futuro

Este artículo proporciona una descripción general del método para lograr niveles muy altos de seguridad para sistemas en los que la característica de seguridad es aplicable a través de la arquitectura de componentes. Hemos probado teoremas para el nivel de kernel y su configuración correcta, así como teoremas que garantizan que la plataforma de componentes establece correctamente los límites de seguridad de acuerdo con la descripción de su arquitectura, y que genera el código correcto para llamadas a procedimientos remotos. La conexión con el análisis de seguridad de alto nivel del sistema sigue siendo informal, y los teoremas del código de comunicación no cubren todas las primitivas de comunicación proporcionadas por la plataforma. Para obtener automáticamente un teorema que cubra todo el sistema de principio a fin, se requiere trabajo adicional. Sin embargo, en esta etapa está claro que esta es una tarea factible.

El objetivo principal del trabajo presentado es reducir drásticamente los esfuerzos de verificación para clases específicas de sistemas. El enfoque puramente arquitectónico descrito aquí puede extenderse a sistemas distintos de ULB, pero está claramente limitado por el hecho de que solo puede expresar propiedades determinadas por la arquitectura de componentes del sistema. Los retornos disminuirán si esta arquitectura cambia durante la ejecución del programa, y ​​si las propiedades dependen críticamente del comportamiento de demasiados componentes confiables o componentes de un tamaño demasiado grande.

El primer paso para aliviar estas limitaciones es crear una biblioteca de componentes probados previamente de un alto nivel de confiabilidad para su uso como bloques de construcción confiables en tales arquitecturas. Esta biblioteca puede incluir patrones de seguridad (como desinfección de datos de entrada, filtros de salida, monitores de privacidad y tiempo de ejecución) potencialmente generados a partir de especificaciones de nivel superior, así como componentes de infraestructura como módulos criptográficos reutilizables, almacenamiento de claves, sistemas de archivos, Pilas y controladores de red altamente confiables. Si la seguridad depende de más de uno de esos componentes, entonces es necesario justificar la confiabilidad de su interacción y uso compartido. Los principales problemas técnicos aquí son las discusiones sobre concurrencia y protocolos, así como el flujo de información en presencia de componentes confiables. A pesar de estas limitaciones, el trabajo demuestra el rápido desarrollo de sistemas reales altamente confiables basados ​​en seL4. Actualmente, la creación de tales sistemas es posible a un costo menor que las pruebas tradicionales.

Aplicación: costos laborales

El desarrollo del diseño y el código para seL4 tomó dos años-hombre. Si agregamos toda la evidencia específica de serotipo, se obtendrá un total de 18 años-persona para 8700 líneas de código para C.Para la comparación, el desarrollo de un microkernel de tamaño comparable L4Ka :: Pistacho de la familia seL4 tomó seis años-hombre y no proporcionó un nivel significativo de confiabilidad. Esto significa una diferencia en la velocidad de desarrollo de solo 3.3 veces entre el software verificado y el tradicional. Según el método de evaluación de Colbert y Bohm , la certificación de acuerdo con los criterios tradicionales EAL7 para 8700 líneas de código C tomará más de 45.9 años-persona. Esto significa que la verificación formal de la implementación a nivel binario ya es 2.3 veces más barata que el nivel más alto de certificación según los criterios generales, al tiempo que proporciona una confiabilidad significativamente mayor.

A modo de comparación, el enfoque HACMS descrito aquí utiliza solo la evidencia existente para cada nuevo sistema, incluida la evidencia generada por las herramientas. Por lo tanto, el esfuerzo de prueba general para un sistema que coincide con este enfoque se reduce a semanas-hombre, no a años, y las pruebas se reducen solo para validar los supuestos.