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

Resumo Técnico: Do Rocq ao Metal

Problema
A proliferação de Grandes Modelos de Linguagem (LLMs) reduziu drasticamente o custo da geração de código, criando um gargalo crítico em sistemas embarcados de segurança crítica, onde a revisão de código não consegue escalar para acompanhar o volume de firmware gerado. A verificação formal oferece uma solução ao provar matematicamente invariantes, mas os pipelines de extração padrão de provadores de teoremas (como o Rocq) para alvos embarcados falham devido a restrições de hardware. Os runtimes existentes para linguagens como Lean 4, OCaml ou mesmo o Scheme padrão são grandes demais, dependem de mecanismos de coleta de lixo (garbage collection) incompatíveis com RAM limitada (ex: 50 KB no ST33J2M0) ou exigem ambientes hospedados (suporte a OS, libc) que não existem em microcontroladores bare-metal. Consequentemente, desenvolvedores recorrem frequentemente à tradução manual ou extensões de linguagem hospedeira, sacrificando o rigor e a composicionalidade das especificações formais.

Metodologia
Os autores propõem um pipeline completo de ponta a ponta, o Encore!, projetado para executar lógica formalmente verificada diretamente em microcontroladores com recursos limitados (especificamente o Cortex-M35P). A metodologia baseia-se em três pilares:

1. Modelo Arquitetural: O firmware é estruturado como uma função pura de transição de estado: step : State × Event → State × (list Effect).

   • O Estado representa a lógica da aplicação.
   • O Evento representa entradas (ex: pacotes USB, pressões de botões).
   • O Efeito descreve efeitos colaterais (ex: I/O, display) a serem interpretados pelo hospedeiro.
   • Esta separação garante que a lógica central de negócio seja uma função pura provável no Rocq, enquanto a Base de Confiança Confiável (TCB) não verificada — consistindo no poller de eventos e no intérprete de efeitos — permanece constante em tamanho, independentemente da complexidade da aplicação.

2. Seleção de Alvo de Extração: Os autores avaliaram múltiplos caminhos de extração (Lean 4, OCaml, CertiRocq, Scheme). Eles determinaram que o Scheme é o único alvo viável porque carece de requisitos obrigatórios de coleta de lixo e possui uma semântica compacta. No entanto, implementações padrão de Scheme (como Chibi ou Ribbit) foram identificadas como capazes de exceder orçamentos de flash ou falhar ao suportar as macros específicas geradas pela extração do Rocq (ex: quasiquote).

3. A VM e o Compilador Encore!:

   • O Encore! é uma máquina virtual em Rust, no_std, que executa bytecode em Estilo de Passagem de Continuação (CPS).
   • Utiliza uma arquitetura baseada em registradores com 256 registradores e sem pilha de chamadas, eliminando o fluxo de controle oculto e simplificando a coleta de lixo (GC).
   • O GC é um algoritmo de marca-compactação que trata todos os registradores ativos como raízes, evitando a varredura de pilha ilimitada.
   • O pipeline do compilador transforma o Scheme extraído do Rocq em um IR de Estilo Direto, descura (uncurries) aplicações, converte para CPS com índices de De Bruijn, otimiza e compila para bytecode.
   • A interface hospedeira utiliza macros procedurais para gerar bindings tipados entre os tipos Rust do hospedeiro e as tags de construtor da VM, garantindo uma ponte verificada.

Principais Contribuições

1. Demonstração de Execução: O artigo demonstra que o código extraído do Rocq pode ser executado com sucesso em microcontroladores Cortex-M ao selecionar o Scheme como alvo de extração e construir um runtime dedicado para bare-metal.
2. Implementação do Encore!: Os autores apresentam o Encore!, uma VM de bytecode CPS em Rust, no_std, que se ajusta ao orçamento de recursos do hardware da classe ST33 (especificamente a restrição de 50 KB de RAM do ST33J2M0) e executa o Scheme extraído do Rocq de ponta a ponta.
3. Arquitetura Verificada: Eles introduzem uma arquitetura de firmware onde a lógica de negócio é uma função pura de transição de estado. Isso permite que o núcleo seja totalmente provável no Rocq enquanto mantém o tamanho da TCB não verificada constante, desacoplando o esforço de verificação da complexidade do hardware.

Resultos Experimentais
Os autores validaram sua abordagem em uma aplicação de assinatura de transações do Ledger Flex e compararam o Encore! com o CertiRocq (o outro candidato viável) através de sete benchmarks (aritmética, FSM, árvores Red-Black) no QEMU e em hardware físico.

• Viabilidade: Entre todos os caminhos de extração, apenas o Encore! e o CertiRocq foram candidatos viáveis. No entanto, o CertiRocq exigiu modificações cirúrgicas em seu runtime para funcionar em bare metal e falhou em cargas de trabalho de alocação dinâmica.
• Uso de Recursos:
  • Flash: O CertiRocq produz binários menores para aritmética simples (5–6× menores) devido à compilação direta para assembly, mas escala mal (146 KB para rbtree-100) porque faz o inline da construção de listas. O Encore! mantém uma pegada constante (~18 KB) pois a construção é tratada em tempo de execução.
  • Heap: O Encore! supera significativamente o CertiRocq no uso de memória. O uso de naturais de Peano para aritmética no CertiRocq causa um inchaço massivo no heap (ex: exigindo ~63 KB para rbtree-100, excedendo o limite de 50 KB de RAM), enquanto o GC de marca-compactação do Encore! mantém os requisitos baixos (ex: 3.7 KB).
  • Tempo de Build: O Encore! constrói 1.3–2.6× mais rápido em casos simples e até 665× mais rápido em casos complexos (rbtree-100), pois evita as pesadas etapas de geração de código C e otimização exigidas pelo CertiRocq.
• Validação no Mundo Real: A aplicação de assinatura de transações, consistindo em ~400 linhas de lógica Gallina verificada e ~575 linhas de código Rust hospedeiro não verificado, foi implantada com sucesso no hardware físico Ledger Flex. Ela processa, exibe e assina dados corretamente, com propriedades como "nenhum byte perdido durante o parsing" e "validade ASCII" verificadas por máquina.

Significância
O artigo afirma que firmware formalmente verificado é alcançável hoje em bare metal sem sacrificar o rigor da linguagem de especificação. Ao estruturar o firmware como uma função pura de transição de estado, a abordagem permite que o núcleo verificado escale com a complexidade da aplicação enquanto a fronteira não verificada permanece fixa. Esta arquitetura é particularmente significativa na era dos LLMs: ela permite um fluxo de trabalho onde o código gerado por IA pode ser automaticamente verificado via prova de teoremas, substituindo a revisão manual de código pela revisão de provas verificáveis por máquina. Os autores concluem que, embora ainda reste engenharia (como verificar as passagens do compilador e a própria VM), a barreira fundamental de executar lógica provada em alvos embarcados restritos foi superada.