Verve es un sistema operativo de investigación desarrollado por Microsoft Research . Verve se verifica de extremo a extremo para la seguridad de tipos y la seguridad de la memoria .
Desarrollador | Investigación de Microsoft |
---|---|
Escrito en | BoogiePL , C # ; gestor de arranque en lenguaje ensamblador , C ++ |
Familia OS | Sistemas operativos basados en idiomas |
Estado de trabajo | En desarrollo por Microsoft Research |
Modelo fuente | Fuente disponible (a través de la Iniciativa de fuente compartida ) |
Último lanzamiento | r73999 / 10 de noviembre de 2013 |
Plataformas | x86 |
Tipo de grano | Microkernel , basado en el lenguaje |
Licencia | Licencia de investigación de Microsoft |
Debido a su complejidad, un santo grial de la verificación de software ha sido verificar las propiedades de los sistemas operativos. Los sistemas operativos suelen estar escritos en lenguajes de bajo nivel, como C , que ofrecen muy pocas garantías. El proyecto Singularity adoptó el enfoque de escribir un sistema operativo en C # , un lenguaje seguro para escribir y para memoria. Una debilidad de este enfoque es que los sistemas operativos necesariamente necesitan llamar al código de nivel inferior para, por ejemplo, mover el puntero de la pila. Verve soluciona este problema dividiendo el sistema operativo en un ensamblaje verificado que debe ser de bajo nivel y una interfaz confiable para el resto del sistema operativo, escrito en C #. Existe una especificación confiable que garantiza que el código de ensamblaje de bajo nivel no interfiere con el montón y que el código C # de alto nivel no interfiere con las pilas.
Verve consta de un pequeño núcleo , que actúa como una capa mínima de abstracción de hardware, y un núcleo , que utiliza primitivas proporcionadas por el núcleo para exponer una interfaz más tradicional a las aplicaciones. Todos los componentes del sistema que no sean Nucleus están escritos en C # administrado y compilados por Bartok (originalmente desarrollado para el proyecto Singularity ) en lenguaje ensamblador mecanografiado , que es verificado por un verificador TAL.
El Nucleus implementa un asignador de memoria y recolección de basura, soporte para cambio de pila y administración de manejadores de interrupciones. Está escrito en BoogiePL, que sirve como entrada para el verificador Boogie de MSR , que demuestra que Nucleus es correcto utilizando el solucionador Z3 SMT . El núcleo se basa en el núcleo para implementar subprocesos, programación, sincronización y para proporcionar la mayoría de los controladores de interrupciones. Aunque el Kernel no se verifica formalmente, por ejemplo, un error en la programación podría hacer que el sistema se cuelgue, no puede violar la seguridad de tipos o de memoria y, por lo tanto, no puede causar directamente un comportamiento indefinido. Si intenta hacer solicitudes inválidas al Nucleus, la verificación formal garantiza que el Nucleus maneja la situación de manera controlada .
La base informática confiable de Verve se limita a: Boogie / Z3 para verificar la corrección del Nucleus; BoogieASM para traducirlo en ensamblado x86; la especificación BoogiePL de cómo debería comportarse el Nucleus; el verificador TAL; el ensamblador y enlazador; y el gestor de arranque. En particular, ni el compilador / tiempo de ejecución de C # ni el compilador Bartok son parte de TCB.
Referencias
- Seguro hasta la última instrucción: verificación automatizada de un sistema operativo con seguridad de tipos , Jean Yang y Chris Hawblitzel. Diseño e implementación de lenguajes de programación , 2010.
- Seguro hasta la última instrucción: verificación automatizada de un sistema operativo con seguridad de tipos , Jean Yang y Chris Hawblitzel. Lo más destacado de la investigación del CACM. Comunicaciones de la ACM , septiembre de 2010.
- Perspectiva técnica: ¡La seguridad es lo primero!
- Verve: Un tipo de sistema operativo seguro . Entrevista a Chris Hawblitzel.
- Verve: Un tipo de sistema operativo seguro . OSnews .
- Anuncio de Verve: un sistema operativo de tipo seguro . InfoQ .