Verve (sistema operativo)

Verve es un sistema operativo de investigación desarrollado por Microsoft Research . Verve ha sido verificado de extremo a extremo en cuanto a seguridad de tipos y seguridad de memoria .

Debido a su complejidad, verificar las propiedades de los sistemas operativos ha sido un objetivo fundamental en la verificación de software . Estos sistemas suelen estar escritos en lenguajes de bajo nivel, como C++ , que ofrecen muy pocas garantías. El Proyecto Singularity optó por escribir un sistema operativo en C# , un lenguaje seguro en cuanto a tipos y memoria. Una desventaja de este enfoque es que los sistemas operativos necesitan necesariamente llamar a código de bajo nivel para, por ejemplo, mover el puntero de pila. Verve resuelve este problema dividiendo el sistema operativo en un lenguaje ensamblador verificado , que debe ser de bajo nivel, y una interfaz confiable para el resto del sistema, escrita en C#. Existe una especificación confiable que garantiza que el código ensamblador de bajo nivel no modifica el montón y que el código C# de alto nivel no modifica 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 Kernel , que utiliza las primitivas proporcionadas por el Núcleo para exponer una interfaz más tradicional a las aplicaciones. Todos los componentes del sistema, excepto el Núcleo, están escritos en código administrado C# y compilados por Bartok (desarrollado originalmente para el proyecto Singularity ) a lenguaje ensamblador tipado (TAL), que es verificado por un verificador TAL.

El Núcleo implementa un asignador de memoria y recolección de basura, soporte para cambio de pila y gestión de manejadores de interrupciones. Está escrito en BoogiePL, que sirve como entrada para el verificador Boogie de MSR , que prueba la corrección del Núcleo utilizando el probador de teoremas automatizado (solucionador) de satisfacibilidad módulo teorías (SMT) Z3 Theorem Prover . El Núcleo depende del Kernel para implementar hilos, planificación, sincronización y para proporcionar la mayoría de los manejadores de interrupciones. Aunque el Kernel no está verificado formalmente, por lo que, por ejemplo, un error en la planificación podría causar que el sistema se bloquee, 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 no válidas al Núcleo, la verificación formal garantiza que el Núcleo maneja la situación de manera controlada .

La base de computación confiable (TCB) de Verve se limita a: Boogie/Z3 para verificar la corrección del Nucleus; BoogieASM para traducirlo a lenguaje ensamblador x86; la especificación BoogiePL sobre cómo debe comportarse el Nucleus; el verificador TAL; el ensamblador y el enlazador; y el gestor de arranque. Cabe destacar que ni el compilador/entorno de ejecución de C# ni el compilador Bartok forman parte de la TCB.

• Seguridad hasta la última instrucción: Verificación automatizada de un sistema operativo con tipado seguro , Jean Yang y Chris Hawblitzel. Diseño e implementación de lenguajes de programación , 2010.
• Seguridad hasta la última instrucción: Verificación automatizada de un sistema operativo con tipado seguro , Jean Yang y Chris Hawblitzel. Artículo destacado de investigación de CACM. Communications of the ACM , septiembre de 2010.
• Perspectiva técnica: ¡La seguridad es lo primero!
• Verve: Un sistema operativo con tipado seguro . Entrevista con Chris Hawblitzel.
• Verve: Un sistema operativo con tipado seguro . Noticias del sistema operativo .
• Presentamos Verve: un sistema operativo con tipado seguro . InfoQ .