From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware

Resumen Técnico: De Rocq al Metal

Planteamiento del Problema
La proliferación de los Modelos de Lenguaje de Gran Escala (LLMs) ha reducido drásticamente el coste de la generación de código, creando un cuello de botella crítico en sistemas embebidos de seguridad crítica donde la revisión de código no puede escalar para igualar el volumen de firmware generado. La verificación formal ofrece una solución mediante la demostración matemática de invariantes, pero las canalizaciones de extracción estándar desde demostradores de teoremas (como Rocq) hacia objetivos embebidos fallan debido a las restricciones de hardware. Los entornos de ejecución existentes para lenguajes como Lean 4, OCaml o incluso Scheme estándar son demasiado grandes, dependen de mecanismos de recolección de basura incompatibles con la RAM limitada (por ejemplo, 50 KB en ST33J2M0), o requieren entornos alojados (soporte de OS, libc) que no existen en microcontroladores bare-metal. En consecuencia, los desarrolladores suelen recurrir a la traducción manual o a extensiones del lenguaje anfitrión, sacrificando el rigor y la composibilidad de las especificaciones formales.

Metodología
Los autores proponen una canalización completa de extremo a extremo, Encore!, diseñada para ejecutar lógica formalmente verificada directamente en microcontroladores con recursos limitados (específicamente Cortex-M35P). La metodología se basa en tres pilares:

1. Modelo Arquitectónico: El firmware se estructura como una función pura de transición de estado: step : State × Event → State × (list Effect).

   • El Estado representa la lógica de la aplicación.
   • El Evento representa las entradas (por ejemplo, paquetes USB, pulsaciones de botones).
   • El Efecto describe los efectos secundarios (por ejemplo, E/S, pantalla) para ser interpretados por el anfitrión.
   • Esta separación asegura que la lógica de negocio central sea una función pura demostrable en Rocq, mientras que la Base de Computación Confiable (TCB) no verificada —que consiste en el rastreador de eventos y el intérprete de efectos— mantiene un tamaño constante independientemente de la complejidad de la aplicación.

2. Selección del Objetivo de Extracción: Los autores evaluaron múltiples rutas de extracción (Lean 4, OCaml, CertiRocq, Scheme). Determinaron que Scheme es el único objetivo viable porque carece de requisitos obligatorios de recolección de basura y posee una semántica compacta. Sin embargo, se descubrió que las implementaciones de Scheme estándar (como Chibi o Ribbit) o bien excedían los presupuestos de flash o fallaban al no soportar las macros específicas generadas por la extracción de Rocq (por ejemplo, quasiquote).

3. La VM y el Compilador de Encore!:

   • Encore! es una máquina virtual en Rust, no_std, que ejecuta bytecode de Estilo de Paso de Continuación (CPS).
   • Utiliza una arquitectura basada en registros con 256 registros y sin pila de llamadas, eliminando el flujo de control oculto y simplificando la recolección de basura (GC).
   • El GC es un algoritmo de marcado-compactación (mark-compact) que trata todos los registros activos como raíces, evitando el escaneo ilimitado de la pila.
   • La canalización del compilador transforma el Scheme extraído de Rocq en un IR de Estilo Directo, desencurla las aplicaciones, las convierte a CPS con índices de De Bruijn, optimiza y compila a bytecode.
   • La interfaz del anfitrión utiliza macros de procedimiento para generar enlaces de tipos seguros entre los tipos de Rust del anfitrión y las etiquetas de constructor de la VM, asegurando un puente verificado.

Contribuciones Clave

1. Demostración de Ejecución: El artículo demuestra que el código extraído de Rocq puede ejecutarse con éxito en microcontroladores Cortex-M mediante la selección de Scheme como objetivo de extracción y la construcción de un entorno de ejecución (runtime) diseñado específicamente para bare-metal.
2. Implementación de Encore!: Los autores presentan Encore!, una VM de bytecode CPS en Rust, no_std, que se ajusta al presupuesto de recursos del hardware de clase ST33 (específicamente la restricción de 50 KB de RAM del ST33J2M0) y ejecuta Scheme extraído de Rocq de extremo a extremo.
3. Arquitectura Verificada: Introducen una arquitectura de firmware donde la lógica de negocio es una función pura de transición de estado. Esto permite que el núcleo sea totalmente demostrable en Rocq mientras mantiene el tamaño de la TCB no verificada constante, desacoplando el esfuerzo de verificación de la complejidad del hardware.

Resultos Experimentales
Los autores validaron su enfoque en una aplicación de firma de transacciones de Ledger Flex y compararon Encore! contra CertiRocq (el otro candidato viable) a través de siete benchmarks (aritmética, FSM, árboles Red-Black) en QEMU y hardware físico.

• Viabilidad: Entre todas las rutas de extracción, solo Encore! y CertiRocq fueron candidatos viables. Sin embargo, CertiRocq requirió modificaciones quirúrgicas en su runtime para funcionar en bare-metal y falló en cargas de trabajo de asignación dinámica.
• Uso de Recursos:
  • Flash: CertiRocq produce binarios más pequeños para aritmética simple (5–6× más pequeños) debido a la compilación directa a ensamblador, pero escala mal (146 KB para rbtree-100) porque realiza inline de la construcción de listas. Encore! mantiene una huella constante (~18 KB) ya que la construcción se gestiona en tiempo de ejecución.
  • Heap: Encore! supera significativamente a CertiRocq en el uso de memoria. El uso de naturales de Peano para la aritmética en CertiRocq causa una enorme expansión del heap (por ejemplo, requiriendo ~63 KB para rbtree-100, excediendo el límite de 50 KB de RAM), mientras que el GC de marcado-compactación de Encore! mantiene los requisitos bajos (por ejemplo, 3.7 KB).
  • Tiempo de Construcción: Encore! construye de 1.3 a 2.6× más rápido en casos simples y hasta 665× más rápido en casos complejos (rbtree-100) porque evita los pesados pasos de generación de código C y optimización requeridos por CertiRocq.
• Validación en el Mundo Real: La aplicación de firma de transacciones, que consta de ~400 líneas de lógica Gallina verificada y ~575 líneas de código Rust anfitrión no verificado, se desplegó con éxito en el hardware físico de Ledger Flex. Parsea, muestra y firma datos correctamente, con propiedades como "ningún byte perdido durante el parseo" y "validez ASCII" verificadas mediante máquina.

Significancia
El artículo sostiene que el firmware formalmente verificado es alcanzable hoy en día en bare-metal sin sacrificar el rigor del lenguaje de especificación. Al estructurar el firmware como una función pura de transición de estado, el enfoque permite que el núcleo verificado escale con la complejidad de la aplicación mientras que el límite no verificado permanece fijo. Esta arquitectura es particularmente significativa en la era de los LLM: permite un flujo de trabajo donde el código generado por IA puede ser verificado automáticamente mediante la demostración de teoremas, reemplazando la revisión manual de código por la revisión de pruebas verificables por máquina. Los autores concluyen que, si bien queda trabajo de ingeniería (como verificar las pasadas del compilador y la propia VM), la barrera fundamental de ejecutar lógica probada en objetivos embebidos con recursos limitados ha sido superada.