Microkernel seL4. Verificaci贸n formal de programas en el mundo real.

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 鈥嬧媏n 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 鈥嬧媏n 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 remotaf en otro componente. Para guardar la abstracci贸n, llameg deber铆a ser equivalente a llamarfg . El sistema generado lemma asegura que del c贸digo RPC generado se comporta como una llamada directafg .


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 quegg 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 鈥嬧媗os 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 鈥嬧媠i 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 鈥嬧媏n 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.

Source: https://habr.com/ru/post/437406/


All Articles