From LaTeX and OCaml to LEAN4 and Executables: Lean-Checked Theorems and Generating Proof-Carrying Rust

En el mundo del software, existe una tensión constante entre cómo escribimos el código y cómo sabemos que es seguro. Los programadores utilizan lenguajes de alto nivel para describir una lógica compleja de una manera que sea legible y manejable, pero las máquinas que ejecutan este código hablan un lenguaje mucho más simple y rígido. Para pasar de uno al otro, los compiladores actúan como traductores, pero es en este proceso de traducción donde los errores suelen esconderse. Un error en la traducción puede convertir una instrucción segura en una peligrosa, causando que un programa falle o se comporte de manera impredecible. Durante décadas, la forma más fiable de garantizar la seguridad ha sido verificar el código máquina final, pero esto es difícil porque el significado de alto nivel del programa original suele perderse en el proceso. La pregunta que los investigadores se plantean es si podemos mantener la claridad del lenguaje original de alto nivel y, al mismo tiempo, demostrar con absoluta certeza que las instrucciones de máquina finales harán exactamente lo que pretendemos.

Brent Hartshorn ha construido un sistema que responde a esta pregunta tratando una única pieza de código como dos cosas diferentes a la vez. Imagine un documento que puede leerse simultáneamente como una prueba matemática y como un conjunto de instrucciones para una máquina. En este nuevo trabajo, el autor toma un subconjunto de un lenguaje de programación llamado OCaml, conocido por sus reglas estrictas sobre cómo se manejan los datos, y le otorga a cada definición dos significados distintos. Primero, el código se lee como un argumento lógico, donde la estructura del propio programa sirve como prueba de que ciertas condiciones se cumplirán siempre. Segundo, el mismo código se traduce a un lenguaje diferente llamado Rust, diseñado para la velocidad y la seguridad, y luego se compila en un programa que una computadora puede ejecutar realmente. La brillantez del enfoque reside en la verificación: la prueba lógica es comprobada por un pequeño motor matemático de confianza, mientras que el programa en ejecución se comprueba contra un intérprete de referencia que simula el código paso a paso. Si ambos coinciden, y si la prueba lógica se sostiene, el resultado es una pieza de software que viene con su propio certificado de seguridad.

Los investigadores comenzaron construyendo un traductor que entiende una porción específica de OCaml. Este traductor, escrito en Python, es lo suficientemente pequeño como para ser leído y comprendido por una sola persona, lo cual es crucial porque si el propio traductor es demasiado complejo, no podemos confiar en su producción. Toma el código OCaml y lo divide en dos caminos. En el camino de la prueba, convierte el código en un formato que un núcleo matemático pueda verificar. Este núcleo es un programa diminuto que actúa como juez, verificando que la lógica sea sólida sin hacer suposiciones. En el camino del programa, el traductor convierte el código en Rust, un lenguaje que se compila en código máquina nativo y rápido. Para asegurar que la traducción fuera perfecta, el equipo también construyó un intérprete de referencia que ejecuta el código OCaml original directamente. Luego ejecutaron trece programas de ejemplo diferentes a través de la versión de Rust compilada y el intérprete. En cada uno de los casos, el código compilado produjo exactamente la misma salida que el intérprete, demostrando que el proceso de traducción no alteró el comportamiento de los programas.

Una vez que el código fue traducido con éxito, el equipo aplicó una rigurosa comprobación de seguridad a la versión de Rust compilada. Trataron el código compilado como un contrato, donde reglas específicas sobre cómo debería comportarse el programa fueron escritas como teoremas matemáticos. Por ejemplo, comprobaron que los cálculos de enteros nunca se desbordaran accidentalmente y dieran la vuelta hacia un número negativo, una fuente común de errores en el software. Descubrieron que, si bien la mayoría de estas reglas de seguridad se cumplían, existían casos específicos donde las reglas se rompían. En once escenarios diferentes, el código compilado llegó a un punto donde un cálculo de enteros podía dar la vuelta, como cuando se resta el número más pequeño posible de cero. El sistema identificó correctamente estos como obligaciones abiertas, lo que significa que el código es seguro en todas partes excepto en estos límites específicos y conocidos. De un total de noventa comprobaciones de seguridad realizadas en los programas de ejemplo, setenta y nueve fueron plenamente probadas, mientras que las once restantes quedaron abiertas porque representaban límites reales y alcanzables en la forma en que la computadora maneja los números.

El proyecto fue más allá al aplicar este método a un pequeño núcleo de sistema operativo, una pieza central de software que gestiona los recursos de la computadora. Los investigadores tomaron un núcleo que había sido escrito previamente en Python y Rust y lo reescribieron en su subconjunto de OCaml. Luego tradujeron esta nueva versión a Rust y la compilaron. El resultado fue una tercera implementación del mismo núcleo. Al probarla contra la versión original de Python, la nueva versión derivada de OCaml respondió correctamente en los 236 casos de prueba. El equipo intentó entonces demostrar la seguridad de este nuevo núcleo. Lograron probar 227 de las 236 obligaciones de seguridad. Las pocas que quedaron sin probar no fueron errores en el código, sino brechas en las herramientas matemáticas utilizadas para comprobarlas, específicamente en relación con cómo el sistema maneja bucles y contadores complejos. Esto demostró que el método podía escalar desde ejemplos pequeños hasta un componente funcional de un sistema operativo.

Quizás la parte más sorprendente del trabajo fue la capacidad de convertir una ecuación matemática directamente en un programa funcional. Los investigadores tomaron una ecuación formal que describía el comportamiento de un núcleo, escrita en una notación matemática estándar, y la introdujeron en una herramienta que la convirtió en código OCaml. Este código fue luego compilado y ejecutado. El programa resultante se comportó exactamente como la ecuación describía, coincidiendo con la salida del modelo original de Python en cada instancia. Este proceso mostró que una descripción matemática de alto nivel puede transformarse en un binario ejecutable verificado sin perder su significado. El equipo demostró que la versión compilada de esta ecuación cumplía con la mayoría de sus contratos de seguridad, aunque algunos de los pasos lógicos más complejos requirieron un mayor refinamiento en las herramientas de comprobación.

Los hallazgos de este trabajo sugieren un nuevo camino para construir software fiable. Al mantener el código fuente de alto nivel y verificar tanto su significado lógico como su forma compilada, los investigadores crearon un sistema donde la seguridad del programa final está respaldada por una prueba matemática. El método identificó con éxito limitaciones del mundo real en cómo las computadoras manejan los números, como el desbordamiento de enteros, y las distinguió de errores reales. Si bien el sistema no probó cada una de las reglas de seguridad para las partes más complejas del núcleo, probó la gran mayoría, y las que quedaron abiertas fueron identificadas claramente como áreas donde las herramientas de comprobación, más que el código en sí, necesitaban mejorar. El trabajo se presenta como una demostración de que es posible poseer el proceso de traducción desde el código de alto nivel hasta las instrucciones de máquina, asegurando que el ejecutable final lleve un certificado de seguridad que sea tan riguroso como la lógica que lo creó.