Lean comprovou a correção do programa, mas um bug foi encontrado dentro dele

• Ao fazer fuzzing em uma implementação de zlib formalmente verificada, foi encontrado um heap buffer overflow em lean_alloc_sarray do runtime do Lean 4
• Após mais de 100 milhões de testes com o fuzzer de IA Claude, AFL++ e AddressSanitizer, foram confirmados 4 crashes e 1 vulnerabilidade de memória
• Os problemas encontrados se dividem em dois tipos: overflow no runtime e negação de serviço (DoS) baseada em Out-of-Memory em Archive.lean
• Os algoritmos verificados de compressão e descompressão eram seguros, mas havia vulnerabilidades no parser de arquivo não verificado e na camada de runtime
• Em resumo, a verificação formal é poderosa, mas sem garantir a segurança da Trusted Computing Base (TCB), não é possível assegurar a estabilidade de todo o sistema

---

Bug encontrado em um programa aprovado pela verificação do Lean

• Ao fazer fuzzing em uma implementação de zlib formalmente verificada com Lean, foi encontrado um heap buffer overflow no runtime do Lean 4
  • Não havia vulnerabilidades de memória no código verificado da aplicação
  • Porém, ocorreu um overflow na função lean_alloc_sarray do runtime do Lean, afetando todas as versões do Lean 4
• Foram executadas mais de 100 milhões de rodadas de fuzzing com o fuzzer baseado em IA Claude, AFL++, AddressSanitizer, Valgrind, UBSan e outros
  • Foram executados 16 fuzzers em paralelo sobre 6 superfícies de ataque, incluindo compressão, descompressão e processamento de arquivos em lean-zip
  • Em 19 horas, foram encontrados 4 inputs que causavam crash e 1 vulnerabilidade de memória
• Dois bugs principais foram confirmados
  • Heap buffer overflow em lean_alloc_sarray do runtime do Lean
  • Negação de serviço (DoS) baseada em Out-of-Memory no módulo Archive.lean de lean-zip
• Ficou evidente o limite da verificação formal
  • Os algoritmos de compressão e descompressão de lean-zip foram totalmente verificados, mas o parser de arquivo (Archive.lean) não foi verificado, deixando uma vulnerabilidade de DoS
  • O bug de runtime é um problema dentro da Trusted Computing Base, afetando todos os programas em Lean
• Em conclusão, a verificação formal do Lean comprovou a estabilidade do código da aplicação, mas componentes fora do escopo da verificação ainda podem conter vulnerabilidades
  • A verificação só é forte dentro do escopo em que foi aplicada, e garantir a segurança da camada básica de confiança é essencial

---

Visão geral do experimento de fuzzing

• O codebase alvo foi a implementação verificada de zlib em lean-zip
  • Todos os teoremas (theorem), especificações (specification), documentação e bindings de C FFI foram removidos para deixar apenas código Lean puro
  • O Claude foi impedido de saber que o código era verificado, para evitar viés

• Ambiente de experimento

  • 16 fuzzers em paralelo foram executados sobre 6 superfícies de ataque: ZIP, gzip, DEFLATE, tar, tar.gz e compression
  • Também foram usados AddressSanitizer, UndefinedBehaviorSanitizer, Valgrind memcheck, cppcheck e flawfinder
  • Incluindo 48 arquivos de exploit criados manualmente, foram feitas 105.823.818 execuções no total, com 359 arquivos seed
  • Em 19 horas, foram encontrados 4 inputs com crash e 1 vulnerabilidade de memória

  ---

Bug 1: heap buffer overflow no runtime do Lean

• Função vulnerável: lean_alloc_sarray
  • Função que aloca todos os arrays escalares, como ByteArray e FloatArray
  • Pode ocorrer integer overflow no cálculo sizeof(lean_sarray_object) + elem_size * capacity

• Causa do problema

  • Quando capacity se aproxima de SIZE_MAX, a soma sofre overflow e um buffer pequeno é alocado
  • Depois disso, o chamador lê n bytes, causando heap buffer overflow

• Condições de gatilho

  • Ocorre quando nbytes em lean_io_prim_handle_read tem um valor extremamente grande
  • Pode ser reproduzido com um arquivo de 156 bytes cujo cabeçalho ZIP64 define compressedSize como 0xFFFFFFFFFFFFFFFF
  • Afeta todas as versões do Lean 4, incluindo a nightly mais recente
  • Exemplo de código para reprodução

  def main : IO Unit := do
    IO.FS.writeFile "test.bin" "hello"
    let h ← IO.FS.Handle.mk "test.bin" .read
    let n : USize := (0 : USize) - (1 : USize)
    let _ ← h.read n
  

  • Ao executar o código acima, ocorre overflow em lean_alloc_sarray
  • Um PR de correção já foi enviado

  ---

Bug 2: negação de serviço (DoS) no parser de arquivo do lean-zip

• Função vulnerável: readExact (Archive.lean)
  • Usa o campo compressedSize do diretório central ZIP sem validação
  • Ao chamar h.read, solicita um tamanho anormalmente grande, causando alocação excessiva de memória e OOM

• Reprodução do problema

  • Se um arquivo ZIP de 156 bytes alegar ter tamanho de vários exabytes, o processo termina com INTERNAL PANIC: out of memory
  • O unzip do sistema valida o tamanho do cabeçalho, mas lean-zip não faz essa verificação

  ---

O que a verificação formal deixou passar

• Causa da vulnerabilidade de DoS

  • O módulo Archive.lean está fora da área verificada
  • O pipeline de compressão e descompressão (por exemplo, DEFLATE, Huffman, CRC32) foi totalmente verificado e não apresentou problemas
  • A vulnerabilidade surgiu em uma parte à qual a verificação não foi aplicada

• A essência do overflow no runtime

  • O runtime do Lean faz parte da Trusted Computing Base (TCB)
  • Todas as provas em Lean assumem a correção do runtime
  • Portanto, um bug no runtime afeta a segurança de todos os programas em Lean

  ---

Estabilidade do código verificado

• Resultado de 105 milhões de execuções

  • No código C gerado pelo Lean, não foram encontrados heap overflow, use-after-free, stack overflow, UB nem acesso fora dos limites de arrays
  • Segundo a avaliação do Claude, ele foi analisado como “uma das codebases mais seguras em memória”

• Efeito do sistema de tipos do Lean

  • Com dependent types e uma estrutura de recursão well-founded, ele bloqueia estruturalmente classes de vulnerabilidades (classes de CVE) comuns em implementações de zlib em C/C++

• Conclusão

  • A área de código verificada foi muito robusta, e o fuzzer teve dificuldade para encontrar erros
  • Porém, ainda existiam vulnerabilidades em partes não verificadas e na camada de runtime
  • A verificação é limitada pelo escopo em que foi aplicada e pela segurança da base de confiança

  ---

Lição principal

• A verificação formal é extremamente poderosa dentro da área de código à qual foi aplicada, mas componentes periféricos não verificados ou a camada de runtime ainda podem ameaçar a estabilidade do sistema inteiro
• Garantir a segurança da Trusted Computing Base é essencial e, mesmo em sistemas verificados, permanece a pergunta: “quem vigia os vigilantes? (Quis custodiet ipsos custodes)”

---

Links de referência

• lean-zip on GitHub
• Relatório de bug do Lean 4
• PR de correção do Lean 4 #13392

[GN⁺]

Comentários do Hacker News

• O título e o enquadramento deste texto pareceram um pouco estranhos
  Na prática, o autor deixa claro que não conseguiu encontrar bugs ou erros dentro do código comprovado
  Os dois bugs encontrados estavam fora do escopo da prova: um era uma omissão na especificação e o outro um heap overflow no runtime de C++
  Quero destacar que o bug foi encontrado no runtime do Lean, e não no kernel que faz a verificação
  Veja a documentação do Lean

  • Ao discutir bugs em um sistema verificado, acho que é preciso considerar o binário inteiro
    Se você perde bitcoins por causa de um buffer overflow, não é um consolo saber que o bug estava no runtime
    E, se o programa trava, a maioria dos usuários vai considerar isso um bug
    Também deve haver bastante gente rodando Lean em produção de verdade
  • Só pelo título, pensei que havia um bug no kernel do Lean, mas na realidade os problemas foram encontrados no runtime do Lean e no lean-zip
    Se não foi no kernel, isso não afeta muito a confiabilidade da prova em si
  • A omissão na especificação do lean-zip é um problema importante do ponto de vista da filosofia de verificação
    Mesmo ao verificar um programa “Hello world”, é preciso especificar não só a saída, mas também os efeitos colaterais
    Se houver corrupção de memória na fronteira entre o runtime e o kernel, a confiabilidade da prova pode cair
    No fim, o ponto central é definir claramente “o que deve ser verificado”
  • Ao ver a lista de posts deste site, achei engraçado como ele está ficando cada vez mais clickbait
    Lista de posts relacionados
  • Chamar um bug no runtime do Lean de bug no lean-zip é como chamar um bug na JRE de bug em um app Java
    Parece que o autor tentou induzir mal-entendidos de propósito

• Eu também tive uma experiência parecida com código provado
  No meu caso, o problema não foi overflow, mas sim um bug de especificação (spec bug)
  Se a especificação estiver errada, código e prova podem ser perfeitos e ainda assim funcionar diferente do comportamento pretendido
  No fim das contas, a dificuldade da verificação está em expressar com precisão a intenção humana
  A crença de que a IA vai resolver verificação perfeitamente pode gerar uma falsa confiança

  • Também tive uma experiência semelhante
    Especificações demonstráveis com ferramentas como Lean, TLA+ e Z3 são simplificadas e exigem muitas suposições
    Mesmo assim, isso continua sendo uma ferramenta poderosa
    Ela ajuda a reduzir bugs em algoritmos complexos e a enxergar com clareza os limites da especificação
    Graças à IA, esse tipo de trabalho de prova ficou muito mais fácil
  • A dúvida que sempre surge é: “como podemos confiar no próprio sistema de verificação?”
    Outro programa que verifica um programa também pode ter bugs
    A impossibilidade de autoverificação completa faz lembrar o princípio da incerteza de Heisenberg
    No fim, verificação é um processo de aumentar a confiança por meio de uma “segunda implementação independente”
  • Os bugs no meu código se dividem em dois tipos
    (1) quando ele funciona diferente do pretendido
    (2) quando ele funciona como pretendido, mas a intenção estava errada
    Assistentes de prova impedem o tipo (1), mas não o tipo (2)
    Ou seja, não dá para provar a solidez do design
    Verificar tudo, como no seL4, custa caro demais e leva tempo demais
  • Acho que precisamos de um jeito de verificar a própria especificação
    O ideal seria combinar lógica formal + pensamento adversarial (adversarial thinking) para listar de forma completa o que o programa deve fazer e o que não deve fazer

• O título pareceu clickbait
  Não havia bug na parte provada, então não entendi por que foi escrito assim
  No HN, eu queria ver posts baseados em fatos, e isso foi perda de tempo

  • Em software verificado, é justo dizer que “só bugs que violam a prova contam como bug”?
    Anuncia-se “sem bugs”, mas na prática isso vale apenas “dentro do escopo em que a especificação foi expressa perfeitamente”
    Mesmo estando perfeitamente certo, no mundo real você pode estar certo e morto — ou seja, teoricamente correto, mas quebrado na prática
  • O título é tecnicamente correto, mas descreve um problema no código não verificado do lean-zip como se fosse um bug na parte provada
  • No fim, a mensagem “deixe claro o escopo da parte provada” é interessante e válida
  • O segundo bug parece inventado sem base
    Não há referência de código e, olhando o código real, dá para ver que foi um mal-entendido
  • No fim das contas, lean-zip é apenas um binding do Zlib

• Esse problema aparece com frequência também na verificação de sistemas distribuídos
  A prova só vale dentro de certas condições (faixa operacional), e as falhas interessantes acontecem justamente na fronteira
  Com TLA+ é a mesma coisa: se a realidade sai das suposições, a prova perde o sentido
  O que eu quero é uma forma de declarar mecanicamente a faixa operacional e monitorá-la em runtime

  • Eu mesmo já encontrei um bug de hardware de CPU
    Mas a maioria dos bugs não vem do hardware, e sim de gente que não lê a documentação
    Só a modelagem formal já consegue reduzir absurdamente a quantidade de bugs

• Esta é uma boa notícia previsível
  Significa que LLMs conseguem criar código que passa por verificação formal
  Daqui para frente, os bugs vão migrar cada vez mais para a camada de hardware
  No fim, vai ser necessário formalizar as especificações de hardware
  Se os fabricantes não divulgarem isso, pode surgir conflito com a comunidade
  No longo prazo, haverá dois caminhos: extinção das vulnerabilidades ou inserção intencional

• No começo, achei que o autor não tinha testado a parte provada
  Mas, lendo melhor, os bugs foram encontrados fora do escopo da prova
  Por isso, o título me pareceu um pouco exagerado

  • O próprio autor do texto aparece na discussão
    Ele argumenta que, se falamos de bug em um sistema verificado, o alvo deve ser o binário inteiro
    E afirma que encontrou uma entrada que causa crash na parte de parsing de cabeçalho compactado em Archive.lean

• Lembrei de uma frase famosa de Donald Knuth
  “Cuidado, pode haver bugs no código acima. Eu apenas provei que ele está correto, não o executei”

• Não ter verificado o parser parece um erro grande
  Parsing de formato binário é sempre uma área perigosa

• O ponto principal é que um agente de IA trabalhou junto com um fuzzer e encontrou um heap buffer overflow em Lean
  Isso é um resultado bem grande

  • Acho que foi uma descoberta realmente útil

• Foi marcante a parte em que Claude disse que “este é um dos codebases mais memory-safe que já analisei”
  Mas isso soou como uma piada de que era o primeiro código que Claude analisava

  • Não faz sentido ser o primeiro código analisado por um Claude amplamente treinado com RL
    É justamente por isso que ele é tão bom nisso
  • Talvez Claude esteja fazendo secretamente alguma coisa que a gente não sabe 😄