Verve, el SO experimental de MS es seguro hasta la última instrucción

Microsoft cuenta entre sus unidades menos conocidas con una dedicada a la investigación: Microsoft Research. Ésta tiene una gran reputación en distintos campos que abarcan desde las ciencias sociales a las bases de datos, pasando por el machine learning, las redes o el hardware. Es corriente encontrar artículos salidos de estos laboratorios en revistas científicas de primer nivel.

Una de las últimas novedades de Microsoft Research es un sistema operativo experimental llamado Verve, basado en un SO previo, también experimental, denominado Singularity. Hay que resaltar el hecho de que ninguno tiene que ver con Windows y que son experimentales, es decir, herramientas de investigación, por lo que no llegaremos a verlos en el canal comercial. No obstante serán la base para el desarrollo de características que, con el tiempo, se irán incorporando en los sistemas finales, como podría ser Windows.

Singularity era un SO que tenía la particularidad de estar escrito en código supervisado (managed code), no en ensamblador y C/C++ como es habitual. Verve tiene una estructura algo más compleja y se compone de tres capas fundamentales:

• El núcleo (nucleus) está escrito en TAL (Typed Assembly Language) y se encarga de facilitar el acceso al hardware y la memoria a través de servicios de asignación de memoria, interrupciones, recolección de basura, etc.
• El kernel se dispone sobre el núcleo, está escrito en lenguaje C# y ofrecerá los servicios de alto nivel como puede ser la gestión de hilos de ejecución.
• El código de las aplicaciones se encuentra en la capa superior, escrito en C# y haciendo uso de los servicios del kernel o, directamente, de los del núcleo

Esta arquitectura queda reflejada gráficamente en la figura inferior, procedente del artículo Safe to de Last Instruction: Automated Verification of a Type-Safe Operating System hecho público por Microsoft Research.

El clásico kernel de los sistemas operativos tradicionales en Verve se divide en dos capas: el núcleo de bajo nivel escrito en ensamblador y encargado básicamente de servir como abstracción del hardware y el kernel con servicios para aplicaciones. En cualquier caso, todo el código, tanto el escrito originalmente en TAL como el implementado en C#, es finalmente compilado a TAL, un ensamblador con seguridad de tipos y que emplea lógica de Hoare para asegurar la validez de cada una de las instrucciones ejecutadas.

Lo que se consigue con Verve es tener un sistema operativo que incluye una verificación automatizada del código que ejecuta, con independencia de que éste forma parte del núcleo, del kernel, de controladores de dispositivos o de una aplicación externa, incrementando así la seguridad y estabilidad del sistema. La única parte no verificada es el Boot loader que aparece en la figura anterior situado en el margen izquierdo, encargado (como su propio nombre indica) de poner en marcha el sistema, interactuando con el núcleo tras verificar y configurar el mapa de memoria con el que trabajará Verve.

Recomiendo la lectura del citado artículo a cualquiera que esté interesado no ya en el desarrollo de sistemas operativos, sino a cualquier programador que desee aprender cosas nuevas de una de las fuentes más reputadas en este campo.