Lo que una demostración puede prometer

Por lo general se confía en el software porque se ha probado. Alguien pensó en las formas en que podía fallar, las ensayó y vio cómo respondía. Eso funciona bien, hasta que llega el caso en el que nadie pensó.

Una demostración empieza por el otro extremo. No ensaya casos. Muestra, con matemáticas, que una afirmación se cumple en todos.

Todos los casos, no solo los que probamos

Tomemos una promesa pequeña: este código nunca lee más allá del final de su búfer. Una prueba puede darle mil entradas, o mil millones, e informar de que ninguna lo hizo fallar. Una demostración dice algo de otra clase: no hay ninguna entrada que lo haga fallar. No se encontró ninguna, y no existe ninguna.

El precio es el rigor. Una demostración necesita un enunciado exacto de lo que el código debe hacer, su especificación, y un argumento que conecte cada línea del código con él. En el software real, ese argumento es demasiado largo para que una persona lo revise a simple vista. Así que lo comprueba un ordenador.

Comprobada por máquina

Eso significa «comprobada por máquina». La demostración se escribe completa, en un lenguaje que puede leer un programa llamado asistente de demostración, y el programa coteja cada paso con las reglas de la lógica. No se cansa en la página novecientos, y no se fía de la palabra de nadie.

Las demostraciones de seL4 se comprueban así, en un asistente de demostración llamado Isabelle/HOL. Son públicas, y cualquiera puede volver a ejecutarlas.

Qué dicen las demostraciones de seL4

seL4 es el núcleo sobre el que se ejecuta todo sistema NoWayOS: unas 10 000 líneas de código, y el único código con control total del dispositivo. Su tamaño es la clave. Un argumento sobre diez mil líneas se puede terminar. Uno sobre decenas de millones, todavía no.

La seL4 Foundation expone las demostraciones por capas:

• El código hace lo que dice la especificación, y nada más. De ahí se sigue una lista de cosas que el núcleo no puede hacer: desbordar un búfer, seguir un puntero nulo, perder memoria, dividir por cero.
• El programa que se ejecuta corresponde al código que se demostró. Entre ambos hay un compilador, así que otra demostración comprueba su salida.
• El núcleo puede mantener separadas las partes de un sistema. Una parte no puede modificar los datos de otra, ni leerlos, ni quitarle los recursos que necesita, a menos que se le haya concedido ese derecho.
• Un sistema puede arrancar en el estado para el que fue diseñado, con exactamente los permisos que enumera su descripción.

No todas las capas están terminadas para todos los procesadores y todas las configuraciones. Eso importa, y volveremos a ello.

Lo que una demostración da por sentado

Una demostración es exactamente tan amplia como su enunciado, y se apoya en sus supuestos. seL4 pone los suyos por escrito: que el hardware se comporta como dice su modelo, que unos pocos cientos de líneas del código de más bajo nivel son correctas, que el código que se ejecuta antes de que arranque el núcleo ha hecho su trabajo. La demostración de confidencialidad no cubre los tiempos de ejecución.

No dice nada sobre si la especificación pide lo correcto, ni sobre el software que está por encima del núcleo. Un núcleo demostrado aislará fielmente un programa que tenga un error. El error sigue ahí. Solo que no puede alcanzar nada más.

Eso no es una debilidad de las demostraciones. Es lo que las hace valiosas: dicen con precisión qué cubren, de modo que usted sabe con precisión qué queda.

Dónde está NoWayOS

Esta es la posición, sin rodeos. NoWayOS se ejecuta sobre seL4, pero ninguna imagen de NoWayOS está hoy dentro de las demostraciones completadas de seL4. NoWayOS usa la configuración de criticidad mixta de seL4, cuyas demostraciones para nuestros procesadores están en curso. Y las demostraciones de seL4 nunca cubrieron el código propio de NoWayOS. Por eso no decimos que NoWayOS esté “verificado formalmente”, y no lo diremos.

Cada imagen dice dónde está. Un archivo junto a ella enumera la configuración de su núcleo, opción por opción, frente a la que seL4 ha demostrado. Seguridad muestra uno real.

Demostraciones más pequeñas, las nuestras

El código de NoWayOS obtiene su garantía por otro camino: Rust, aislamiento, revisión, pruebas y demostraciones de un tipo más modesto.

Cada decodificador de los mensajes que pasan entre las partes de un sistema tiene demostraciones acotadas, hechas con un verificador de modelos llamado Kani. Una demostración acotada cubre toda entrada hasta un tamaño indicado, aquí el registro más largo que acepta un decodificador. Dentro de esa cota es una demostración de verdad: ninguna entrada hace que el decodificador entre en pánico, se desborde o lea fuera de los límites. Más allá de la cota no dice nada, y por eso la cota es la entrada más larga que existe.

Después rompemos los decodificadores a propósito, para asegurarnos de que las demostraciones lo notan. Una demostración que no puede fallar no es mejor que una prueba que no puede fallar.

Su tamaño real

Una demostración no hace que nada sea “inhackeable”. Hace que una afirmación sea cierta, en todos los casos, bajo supuestos que usted puede leer. Conozca la afirmación y los supuestos, y sabrá lo que tiene.

Por eso NoWayOS se construye sobre el núcleo que las tiene, y por eso le dice, imagen por imagen, hasta dónde llegan.