Traduzindo os crates core e alloc do Rust para Coq para verificação formal

 (formal.land)
1 pontos por GN⁺ 2024-05-16 | 1 comentários | Compartilhar no WhatsApp
  • O coq-of-rust, que transpõe programas Rust para Coq, passou a abranger também os crates core e alloc da biblioteca padrão, reduzindo a carga de escrever manualmente definições em Coq para cada função primitive
  • Como os dois crates são grandes bases de código com muito unsafe e Rust avançado, o desafio central passou a ser tratar a tradução automática em unidades que possam ser compiladas e verificadas
  • Ao dividir a saída por arquivo Rust de entrada, alloc ficou com 54 arquivos e 171.783 linhas, e core com 190 arquivos e 592.065 linhas, facilitando compilação paralela e depuração
  • Os conflitos de nome de módulo em blocos impl foram mitigados com a inclusão de informações da cláusula where, mas ainda restam arquivos que não compilam no Coq, correspondendo a 4% do total
  • O exemplo de Option::unwrap_or_default usa a prova de equivalência entre a definição traduzida automaticamente e uma definição funcional simples, exigindo ao mesmo tempo confiança na automação e checagem no momento da prova

Tratamento de primitives da biblioteca padrão do Rust

  • A Formal Land está desenvolvendo o coq-of-rust, que traduz programas Rust para o sistema de provas formais Coq
  • Antes, para lidar com componentes primitive da biblioteca padrão do Rust, era preciso criar separadamente uma definição em Coq que representasse o comportamento de cada função
  • Para reduzir essa carga, os crates core e alloc do Rust foram traduzidos com coq-of-rust
  • O resultado da tradução pode ser visto nos seguintes caminhos

Resultado da execução inicial da tradução

  • Ao executar coq-of-rust pela primeira vez em alloc e core, foram gerados dois arquivos Coq com centenas de milhares de linhas, cada um correspondente a um crate inteiro
  • Isso confirmou que a ferramenta consegue rodar mesmo em bases de código grandes, mas o código Coq gerado não compilava imediatamente
  • Os erros apareciam com pouca frequência, mas ainda assim na ordem de um a cada alguns milhares de linhas
  • Segundo o cloc, o tamanho do código Rust de entrada era o seguinte
    • alloc: 26.299 linhas de código Rust
    • core: 54.192 linhas de código Rust
  • Como há expansão de macros durante a tradução, o alvo real da tradução é maior que a contagem de linhas original

Divisão do código Coq gerado

  • A maior mudança foi dividir a saída do coq-of-rust em um arquivo Coq para cada arquivo Rust de entrada
  • Isso foi possível porque a tradução é insensível à ordem das definições e context-free
  • Embora normalmente existam dependências circulares entre arquivos Rust, e o Coq não permita isso, essa forma de tradução tornou possível a separação por arquivo
  • Após a divisão, a escala da saída passou a ser a seguinte
    • alloc: 54 arquivos Coq, 171.783 linhas de código Coq
    • core: 190 arquivos Coq, 592.065 linhas de código Coq
  • Com os arquivos divididos, ficou mais fácil explorar e manter o código gerado
    • Mais fácil paralelizar a compilação
    • Possibilidade de depurar com foco em um arquivo por vez
    • Facilidade para excluir arquivos que não compilam
    • Facilidade para acompanhar diffs de arquivos individuais

Correção de conflitos de nome de módulo e arquivos restantes

  • Alguns bugs surgiam de conflitos de nome de módulo em blocos impl
  • A solução foi aumentar a unicidade dos nomes de módulo incluindo mais informações neles
    • Foram incluídas informações da cláusula where, que antes ficavam de fora
    • Por exemplo, na implementação do trait Default para Mapping<K, V>, a condição de que K e V também implementem Default passa a se refletir no nome do módulo
  • No momento, os arquivos que não compilam no Coq são os seguintes
    • alloc/boxed.v
    • core/any.v
    • core/array/mod.v
    • core/cmp/bytewise.v
    • core/error.v
    • core/escape.v
    • core/iter/adapters/flatten.v
    • core/net/ip_addr.v
  • Isso corresponde a 4% do total de arquivos
  • Mesmo entre os arquivos que compilam, ainda há componentes Rust não tratados que foram axiomatizados, então esse percentual sozinho não basta para medir todo o escopo ainda sem suporte

Exemplo de tradução de Option::unwrap_or_default

  • Em Rust, Option::unwrap_or_default retorna x se for Some(x) e chama T::default() se for None
  • O coq-of-rust traduz isso para uma definição em Coq em forma monádica
    • Faz o matching dos argumentos de entrada e dos tipos
    • No ramo Some, obtém e copia o campo da tupla
    • No ramo None, chama o método default do trait core::default::Default
  • Na verificação prática, em vez da definição gerada automaticamente, usa-se uma definição funcional mais simples
    • Se for None, retorna core.simulations.default.Default.default
    • Se for Some x, retorna x
  • A prova de que a definição gerada automaticamente e a definição simples são equivalentes está em CoqOfRust/core/proofs/option.v
  • Se o código Rust original mudar, essa prova captura a alteração
  • Como a tradução da biblioteca core foi feita automaticamente, é possível confiar mais na definição gerada do que em uma definição escrita manualmente
  • Ainda assim, o coq-of-rust pode conter erros ou lacunas, então é preciso verificar na etapa de prova se o código é válido

Desafios restantes

  • A confiança na formalização da biblioteca padrão aumenta a confiabilidade da verificação de programas Rust
  • O próximo objetivo continua sendo simplificar o ainda tedioso processo de prova
  • Em especial, para mostrar que a simulação é equivalente ao código Rust original, ainda são necessárias as seguintes etapas
    • Resolução de nomes
    • Introdução de tipos de alto nível
    • Remoção de efeitos colaterais
  • A direção das próximas melhorias é tratar essas etapas separadamente

Leituras relacionadas

1 comentários

 
GN⁺ 2024-05-16
Comentários do Hacker News

  • Realmente impressionante
    Esse tipo de tradução automática desloca o objeto de confiança para a ferramenta. O próprio coq-of-rust é escrito em Rust, não em Coq, então essa estrutura recursiva é bem surpreendente, mas parece possível provar a correção misturando uma abordagem ao estilo CompCert com a ideia de contornar o ataque Trusting Trust de Ken Thompson usando um segundo compilador, como em “Countering Trusting Trust through Diverse Double-Compiling” (2009), de David A. Wheeler [0]
    Para verificar isso, bastaria converter o tradutor coq-of-rust de Rust para Coq usando o próprio coq-of-rust e, embora essa tradução tenha sido feita em Rust e portanto não precise ser confiável, provar dentro do Coq as propriedades de correção desejadas, em especial que a semântica é preservada ao traduzir programas Rust para Coq
    Como no artigo, provavelmente seria mais fácil provar sobre definições mais funcionais do que as definições geradas, então bastaria seguir um processo como o da biblioteca padrão e provar a equivalência entre as definições. Se o tradutor coq-of-rust atual, especialmente lib/ [1], tem 6.350 linhas de Rust, então também parece viável escrever o tradutor inteiro em Coq e provar que ele é equivalente ao que foi gerado
    Depois disso, se você executar a versão em Coq já provada do tradutor coq-of-rust sobre o código-fonte em Rust do coq-of-rust, as definições em Coq produzidas deverão coincidir com a saída do tradutor coq-of-rust em Rust usado no começo
    Como observação lateral, é bom ver esse tipo de trabalho recebendo financiamento da indústria. Sou cético em relação a cripto, mas é fato que as exigências de correção desse setor acabam impulsionando melhorias em áreas de interesse como Rust, Coq e apoio a estudantes de mestrado que entendem do assunto
    [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf
    [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib

    • Sou um dos autores, e esse procedimento realmente pode ser uma boa forma de verificar o coq-of-rust
      Só que, embora o código em si seja curto, ele depende do compilador Rust para fazer parsing e type checking do código Rust de entrada. Então essa parte também precisaria ser verificada ou, no mínimo, formalmente especificada sem prova. O fato de a API do rustc ser bem grande e instável é um obstáculo, mas ainda assim isso pode ser uma forma de aumentar a confiabilidade
    • Isso me lembra da época em que eu trabalhava com SPARK Ada. Em projetos sem um alvo Ada suportado, especialmente em dispositivos muito pequenos, às vezes convertíamos Ada para C e depois compilávamos para o alvo desejado, o que permitia fazer vários tipos de análise estática do lado do SPARK
      Claro que isso criava a necessidade de verificar o resultado ou o conversor, mas o código C gerado era relativamente fácil de ler para fins de verificação, tinha um estilo restrito, e a confiança nas ferramentas também era alta. A análise estática do SPARK era apenas uma parte de todo o processo de verificação e validação, e testes junto com outras atividades forneciam camadas adicionais de confiança. No geral, era uma abordagem que funcionava bem
    • O motivo de cripto ajudar nesse tipo de coisa não é só a exigência de correção, mas também o fato de que muita riqueza foi transferida para pessoas interessadas em ciência da computação
      Quando elas gastam esse dinheiro em pesquisa em ciência da computação, não é apenas porque isso lhes traz benefício, mas também porque é um tipo de filantropia alinhada aos próprios hobbies
    • Não vejo bem como essa abordagem impediria que o compilador Rust usado para gerar o binário injete uma carga maliciosa. Dá para compilar A com B, depois B com A, e comparar os binários
      Outra abordagem é proof-carrying code: o compilador Rust emitiria junto uma prova em Coq de que a saída executável corresponde à semântica do código-fonte de entrada
      Claro, também daria para escrever um compilador de um subconjunto de Rust, por exemplo sem borrow checker nem otimizações, para código de máquina de uma arquitetura específica, e então fazer todo o bootstrap a partir daí

  • O tamanho dos programas verificados de ponta a ponta com um sistema de prova dedutiva semiautomático como Coq é pequeno. Bibliotecas podem ser mais fáceis, porque o grau de interação entre trechos de código é menor, mas programas em geral não são assim
    De fato, o crescimento do tamanho dos programas que podem ser verificados desse jeito tem sido mais lento do que o crescimento do tamanho médio dos programas como um todo. Verificação de software no sentido forte, isto é, mostrar conformidade de 100% com a especificação, é claramente útil em áreas como prova de correção de algoritmos centrais, mas não escala bem
    Por isso houve certa migração da pesquisa para métodos não sólidos. O custo de uma garantia de 100% pode ser 10 vezes maior do que o de uma garantia de 99,9999%, e essa diferença de probabilidade pode até ser menor do que a probabilidade de falhas não relacionadas ao software. Em sistemas físicos, não dá nem para provar que eles correspondem à especificação, e ainda existe a chance de a própria especificação não refletir adequadamente a realidade

    • O ponto central é que, se você provar as partes unsafe da biblioteca padrão e as garantias de segurança do Rust, então pode provar transitivamente segurança de memória, ausência de data races etc. para todo código Rust seguro que use apenas a biblioteca padrão
      Provar a correção apenas do código unsafe exige muito menos esforço do que provar todo o código Rust. Essa é uma resposta à crítica comum de “mas e o código unsafe?” quando se fala das garantias de segurança do Rust. As lacunas que o sistema de tipos de Rust sozinho não consegue cobrir podem ser preenchidas com um sistema mais forte, como Coq

  • Há uma parte dessas tentativas que não entendo bem. Se for preciso converter o código para Coq manual ou semimanualmente, a chance de cometer erros nesse processo não seria muito maior do que o benefício obtido com a verificação formal?
    Em outras palavras, como sabemos que o que provamos ainda vale para o código original?

    • Não tem como saber. No fim, é preciso confiar em alguma coisa — hardware, compilador, especificação, kernel confiável do Coq etc.
      A verificação formal muitas vezes é discutida como se eliminasse completamente a possibilidade de bugs, mas na prática ela está mais para reduzir muito essa possibilidade. Ainda assim, a tradução automática entre Rust e Coq reduz bastante a complexidade do que precisa ser confiado, então deve ser preferida à tradução manual
    • É uma limitação real, mas não tão ruim assim
      Em muitos casos, um bug na tradução simplesmente torna a prova impossível. Aí alguém vai investigar por que a prova não passa e acaba encontrando o bug de tradução
      O problema de verdade é quando um bug de tradução compensa exatamente um bug do código original. Se não houver um risco sistêmico, é bem improvável que dois bugs se anulem dessa forma
    • O código é traduzido automaticamente com coq-of-rust. Se um problema for encontrado na tradução, basta corrigir uma vez na ferramenta coq-of-rust, e todos os resultados de tradução são atualizados

  • Para os leitores interessados: enviei este post de blog porque ele é menos diretamente relacionado a criptomoedas do que outros posts do mesmo blog, mas há muitos textos tecnicamente mais interessantes por lá
    Em especial, os dois posts mais recentes tratam de aplicar a mesma abordagem não a Rust, mas a Python

  • Lembrei de uma palestra [1] em que um fuzzer encontrou bugs em um compilador C formalmente verificado. Isso aconteceu porque a verificação formal não cobria o frontend nem o backend
    Também sei que surge a pergunta sobre o quanto se pode confiar no próprio Coq ou na tradução, e fica a dúvida de como isso será sincronizado com as atualizações do Rust, mas mesmo uma verificação formal perfeita não significa 100% de correção de ponta a ponta
    [1] https://youtu.be/Ux0YnVEaI6A

  • Não sou especialista em verificação formal de forma alguma, mas se a biblioteca padrão do Rust for formalmente verificada e não usar código unsafe, então todo programa Rust que use bibliotecas formalmente verificadas passaria a ter, do ponto de vista de tratamento de memória, algo como qualidade em nível de verificação formal?

    • A segurança do Rust quase não tem relação com bugs
      Rust tem sua própria definição de “safe”, e isso pode ser visto como um subconjunto de segurança de memória. Mesmo em código Rust totalmente seguro ainda são possíveis corridas de dados, deadlocks, esgotamento de memória e, nem é preciso dizer, erros lógicos
    • Acho que, em certa medida, esse é o sonho, mas há muitas ressalvas e várias coisas precisam se alinhar
      Primeiro, é preciso formalizar a semântica de unsafe Rust. O trabalho pioneiro RustBelt[1], de Ralf Jung, foi um grande avanço, mas ainda não está completo. Em especial, a origem de ponteiros está se revelando um elemento complicado
      Segundo, como parte disso, é necessário um modelo formal do borrow checker. Stacked borrows[2] foi uma boa tentativa, mas tem falhas, e Tree borrows[3] talvez corrija isso, embora também seja possível que surja algo ainda mais sofisticado
      Terceiro, é preciso um modelo formal de memória. Isso trata principalmente do comportamento de operações atômicas e sincronização e, por isso, é muito importante para componentes da biblioteca padrão como Arc. É amplamente aceito que o modelo de memória do Rust deve ser parecido com o do C++ e interoperável com ele, mas ainda restam o problema de “out of thin air” e funcionalidades ausentes como seqlock. Essa é uma das razões pelas quais o kernel Linux ainda usa seu próprio modelo
      Quarto, é preciso provar que as garantias de segurança se compõem bem. Em especial, código correto escrito em unsafe Rust e código safe Rust devem continuar preservando as garantias de segurança quando compostos. Há bons resultados até agora, mas isso precisa ser provado para o sistema inteiro
      Quinto, para que essa prova valha para todo código, é preciso fechar todos os bugs de soundness ainda restantes no Rust[1]. Muitos desses problemas são teóricos ou só importam na prática em código adversarial[5], então o progresso é lento
      Mesmo quando tudo isso estiver resolvido, ainda será só uma garantia parcial. Uma parte enorme da superfície de contato com o sistema se baseia em código unsafe. A menos que você faça apenas computação pura, se estiver criando, por exemplo, uma interface gráfica, ainda haverá muitas coisas que podem dar errado
      Ainda assim, existe um caminho prático de avanço, e ele leva a uma situação muito melhor do que o estado geral atual de sistemas cheios de vulnerabilidades
      [1]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
      [2]: https://plv.mpi-sws.org/rustbelt/stacked-borrows/
      [3]: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html
      [4]: https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao...
      [5]: https://github.com/Speykious/cve-rs
    • Não sou especialista em Rust, mas o código de core parece ter bastante unsafe. O que faz sentido
      https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l...
      Não acho que o Coq, da forma apresentada aqui, consiga verificar todas as chamadas unsafe

  • Dá para comparar como essa abordagem difere do Aeneas ou do RustHornBelt? Como ela lida com ponteiros e empréstimos mutáveis?

    • Não sei como o RustHornBelt funciona. Nós focamos em código seguro, mas também geramos traduções para blocos unsafe em regime de “melhor esforço”.
      Em comparação com o Aeneas, o objetivo é muito parecido. Ambos tentam verificar programas Rust com um provador interativo de teoremas. A diferença é que, no coq-of-rust, escrevemos manualmente uma versão puramente funcional do código a ser provado ou, por ser uma tarefa repetitiva, escrevemos com ajuda do GitHub Copilot, e então provamos que ela é equivalente ao resultado da tradução automática. O objetivo do Aeneas é gerar diretamente a versão funcional.
      Todos os ponteiros são tratados como ponteiros mutáveis, ou seja, como se fossem do tipo *. Não usamos as informações do verificador de empréstimos do Rust, o que simplifica a tradução, mas cobra esse custo na etapa da prova.
      Para raciocinar sobre ponteiros na prova, fazemos o usuário fornecer um alocador personalizado, que ele pode projetar de acordo com como a memória será usada. Por exemplo, se o programa usa três variáveis globais mutáveis, a memória pode ser representada como um registro com três campos. Esses campos começam como None, para representar o estado ainda não alocado.
      Ainda não sabemos o quanto essa técnica vai escalar, mas ao menos por enquanto ela permite evitar raciocínio com lógica de separação. Esperamos que a maior parte dos programas que queremos verificar, especialmente do lado de aplicações, tenha uma disciplina de memória relativamente “simples”.

  • Escrever especificações para verificação formal é parecido com usar testes baseados em propriedades mais complexos? Quando passa de programas não muito complexos, escrever testes baseados em propriedades também costuma ficar bem difícil e consumir bastante tempo

    • É parecido, mas nem sempre igual. Testes baseados em propriedades normalmente especificam uma descrição das entradas na interface do sistema, no nível de função ou procedimento, ou em um nível mais alto, e testam se a saída satisfaz alguma propriedade ou um conjunto de propriedades.
      Ao fazer verificação formal no mesmo nível, isso também pode parecer bastante parecido. Mas as ferramentas de verificação formal conseguem ir mais fundo. Por exemplo, elas podem responder perguntas como: “Dado este invariante de laço para o estado interno do sistema neste cálculo, dá para provar que ele realmente se mantém em todas as iterações?” ou “Dá para provar que nunca ocorre underflow/overflow em nenhum cálculo intermediário durante essa computação?”.
      O primeiro caso também é possível com testes baseados em propriedades, se você extrair o núcleo do laço para um procedimento separado e testar a propriedade do invariante executando com muitos estados intermediários. O segundo é bem mais difícil, a menos que você fragmente o programa de forma extrema a ponto de cada linha poder ser executada separadamente.

  • Eu nem sabia que isso era possível.
    Fico curioso se esse tipo de tentativa pode acelerar a adoção de Rust em partes centrais da introdução no kernel.

  • Alguém poderia explicar o conceito de “verificação” de forma bem simples? Tenho curiosidade sobre por que existe toda uma linguagem como Coq só para esse propósito e qual é o significado prático disso para a sociedade em geral