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

Ferramenta Verus para a verificação da correção de código Rust

• Verus é uma ferramenta para verificar a correção de código escrito em Rust.
• O desenvolvedor escreve a especificação que o código deve atender, e 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, o Verus depende de um solver robusto para provar a correção do código.
• O Verus atualmente suporta um subconjunto de Rust (em expansão) e, em alguns casos, permite que os desenvolvedores verifiquem estaticamente a correção do código além do sistema de tipos padrão do Rust (por exemplo, manipulação de ponteiros brutos).

Estado atual do Verus

• O Verus está em desenvolvimento ativo.
• Funcionalidades podem quebrar ou faltar, e a documentação ainda é incompleta.
• Para experimentar o Verus, esteja pronto para pedir ajuda no Zulip.

Testando o Verus

• Para testar o Verus no navegador, visite o Verus Playground.
• Para desenvolvimentos mais complexos, siga as instruções de instalação e comece pelos tutoriais e referências antes de conferir os documentos abaixo.

Documentação do Verus

• Tutoriais e referência
• Documentação da API para a biblioteca padrão do Verus
• Guia de verificação de código concorrente
• Objetivos do projeto
• Contribuindo para o Verus
• Licença

Entrar em contato, relatar problemas e iniciar discussões

• Abra issues ou inicie discussões no GitHub, e participe do Zulip para discussão em tempo real e quando precisar de ajuda.
• Para problemas reais de funcionalidades existentes (bugs), use issues no GitHub; para conversas mais abertas sobre solicitações de recursos e funcionalidades planejadas, use GitHub Discussions.
• Contribuições são bem-vindas; se você deseja contribuir com código, confira as dicas em Contributing to Verus.

Opinião do GN⁺

• Rust é uma linguagem reconhecida por ser ideal para programação de sistemas, por oferecer segurança e desempenho, e o Verus parece um projeto que pode potencializar ainda mais essas vantagens do Rust. Em especial, o recurso de validação para programação concorrente parece bastante promissor.

• No entanto, parece ainda estar em uma fase inicial e ter suporte limitado à sintaxe do Rust, então ainda precisa de mais desenvolvimento para ser aplicado em produção. Ainda assim, como a análise estática é importante para garantir a segurança do código antecipadamente, o potencial de avanço é alto.

• Embora ainda esteja no início e precise de melhorias, como documentação insuficiente e suporte sintático limitado, é provável que se torne um projeto importante no ecossistema Rust no longo prazo. Especialmente, espera-se alta adoção em áreas críticas de confiabilidade, como programação de sistemas ou blockchain.

[GN⁺]

Comentário do Hacker News

• Escrevi um controller de Kubernetes formalmente verificado usando o Verus
  • Dá para provar uma propriedade de vivacidade de que o controller eventualmente irá ajustar o cluster para o desired state solicitado
  • Há muita sutileza e nuance em formalizar a correção (mudanças rápidas nos requisitos do desired state, assincronia, falhas, etc.)
  • O código está no link do GitHub e está vinculado a um paper que deve ser apresentado na OSDI 2024
• Como um primeiro passo em direção ao Verus, é possível adicionar pré e pós-condições com debug_assert no Rust
  • O compilador Rust remove isso por padrão no build de produção
  • Fornece exemplos do tutorial do Verus e exemplos de checagem em runtime usando debug_assert
• Pergunta de iniciante sobre a diferença entre "verificar a correção de código" e "provar a correção de código"
  • Fica a curiosidade sobre se há bons materiais de estudo de "prova" de código para desenvolvedores de produção com pouca base em CS/matemática
  • Fiquei muito curioso sobre por que a prova de "zero knowledge" é importante e por que isso é tão relevante
• Rust ainda não tem uma opção no padrão assim como C/C++, Common Lisp e Ada/SPARK2014
  • Em comparação com ferramentas de verificação desenvolvidas para Ada/SPARK2014, isso é um alvo em movimento
• Dafny é uma "linguagem de programação consciente da verificação" que pode compilar para Rust (link do GitHub)
• Um dos principais contribuidores fez uma ótima apresentação do Verus no meetup de Rust de Zurique (link do YouTube)
  • O código de "ghost" ficando encaixado no programa foi muito impressionante (me lembrou um pouco de Ada)
• Comparação entre Verus e SPARK
  • É o mesmo tipo de verificador? Que diferenças existem além do fato de Verus não ser um verificador para Ada, e sim para Rust?
• Alguém familiarizado com Verus poderia comparar desempenho e expressividade do Verus e do Lean4?
  • Entendo que Verus é uma ferramenta de verificação baseada em SMT e Lean é um assistente de prova interativo e também baseado em SMT
  • Porém, como meu entendimento de verificação formal é limitado, seria bom ouvir a opinião de alguém expert em técnicas formais de software
• Existe alguma relação entre Verus e Kani? Eles funcionam de forma diferente? (link do GitHub do Kani)
  • Existe uma forma de implementar isso mantendo o código gerado como código Rust válido compilável com ferramentas Rust vanilla?