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

Sintesi Tecnica: Da Rocq al Metal

Problematica
La proliferazione dei Large Language Models (LLM) ha ridotto drasticamente il costo della generazione di codice, creando un collo di bottiglia critico nei sistemi embedded critici per la sicurezza, dove la revisione del codice non può scalare per eguagliare il volume del firmware generato. Sebbene la verifica formale offra una soluzione attraverso la prova matematica degli invarianti, le pipeline di estrazione standard dai theorem prover (come Rocq) verso i target embedded falliscono a causa dei vincoli hardware. I runtime esistenti per linguaggi come Lean 4, OCaml o anche lo standard Scheme sono troppo grandi, si affidano a meccanismi di garbage collection incompatibili con la RAM limitata (ad es. 50 KB su ST33J2M0), o richiedono ambienti ospitati (supporto OS, libc) che non esistono sui microcontrollori bare-metal. Di conseguenza, gli sviluppatori ricorrono spesso alla traduzione manuale o all'estensione del linguaggio host, sacrificando il rigore e la compositività delle specifiche formali.

Metodologia
Gli autori propongono una pipeline completa end-to-end, Encore!, progettata per eseguire logica formalmente verificata direttamente su microcontrollori con risorse limitate (specificamente Cortex-M35P). La metodologia si basa su tre pilastri:

1. Modello Architetturale: Il firmware è strutturato come una funzione pura di transizione di stato: step : State × Event → State × (list Effect).

   • Lo State rappresenta la logica applicativa.
   • L'Event rappresenta gli input (ad es. pacchetti USB, pressione di tasti).
   • L'Effect descrive gli effetti collaterali (ad es. I/O, display) da essere interpretati dall'host.
   • Questa separazione garantisce che la logica di business centrale sia una funzione pura dimostrabile in Rocq, mentre il Trusted Computing Base (TCB) non verificato — costituito dal poller degli eventi e dall'interprete degli effetti — rimane costante in termini di dimensioni indipendentemente dalla complessità dell'applicazione.

2. Selezione del Target di Estrazione: Gli autori hanno valutato molteplici percorsi di estrazione (Lean 4, OCaml, CertiRocq, Scheme). Hanno determinato che Scheme è l'unico target vitale perché non presenta requisiti obbligatori di garbage collection e possiede una semantica compatta. Tuttavia, le implementazioni standard di Scheme (come Chibi o Ribbit) sono risultate o troppo ingombranti per il budget di flash o incapaci di supportare le macro specifiche generate dall'estrazione di Rocq (ad es. quasiquote).

3. La VM e il Compilatore Encore!:

   • Encore! è una macchina virtuale bare-metal, no_std in Rust, che esegue bytecode in stile CPS (Continuation Passing Style).
   • Utilizza un'architettura basata su registri con 256 registri e nessun call stack, eliminando il controllo di flusso nascosto e semplificando la garbage collection (GC).
   • La GC è un algoritmo mark-compact che tratta tutti i registri attivi come root, evitando lo scanning incontrollato dello stack.
   • La pipeline del compilatore trasforma lo Scheme estratto da Rocq in un IR in Direct-Style, uncurries le applicazioni, converte in CPS con indici di De Bruijn, ottimizza e compila in bytecode.
   • L'interfaccia host utilizza macro procedurali per generare binding type-safe tra i tipi Rust dell'host e i tag dei costruttori della VM, garantendo un ponte verificato.

Contributi Chiave

1. Dimostrazione di Esecuzione: Il documento dimostra che il codice estratto da Rocq può essere eseguito con successo su microcontrollori Cortex-M selezionando Scheme come target di estrazione e costruendo un runtime bare-metal dedicato.
2. Implementazione di Encore!: Gli autori presentano Encore!, una VM in bytecode CPS no_std in Rust che rientra nel budget di risorse di hardware di classe ST33 (specificamente il vincolo di 50 KB di RAM dello ST33J2M0) ed esegue lo Scheme estratto da Rocq end-to-end.
3. Architettura Verificata: Introducono un'architettura firmware in cui la logica di business è una funzione pura di transizione di stato. Ciò consente al nucleo centrale di essere pienamente dimostrabile in Rocq mantenendo costante la dimensione del TCB non verificato, disaccoppiando lo sforzo di verifica dalla complessità dell'hardware.

Risultati Sperimentali
Gli autori hanno validato il loro approccio su un'applicazione di firma di transazioni per Ledger Flex e hanno confrontato Encore! con CertiRocq (l'altro candidato vitale) attraverso sette benchmark (aritmetica, FSM, alberi Red-Black) su QEMU e hardware fisico.

• Fattibilità: Tra tutti i percorsi di estrazione, solo Encore! e CertiRocq erano candidati vitali. Tuttavia, CertiRocq richiedeva modifiche chirurgiche al proprio runtime per funzionare su bare metal e falliva su carichi di lavoro con allocazione dinamica.
• Utilizzo delle Risorse:
  • Flash: CertiRocq produce binari più piccoli per l'aritmetica semplice (5–6× più piccoli) grazie alla compilazione diretta in assembly, ma scala male (146 KB per rbtree-100) perché inlinea la costruzione delle liste. Encore! mantiene un footprint costante (~18 KB) poiché la costruzione è gestita a runtime.
  • Heap: Encore! supera significativamente CertiRocq nell'uso della memoria. L'uso di naturali di Peano per l'aritmetica in CertiRocq causa un enorme bloat dell'heap (ad es. richiedendo ~63 KB per rbtree-100, superando il limite di 50 KB di RAM), mentre la GC mark-compact di Encore! mantiene i requisiti bassi (ad es. 3.7 KB).
• Tempo di Build: Encore! builda da 1.3 a 2.6 volte più velocemente nei casi semplici e fino a 665 volte più velocemente nei casi complessi (rbtree-100) perché evita i pesanti passaggi di generazione e ottimizzazione del codice C richiesti da CertiRocq.
• Validazione nel Mondo Reale: L'app di firma di transazioni, composta da circa 400 righe di logica Gallina verificata e circa 575 righe di codice host Rust non verificato, è stata distribuita con successo sull'hardware fisico Ledger Flex. Essa analizza, visualizza e firma correttamente i dati, con proprietà come "nessun byte perso durante il parsing" e "validità ASCII" verificate tramite macchina.

Significatività
Il paper sostiene che il firmware formalmente verificato è ottenibile oggi su bare metal senza sacrificare il rigore del linguaggio di specifica. Strutturando il firmware come una funzione pura di transizione di stato, l'approccio permette al nucleo verificato di scalare con la complessità dell'applicazione mentre il confine non verificato rimane fisso. Questa architettura è particolarmente significativa nell'era degli LLM: consente un workflow in cui il codice generato dall'IA può essere automaticamente verificato tramite theorem proving, sostituendo la revisione manuale del codice con la revisione di prove verificabili dalla macchina. Gli autori concludono che, sebbene rimanga del lavoro ingegneristico (come la verifica dei passaggi del compilatore e della VM stessa), l'ostacolo fondamentale di eseguire logica provata su target embedded vincolati è stato superato.