Verus: uma base prática para a verificação de sistemas

Software de sistema, como sistemas de arquivos, kernels, bancos de dados e alocadores, é de baixo nível, crítico para o desempenho e muitas vezes concorrente, então é difícil acertá-lo. A verificação formal pode eliminar classes inteiras de bugs antes da entrega, e a comunidade já verificou muitos sistemas, mas os autores observam que boa parte desse sucesso exigiu esforço heroico, lógicas sob medida para um domínio (a segurança contra falhas, por exemplo) ou perda de expressividade em troca de automação das provas.

Este artigo do SOSP 2024 (Austin), uma colaboração entre Carnegie Mellon University, Microsoft Research, VMware Research, MPI-SWS, ETH Zurich, University of Texas at Austin, University of Michigan, University of British Columbia, University of Wisconsin-Madison e Weizmann Institute of Science, apresenta o Verus como base para a verificação de sistemas. O Verus confere código Rust contra especificações escritas na sintaxe do Rust e envia as obrigações de prova ao solver SMT Z3. Um artigo anterior do OOPSLA 2023, de autores em parte coincidentes, formalizou como o Verus verifica Rust seguro e inseguro com tipos ghost lineares. Este descreve os recursos voltados a sistemas e os avalia.

Termos-chave: uma spec function é uma função matemática pura usada só nas especificações, uma proof function é código ghost que ajuda o solver e o código exec é o Rust comum que executa. Um trigger é o padrão de expressão que diz a um solver SMT quando instanciar um quantificador. A EPR (effectively propositional logic) é uma lógica restrita que pode ser verificada de forma totalmente automática. O VerusSync é a nova linguagem para descrever estado ghost concorrente como transições de estado. A razão prova-código (P/C) é o número de linhas de prova por linha de código executável. A base confiável (TCB) aqui são as especificações de nível mais alto, o verificador Verus, os solvers e o compilador do Rust.

Vale conhecer antes: pré e pós-condições no estilo de Hoare (requires e ensures), como um solver SMT instancia quantificadores e o ownership do Rust. O RustBelt é citado nos trabalhos relacionados como a verificação manual de Rust inseguro em Coq, o contraste com a abordagem automatizada do Verus. Entre os usos do Verus por outros grupos, o artigo cita um artigo de workshop sobre o microkernel Atmosphere. O Atmosphere, artigo posterior do SOSP 2025 nesta biblioteca, também usa o Verus, mas este artigo não poderia citá-lo, então esse link é um pareamento meu.

• Automação geral enxuta. O Verus converte requires e ensures em condições de verificação para o Z3 com a lógica de Floyd-Hoare padrão e mantém as consultas pequenas. As spec functions são puras, totais e sem acesso ao heap, então se traduzem direto em funções SMT. O raciocínio sobre memória, vetores de bits e aritmética não linear fica isolado das consultas principais, o contexto de cada módulo é podado de imports inalcançáveis e os triggers são escolhidos de forma conservadora, o mínimo possível, com o usuário incentivado a revisá-los. Os autores aceitam mais esforço inicial em projetos pequenos em troca de escalar para projetos grandes.
• EPR seletiva. O desenvolvedor marca um módulo com #[epr_mode], abstrai uma estrutura de dados ou protocolo para a EPR (chaves como um conjunto totalmente ordenado, por exemplo), obtém uma prova automática do invariante indutivo e exporta o resultado para o original irrestrito. O Verus confere que os campos das structs são privados, que o grafo de alternância de quantificadores é acíclico e ativa a instanciação de quantificadores baseada em modelo do Z3. O exemplo trabalhado é o delegation map do IronKV, cuja operação set custou cerca de 300 linhas de prova no modo padrão e vários dias de esforço do desenvolvedor.
• Ferramentas para idiomas de sistemas. by(bit_vector) lê inteiros como vetores de bits SMT dentro de uma asserção, by(integer_ring) prova relações de congruência, by(nonlinear_arith) roda uma consulta isolada sem contexto implícito e a prova por computação usa um interpretador simbólico embutido (o exemplo dos autores é uma tabela de consulta de CRC-32 cuja prova eles chegaram a abandonar). Macros do Rust eliminam provas repetitivas, como as de marshalling. Cada verificação é automática, mas a codificação SMT principal então simplesmente assume o resultado, e é por isso que o artigo chama essas ferramentas de confiáveis.
• VerusSync. Combina álgebras de recursos da lógica de separação concorrente com uma linguagem de transições cuja sintaxe segue a do Ivy. O desenvolvedor declara campos com estratégias de sharding (variável, constante, mapa), escreve transições com condições de habilitação e atualizações e fornece um invariante indutivo. O Verus então gera shards ghost e operações que o código usa, ligados a células atômicas de memória. Os autores dizem que um sistema VerusSync bem formado sempre corresponde a uma álgebra de recursos, então o desenvolvedor não precisa construir monoides. Máquinas de estado no nível do sistema, como modelos de segurança contra falhas, são um caso particular.
• Tipos do Rust para segurança de memória. A segurança de memória vem do verificador de tipos de ownership do Rust. O Verus aceita um subconjunto do Rust inseguro, com ponteiros brutos protegidos por permissões ghost, e rejeita o que está fora dele. Os autores ampliaram o suporte a ponteiros brutos para esses estudos de caso.

A avaliação tem duas escalas. Os milibenchmarks comparam o Verus com Dafny, Low* (o subconjunto de baixo nível do F*), Prusti, Creusot e Ivy em uma lista simplesmente encadeada, uma lista duplamente encadeada (Rust inseguro, por causa dos ponteiros cíclicos), um teste de raciocínio sobre memória que atualiza quatro listas em uma função e um lock distribuído provado no modo padrão e no modo EPR. Rodam em uma AWS EC2 m5.8xlarge (16 núcleos, sem multithreading, 128GiB) e relatam medianas de 20 execuções, além do tempo para reportar um erro depois de remover uma pré-condição de pop ou index.

Os macrobenchmarks somam mais de 6,1K linhas de Rust e mais de 31K linhas de prova. Dois são portes que preservam os algoritmos originais: o host do IronKV, do IronFleet (Dafny, nível de protocolo ignorado), e a biblioteca de Node Replication NR, do IronSync (Linear Dafny). Três são novos: uma tabela de páginas x86-64, um alocador concorrente baseado no mimalloc e um log circular persistente para memória persistente Optane, projetado para um sistema de armazenamento de produção em escala de nuvem (os agradecimentos citam o Azure Storage pela ajuda com a definição do problema e a integração). As verificações de desempenho são o IronKV contra o IronFleet em um laptop com Windows, o NR em um Xeon Platinum 8260 de quatro soquetes com 0%, 10% e 100% de escritas, a tabela de páginas contra uma não verificada em 100M de operações de map e unmap, o alocador no mimalloc-bench e o log contra o libpmemlog em um módulo Optane de 128GiB.

Estes são os resultados relatados pelos autores.

• Listas encadeadas. O Verus verifica as listas simples e dupla em 0,66 s e 1,15 s. As outras ferramentas levam de 3 a 28 vezes mais na primeira e de 24 a 61 vezes mais na segunda, de onde vem o 3 a 61× do resumo. Os 1,88 s do Creusot na primeira são apenas o tempo até um resultado parcial que exige conclusão manual, e o Prusti não consegue expressar a segunda.
• Retorno de falhas e raciocínio sobre memória. Com uma pré-condição removida, Verus, Dafny e Prusti reportam o erro quase tão rápido quanto reportam o sucesso, enquanto o Low* vai de um segundo para quatro e o Creusot de um segundo para vinte. Ao atualizar quatro listas, o tempo do Verus cresce linearmente, cerca de 1,6 ms por push (1,8 ms nas listas duplamente encadeadas). O do Dafny cresce de forma dramática, o Low* não retorna depois de mais de um push, e Prusti e Creusot crescem de forma super-linear.
• Lock distribuído. A prova de indutividade no modo padrão tem cerca de 25 linhas. A versão EPR é automática, mas exige cerca de 100 linhas de boilerplate, então os autores concluem que a EPR compensa em casos complexos como o delegation map e que o Verus deveria automatizar o boilerplate.
• IronKV. O porte tem 1.533 linhas de código e 4.509 de prova (P/C 2,9), contra 1.923 e 8.070 (4,2) em Dafny. A verificação leva 41 s em um núcleo e 18 s em oito, contra 445 s e 201 s, e as consultas SMT têm 17 MB contra 352 MB. Os autores resumem isso como consultas 95% menores e verificação 10× mais rápida, com desempenho comparável ao original.
• NR. O porte tem 736 linhas de código e 5.237 de prova (7,1), contra 730 e 7.828 (10,7) em Linear Dafny. A verificação leva 17 s em um núcleo e 9 s em oito, contra 1.089 s e 228 s, com consultas de 22 MB contra 2.063 MB. Os autores atribuem ao VerusSync a maior parte da redução de prova, e o Verus-NR iguala o IronSync-NR e o original não verificado em throughput.
• Tabela de páginas. 400 linhas de código e 5.329 de prova (13,3:1), verificadas em 63 s em um núcleo e 34 s em oito, usando as ferramentas de vetor de bits, não linear e computação 62, 39 e 11 vezes. A latência de map iguala a da referência não verificada, enquanto o unmap é muito mais lento porque a versão verificada recupera os diretórios de páginas esvaziados, o que uma variante não verificada sem recuperação confirma. Benchmarks maiores no nível do SO mostram diferenças desprezíveis.
• Alocador. Cerca de 3,1K linhas de código executável contra cerca de 10K no mimalloc, P/C 4,3, uma especificação de 37 linhas voltada ao usuário mais 245 linhas de especificação confiável para mmap e utilitários de threads. A verificação leva 262 s em um núcleo e 55 s em oito na Figura 9. Ele funciona como substituto direto, com limites (sem realloc, alocações alinhadas ou alocações acima de 128KiB), e completa 8 dos 19 benchmarks do mimalloc-bench, sem paridade de desempenho.
• Log persistente. 739 linhas de código, P/C 3,9, verificadas em 12 s. Ele refina um log infinito abstrato, torna as operações atômicas com relação a falhas e protege os metadados contra corrupção até o CRC, e está integrado a uma base de código de produção como um crate Rust comum. Depois que um trait Serializable removeu um overhead inicial de cópia, o throughput de append é comparável ao do libpmemlog. Os autores observam que isso vale mesmo com o log verificado calculando CRCs e o libpmemlog não, porque o libpmemlog toma um lock a cada append e o log verificado não usa nenhum.

O artigo é franco sobre o alcance de suas evidências. Ele admite o seguinte.

• A base confiável é real. Os resultados valem em relação às especificações de nível mais alto, ao verificador Verus, aos solvers e ao compilador do Rust, e o Verus aceita apenas um subconjunto do Rust inseguro. A automação customizada também é confiável, e a tabela de páginas, o alocador e o log dependem de especificações confiáveis da MMU, do mmap, de utilitários de threads e de um crate de CRC.
• A avaliação é inicial. Os autores chamam a razão de 13,3:1 da tabela de páginas de "relatively high" e dizem que ela pode refletir inexperiência ou ser inevitável para um componente de SO. Partir de código correto e provas prontas é, nas palavras deles, "overly optimistic", e a verdadeira avaliação virá de projetos futuros. O alocador está incompleto e é mais lento que o mimalloc.
• Restam arestas. O modo EPR exige cerca de 100 linhas de boilerplate mesmo para o lock simples, e suas consultas não são estritamente EPR por causa de como os tipos polimórficos são codificados, embora nenhuma prova correta tenha falhado. As contagens de linhas confiáveis do IronKV são, segundo eles, ruidosas, e os triggers conservadores custam esforço em projetos pequenos.

Os pontos a seguir são uma leitura das evidências, não afirmações do artigo.

• O esforço é inferido, não medido. O resumo promete verificação mais rápida e mais barata, mas o esforço é aproximado por contagens de linhas e tempo de verificação. Além da anedota de vários dias do delegation map, não aparece nenhuma pessoa-hora, e a "crisp interactivity" do porte do IronKV é o relato dos próprios autores do porte. Os portes também partem de provas prontas, e o nível de protocolo do IronKV foi ignorado na expectativa de que as provas em Dafny e Verus fossem parecidas, o que é afirmado, não testado.
• As razões deixam de fora a base confiável. A coluna de linhas confiáveis da Figura 9 soma 4.692 linhas, perto das 6.119 de código executável, e supera o código na tabela de páginas (1.117 contra 400) e no log (1.284 contra 739). O ônus de auditoria que resta para humanos não é capturado pela razão de destaque de 5,1.
• Texto e tabela divergem em alguns pontos. Para o NR o texto afirma duas ordens de grandeza, enquanto a Figura 9 dá cerca de 64× em um núcleo e 25× em oito (as consultas são cerca de 94× menores). O alocador é verificado em "just over a minute" no texto, mas em 55 s com oito núcleos e 262 s com um na tabela. A linha de total do Verus (6.119 linhas de código e 31.231 de prova, atrás do 6,1K e 31K de destaque) não é a soma das cinco linhas acima dela, que eu leio como cerca de 6.586 e 31.691. Esta análise usa os valores da tabela.
• As comparações são dos próprios autores. Os milibenchmarks vêm de exemplos de outros frameworks, conferidos com seus projetistas, o que é justo, mas cada número dos milibenchmarks é uma mediana de 20 execuções em uma máquina, sem dispersão, e o extremo baixo da faixa de 3 a 28× é o resultado parcial do Creusot. O Ivy é citado como ferramenta de comparação, mas nenhuma medição do Ivy é relatada, só as duas provas do próprio Verus para o lock.
• A evidência de desempenho é fina. O IronKV rodou como três servidores e um cliente de 10 threads em um laptop, com payloads limitados a 512 bytes (100 execuções por barra, com intervalos de confiança). O benchmark do log não diz quantas threads fazem append, então a explicação do lock para a paridade é plausível, mas não testada. O Verus-mimalloc é mais lento em seis dos oito benchmarks que completa (o sh6benchN leva 2,0 s contra 0,14 s, o glibc-simple 6,6 s contra 1,2 s) e empata só nas duas execuções de cache-scratch. O artigo não diz o que causa a diferença, apenas que um subconjunto dos recursos e otimizações do mimalloc foi implementado, então nenhum profile liga a lentidão às ausentes.
• A usabilidade é afirmada, não estudada. O objetivo de alcançar desenvolvedores sem grande experiência em verificação não é testado: os cinco estudos de caso foram feitos pelos autores, que também desenvolvem o Verus, e o uso externo é apenas listado (controladores de cluster, um microkernel, um módulo para VMs confidenciais, código produzido por LLMs). A metateoria do VerusSync é declarada ("our metatheory shows") sem prova nem citação no artigo.

• Automatizar o boilerplate da EPR, que os autores apontam como uma necessidade do Verus, para que protocolos pequenos como o lock também se beneficiem.
• Terminar o alocador (realloc, alocações alinhadas e grandes) e fechar sua diferença de desempenho, com um profile de onde o tempo vai.
• Medir esforço e experiência diretamente: pessoa-horas, defeitos pegos no log de produção e um estudo com desenvolvedores de fora do grupo do Verus, já que a meta de alcançar uma comunidade mais ampla depende disso.
• Verificar sistemas maiores sobre o Verus, a fronteira declarada pelos autores, e encontrar abstrações que reduzam a razão da tabela de páginas. O Atmosphere é um exemplo posterior de microkernel verificado com o Verus.