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

No mundo do software, existe uma tensão constante entre como escrevemos o código e como sabemos que ele é seguro. Os programadores usam linguagens de alto nível para descrever lógicas complexas de uma forma que seja legível e gerenciável, mas as máquinas que executam esse código falam uma linguagem muito mais simples e rígida. Para ir de um ao outro, os compiladores atuam como tradutores, mas é nesse processo de tradução que os erros costumam se esconder. Um erro na tradução pode transformar uma instrução segura em uma perigosa, fazendo com que um programa trave ou se comporte de maneira imprevisível. Durante décadas, a maneira mais confiável de garantir a segurança tem sido verificar o código de máquina final, mas isso é difícil porque o significado de alto nível do programa original é frequentemente perdido no processo. A questão que os pesquisadores estão fazendo é se podemos manter a clareza da linguagem original de alto nível e, ao mesmo tempo, provar, com absoluta certeza, que as instruções de máquina finais farão exatamente o que pretendemos.

Brent Hartshorn construiu um sistema que responde a essa pergunta ao tratar um único pedaço de código como duas coisas diferentes ao mesmo tempo. Imagine um documento que pode ser lido simultaneamente como uma prova matemática e como um conjunto de instruções para uma máquina. Neste novo trabalho, o autor utiliza um subconjunto de uma linguagem de programação chamada OCaml, conhecida por suas regras estritas sobre como os dados são manipulados, e atribui a cada definição dois significados distintos. Primeiro, o código é lido como um argumento lógico, onde a própria estrutura do programa serve como uma prova de que certas condições serão sempre atendidas. Segundo, o mesmo código é traduzido para uma linguagem diferente chamada Rust, que é projetada para velocidade e segurança, e então compilado em um programa que um computador possa realmente executar. A genialidade da abordagem reside na verificação: a prova lógica é verificada por um pequeno motor matemático confiável, enquanto o programa em execução é verificado contra um interpretador de referência que simula o código passo a passo. Se os dois coincidirem, e se a prova lógica se sustentar, o resultado é um software que vem com seu próprio certificado de segurança.

Os pesquisadores começaram construindo um tradutor que entende um recorte específico de OCaml. Este tradutor, escrito em Python, é pequeno o suficiente para ser lido e compreendido por uma única pessoa, o que é crucial porque, se o próprio tradutor for muito complexo, não podemos confiar em sua saída. Ele pega o código OCaml e o divide em dois caminhos. No caminho da prova, ele converte o código em um formato que um núcleo matemático pode verificar. Este núcleo é um programa minúsculo que atua como um juiz, verificando se a lógica é sólida sem fazer suposições. No caminho do programa, o tradutor converte o código em Rust, uma linguagem que é compilada em código de máquina nativo e rápido. Para garantir que a tradução fosse perfeita, a equipe também construiu um interpretador de referência que executa o código OCaml original diretamente. Eles então rodaram treze programas de exemplo diferentes através tanto da versão Rust compilada quanto do interpretador. Em todos os casos, o código compilado produziu exatamente a mesma saída que o interpretador, provando que o processo de tradução não alterou o comportamento dos programas.

Assim que o código foi traduzido com sucesso, a equipe aplicou uma verificação de segurança rigorosa à versão Rust compilada. Eles trataram o código compilado como um contrato, onde regras específicas sobre como o programa deve se comportar foram escritas como teoremas matemáticos. Por exemplo, eles verificaram se cálculos de inteiros nunca sofreriam um estouro acidental e voltariam para um número negativo, uma fonte comum de bugs em software. Eles descobriram que, embora a maioria dessas regras de segurança fosse verdadeira, havia casos específicos onde as regras eram quebradas. Em onze cenários diferentes, o código compilado atingiu um ponto onde um cálculo de inteiro poderia sofrer um estouramento, como quando se subtrai o menor número possível de zero. O sistema identificou corretamente esses pontos como obrigações abertas, o que significa que o código é seguro em todos os lugares, exceto nesses limites específicos e conhecidos. De um total de noventa verificações de segurança realizadas nos programas de exemplo, setenta e nove foram totalmente provadas, enquanto as onze restantes ficaram abertas porque representavam limites reais e alcançáveis na forma como o computador lida com números.

O projeto foi além, aplicando este método a um pequeno kernel de sistema operacional, uma parte central de software que gerencia recursos do computador. Os pesquisadores pegaram um kernel que havia sido anteriormente escrito em Python e Rust e o reescreveram em seu subconjunto de OCaml. Eles então traduziram esta nova versão para Rust e a compilaram. O resultado foi uma terceira implementação do mesmo kernel. Ao ser testada contra a versão original em Python, a nova versão derivada de OCaml respondeu corretamente em todos os 236 casos de teste. A equipe tentou provar a segurança deste novo kernel. Eles conseguiram provar 227 das 236 obrigações de segurança. As poucas que permaneceram não provadas não eram erros no código, mas sim lacunas nas ferramentas matemáticas usadas para verificá-las, especificamente em relação a como o sistema lida com loops e contadores complexos. Isso demonstrou que o método pode escalar de pequenos exemplos para um componente funcional de um sistema operacional.

Talvez a parte mais impressionante do trabalho tenha sido a capacidade de transformar uma equação matemática diretamente em um programa funcional. Os pesquisadores pegaram uma equação formal que descrevia o comportamento de um kernel, escrita em uma notação matemática padrão, e a inseriram em uma ferramenta que a converteu em código OCaml. Este código foi então compilado e executado. O programa resultante comportou-se exatamente como a equação descrevia, correspondendo à saída do modelo original em Python em todas as instâncias. Este processo mostrou que uma descrição matemática de alto nível pode ser transformada em um binário executável verificado sem perder seu significado. A equipe provou que a versão compilada desta equação satisfazia a maioria de seus contratos de segurança, embora alguns dos passos lógicos mais complexos tenham exigido refinamento adicional nas ferramentas de verificação.

As descobertas deste trabalho sugerem um novo caminho para a construção de software confiável. Ao manter o código-fonte de alto nível e verificar tanto seu significado lógico quanto sua forma compilada, os pesquisadores criaram um sistema onde a segurança do programa final é respaldada por uma prova matemática. O método identificou com sucesso limitações do mundo real na forma como os computadores lidam com números, como o estouro de inteiros, e distinguiu-os de bugs reais. Embora o sistema não tenha provado cada regra de segurança para as partes mais complexas do kernel, ele provou a grande maioria, e as que permaneceram abertas foram claramente identificadas como áreas onde as ferramentas de verificação, e não o código em si, precisavam de melhorias. O trabalho serve como uma demonstração de que é possível deter o controle do processo de tradução do código de alto nível para as instruções de máquina, garantindo que o executável final carregue um certificado de segurança tão rigoroso quanto a lógica que o criou.