Tecnologia de verificação em Rust aplicada a código de sistemas de baixo nível

 (github.com/verus-lang)
1 pontos por GN⁺ 2024-05-06 | 1 comentários | Compartilhar no WhatsApp
  • Verus é uma ferramenta para verificar a correção de código escrito em Rust: quando o desenvolvedor especifica o que o código deve fazer, ela verifica estaticamente se o código Rust executável satisfaz essa especificação em todas as execuções possíveis
  • Em vez de adicionar verificações em tempo de execução, ela usa um solver poderoso para provar que o código está correto; atualmente, oferece suporte apenas a uma parte do Rust
  • Em alguns casos, consegue verificar estaticamente a correção de código que manipula raw pointers, indo além do sistema de tipos padrão do Rust
  • O projeto está em desenvolvimento ativo, e recursos podem estar quebrados ou ausentes; a documentação ainda não está completa, então usuários devem estar preparados para pedir ajuda no Zulip
  • Verus Playground para navegador, instruções de instalação, tutorial e referência, documentação da API da biblioteca padrão, guia de verificação de código concorrente, exemplos e testes são oferecidos como caminhos para aprendizado e experimentação

O que o Verus verifica

  • Verus é uma ferramenta para verificar a correção de código Rust
  • O desenvolvedor escreve, como uma especificação, o comportamento que o código deve realizar
  • O Verus verifica estaticamente se o código Rust executável sempre satisfaz essa especificação em todas as execuções possíveis
  • Em vez de adicionar verificações em tempo de execução, ele usa um solver para provar que o código está correto
  • A cobertura atual é um subconjunto do Rust, e há trabalho em andamento para ampliar essa cobertura
  • Em alguns casos, ele consegue verificar estaticamente a correção de código além do sistema de tipos padrão do Rust, por exemplo código que manipula raw pointers

Estado de desenvolvimento e cuidados ao usar

  • O Verus é um projeto em desenvolvimento ativo
  • Recursos podem estar quebrados ou ausentes
  • A documentação ainda não está completa
  • Para experimentar o Verus, é preciso estar preparado para pedir ajuda no Zulip
  • A comunidade do Verus publicou vários artigos de pesquisa, e diversos projetos na indústria e na academia usam o Verus
  • A lista relacionada pode ser conferida na página publications and projects

Como começar e ferramentas de desenvolvimento

  • Para experimentar o Verus no navegador, é possível usar o Verus Playground
  • Para um desenvolvimento mais sério, é necessário seguir as instruções de instalação
  • O aprendizado pode começar em Tutorial and reference
  • Também há suporte ao formatador automático verusfmt para código Verus

Documentação e materiais de aprendizado

Exemplos e participação na comunidade

  • Exemplos de uso do Verus também oferecem vários pontos de partida além da documentação
    • Publications and projects: publicações e projetos que usam o Verus
    • Videos, slides, and exercises: vídeos, slides e exercícios de um tutorial de um dia sobre Verus
    • Standalone examples: exemplos independentes de uso do Verus em tarefas pequenas e concretas
    • Small and medium-sized examples: exemplos que demonstram diversos recursos do Verus
    • Unit tests: testes com exemplos da sintaxe e dos recursos do Verus
  • Relatos de issues e discussões podem ser feitos no GitHub ou no Zulip
  • O projeto usa GitHub discussions para solicitações de recursos e conversas abertas, e mantém bugs executáveis de recursos existentes em GitHub issues
  • Quem quiser contribuir com código pode consultar as instruções de Contributing to Verus

Leituras relacionadas

1 comentários

 
GN⁺ 2024-05-06
Opiniões no Hacker News

  • Escrevi um controlador do Kubernetes formalmente verificado com Verus
    Basicamente, é possível provar propriedades de vivacidade como “em algum momento, o controlador reconcilia o cluster para o estado-alvo solicitado”
    Mas, quando se considera que o estado-alvo muda rapidamente, assincronicidade, falhas etc., a própria especificação do que é “correto” tem muitas sutilezas
    Código: https://github.com/vmware-research/verifiable-controllers/, e o artigo relacionado deve aparecer no OSDI 2024

    • Fico curioso sobre o que isso faz além de testes unitários

  • Como um pequeno passo rumo ao Verus, dá para colocar debug_assert do Rust em pré-condições e pós-condições
    O compilador Rust, por padrão, remove isso em builds de produção
    Nos exemplos de verificação do tutorial do Verus, escrevem-se o intervalo de entrada e as condições do resultado com requires e ensures; na versão com checagens em tempo de execução, as mesmas condições são verificadas durante a execução, como em debug_assert(-16 <= x1) e debug_assert(x8 == 8 * x1)

    • Um problema atual da sintaxe do Verus é que todo o código precisa ser envolvido por uma macro procedural
      Outras ferramentas de prova/verificação/contratos em Rust, como Creusot, usam uma sintaxe baseada em atributos, que em geral parece mais leve e mais “Rust”
      Seria bom se esse estilo também se tornasse possível em futuras versões do Verus
    • Gostaria que mais gente usasse assert desse tipo
      É uma ótima ferramenta de documentação e complementa muito bem o sistema de tipos e os testes
    • Também dá para experimentar o crate "contracts": https://docs.rs/contracts/latest/contracts/
    • O exemplo do Verus é parecido com a forma como escrevo código Clojure
      Coloco pré-condições e pós-condições na maioria das funções, e a JVM tem uma flag que permite removê-las facilmente em builds de produção

  • Como alguém que não tem muita experiência real em ciência da computação, fiquei curioso: no README, qual é a diferença entre verificação, em “verificar a correção do código”, e “prova”, como se diz em outros lugares?
    Também queria materiais bons para um programador profissional sem uma formação forte em ciência da computação/matemática aprender sobre “provas” aplicadas a código
    Além disso, não entendo muito bem por que provas de conhecimento zero são tão importantes e relevantes. Por exemplo, ouvi falar de coisas como x.com/ZorpZK, mas não entendo por que isso é legal

    • Um bom material para aprender verificação de código junto com programação funcional é Software Foundations: https://softwarefoundations.cis.upenn.edu
      Mas o Coq usado no Verus e em Software Foundations tem abordagens diferentes
      O Verus tenta provar propriedades automaticamente usando um sistema automático de resolução de restrições chamado solucionador SMT, enquanto no Coq é preciso provar muito mais coisas manualmente, com automação limitada
      Ambos têm prós e contras; a automação é ótima quando funciona, mas frustrante quando não funciona
      Provas de conhecimento zero devem ser vistas como uma área um pouco diferente, e muita gente que trabalha com verificação/provas formais nem mexe com elas. É melhor pensar nelas como uma primitiva criptográfica
    • Aqui, verificação e prova estão sendo usadas como sinônimos, e isso fica claro também mais adiante no primeiro parágrafo
      Provas de conhecimento zero têm overhead alto e carecem do chamado “killer app”, então sua utilidade prática, importância e relevância ainda não são grandes, mas conceitualmente são interessantes
    • Neste contexto, “verificação” e “prova” são a mesma coisa
      Também gostaria de ter bons materiais de estudo. A documentação do Dafny é bem boa, mas verificação formal de software ainda não parece estar em um estágio bom para programadores comuns que não têm doutorado em ciência da computação/matemática
      Olhando só os exemplos, parece relativamente fácil, mas logo você esbarra em “não foi possível provar”, e a resposta para o porquê costuma entrar em detalhes profundos de implementação que só o autor parece saber
    • Pelo que sei, provas de conhecimento zero permitem provar que você sabe algo sem revelar esse conteúdo
      Por exemplo, é possível verificar que você sabe a senha sem enviá-la ao servidor, dificultando que um servidor malicioso ou um atacante man-in-the-middle espione a senha
      Também podem oferecer opções melhores para verificação de identidade. Você pode provar que possui um documento de identidade emitido pelo governo sem entregar o documento em si ao servidor, reduzindo situações em que ele é “armazenado por no máximo 2 anos/3 anos/6 meses” e acaba vazando
    • Acho que a expressão “um programador profissional provar coisas sobre código” ainda é quase uma contradição
      Provas sobre código ainda não são algo feito por programadores profissionais
      Lógica de Hoare é um bom ponto de partida e às vezes é ensinada em cursos introdutórios de ciência da computação
      Coq tem uma curva de aprendizado íngreme, especialmente se você não estiver familiarizado com OCaml ou linguagens parecidas. Why3 talvez seja mais amigável para iniciantes: https://www.why3.org
      Prova e verificação podem significar a mesma coisa, mas prova dá mais uma sensação de algo interativo, enquanto verificação dá a sensação de algo que pode ser automatizado, como model checking ou resolução SMT de programas anotados

  • Para quem não conhecia projetos parecidos, Dafny é uma “linguagem de programação consciente de verificação” que pode ser compilada para Rust: https://github.com/dafny-lang/dafny

  • Parece muito legal. Acho que seria útil para as pessoas ter orientações ou exemplos de como adicionar provas a uma base de código existente
    Por exemplo, imagine um app GUI mínimo com apenas uma caixa de texto que recebe, via requisição HTTP, um array não confiável e desconhecido em tempo de compilação, faz bubble sort nele e depois o exibe
    O bubble sort tem um bug intencional, como um erro off-by-one que deixa o último elemento inalterado, e os testes unitários por acaso não pegam esse bug. A preocupação de que os testes estejam incompletos pode ser a principal motivação para partir para provas
    Então seria bom mostrar o processo de substituir os testes unitários por provas, descobrir o bug e corrigi-lo
    Não é preciso explicar em detalhes o próprio código de prova; basta focar em detalhes práticos, como a fronteira entre o código matemático provado e o código de entrada/saída não provado, as linhas de comando usadas para provar e compilar, e um arquivo zip para a pessoa mexer
    Na verdade, talvez só ler da entrada padrão e escrever na saída padrão já seja suficiente

  • Um dos principais contribuidores fez uma excelente apresentação sobre Verus no meetup de Rust em Zürich: https://www.youtube.com/watch?v=ZZTk-zS4ZCY
    Achei impressionante como esse código “ghost” se encaixa de forma limpa no programa, e me lembrou um pouco Ada

  • Fico me perguntando se Rust já tem um padrão como C/C++, Common Lisp e Ada/SPARK2014
    Se não tiver, isso vira um alvo em movimento em comparação com as ferramentas de verificação desenvolvidas para Ada/SPARK2014
    O legado de Ada/SPARK2014, que vai de bare metal a aplicações críticas de segurança de alta integridade, também é difícil de ignorar

  • Fico curioso sobre qual é a relação entre isso e o Kani. Eles funcionam de formas diferentes?
    https://github.com/model-checking/kani

    • Verificadores de modelo normalmente exploram apenas um número limitado de estados, então são eficientes para encontrar bugs e muitas vezes não exigem anotações adicionais no programa
      Verificadores baseados em SMT automático, como Verus, Dafny, F* e o meu VCC, exigem anotações em quase todas as funções e loops, mas oferecem garantias mais amplas sobre a correção do programa
      Ferramentas baseadas em provadores interativos, como Coq ou Lean, geralmente precisam de mais orientação do usuário, mas conseguem garantir propriedades mais complexas

  • Fico me perguntando como Verus se compara ao SPARK
    É o mesmo tipo geral de verificador? Tirando o fato de ser um verificador para Rust em vez de Ada, em que Verus é diferente?

  • Seria bom se alguém que conhece bem Verus pudesse explicar as diferenças de desempenho e expressividade entre Verus e Lean4
    Entendo que Verus é uma ferramenta de verificação baseada em SMT, enquanto Lean é um provador interativo e também uma ferramenta baseada em SMT
    Mas meu entendimento da área de verificação formal é limitado, então gostaria de ouvir a visão de alguém que conhece bem métodos formais de software

    • Lean é parecido com Coq
      Por exemplo, assim como no livro “Software Foundations” de Coq, é possível formular e provar proposições sobre código C, mas parece que quase ninguém faz isso com Lean, e o ferramental é insuficiente
      Também é possível escrever programas em Lean4 e provar coisas sobre esses programas, e há algumas pessoas fazendo isso aos poucos
      Formalizar matemática pura e publicar artigos sobre isso é hoje a principal forma de uso de Lean4 e Coq
      O tipo de coisa que Lean/Coq conseguem de fato enunciar e provar é mais geral, mas talvez programas do mundo real não precisem necessariamente de tanta generalidade