ESBMC no
Projeto verify-rust-std
Vencemos a trilha Tool Applications do concurso de verificação da biblioteca padrão de Rust patrocinado pela AWS. O ESBMC (via o GOTO Transcoder) é agora uma das quatro ferramentas de verificação listadas no livro model-checking/verify-rust-std, ao lado de Kani, VeriFast e Flux.
1 de 4
Ferramentas de verificação listadas no livro model-checking/verify-rust-std (Kani, GOTO Transcoder, VeriFast, Flux)
>90%
Produtos e serviços baseados em Rust que dependem da biblioteca padrão de Rust (segundo o AWS Open Source Blog)
~70%
Programas em C nos quais o ESBMC reportou possíveis vulnerabilidades antes da transpilação (segundo o SafeTrans, Farrukh et al., 2026)
CI
O GOTO Transcoder roda no fluxo de CI do projeto verify-rust-std
Contexto
Rust é cada vez mais adotada como linguagem de programação de sistemas com segurança
de memória, mas a maioria das aplicações Rust ainda depende de uma fina camada de
código unsafe
não verificado na biblioteca padrão. Como observa o AWS Open Source Blog, "mais de
90% dos produtos/serviços baseados em Rust dependem da biblioteca padrão de Rust, e
praticamente toda aplicação Rust depende da biblioteca core", portanto, qualquer
falha de solidez na biblioteca padrão se propaga por toda parte.
A AWS e a Rust Foundation lançaram um esforço comunitário, model-checking/verify-rust-std, para verificar formalmente a biblioteca padrão, estruturado como um concurso baseado em desafios com uma trilha Tool Applications que abriu o projeto a backends de verificação adicionais.
Abordagem
Nossa equipe liderou o desenvolvimento do GOTO Transcoder, descrito pela Rust Foundation como uma camada de compatibilidade originalmente construída como projeto de pesquisa de doutorado para formalizar e unificar as representações internas do toolchain CPROVER. Ele é distribuído como parte do projeto open-source ESBMC. Ele permite que o ESBMC consuma os arquivos de programa GOTO que o Kani já produz, de modo que o fluxo de verificação Rust existente possa ser redirecionado para o motor de verificação limitada de modelos baseado em SMT do ESBMC, sem alterações no toolchain do compilador Rust. Submetemos este trabalho pela trilha Tool Applications do concurso de verificação patrocinado pela AWS, o qual vencemos.
O ESBMC também foi adotado como ferramenta upstream no framework SafeTrans (Farrukh, Coskun, Palit e Polychronakis, ReCode '26 / arXiv 2505.10708, 2026). O SafeTrans é um pipeline de transpilação de C para Rust assistido por LLM, desenvolvido por pesquisadores de Stony Brook, UC Davis e AWS, que usa o ESBMC para identificar possíveis vulnerabilidades no código-fonte em C antes da tradução. A Cyber-Reasoning Consultancy (CRC) não é autora do SafeTrans; o próprio artigo afirma que "this work does not relate to Baris Coskun's position at Amazon."
Resultados
O ESBMC (via o GOTO Transcoder) é uma das quatro ferramentas de verificação listadas no livro verify-rust-std, ao lado de Kani, VeriFast e Flux (segundo o SUMMARY do projeto).
O GOTO Transcoder roda no fluxo de CI do projeto verify-rust-std, aplicando a verificação do ESBMC aos componentes da biblioteca padrão cobertos pelos desafios aceitos do projeto (segundo o post da Rust Foundation e a proposta de ferramenta aceita #108).
Em uma avaliação independente do SafeTrans (Farrukh et al., ReCode '26): "approximately 70% of the programs failed verification", ou seja, o ESBMC reportou possíveis vulnerabilidades em cerca de 70% dos 2.653 programas em C avaliados antes da transpilação, totalizando 10.375 problemas reportados em todas as categorias.
Referências
- Rust Foundation. Expanding the Rust Formal Verification Ecosystem: Welcoming ESBMC. rustfoundation.org/media/expanding-the-rust-formal-verification-ecosystem-welcoming-esbmc
- AWS Open Source Blog. Verify the Safety of the Rust Standard Library. aws.amazon.com/blogs/opensource/verify-the-safety-of-the-rust-standard-library
- Muhammad Farrukh, Baris Coskun (Amazon Web Services), Tapti Palit, Michalis Polychronakis. SafeTrans: LLM-assisted Transpilation from C to Rust. ReCode '26 (1st Workshop on Code Translation, Transformation, and Modernization). arxiv.org/abs/2505.10708 , "This work does not relate to Baris Coskun's position at Amazon."
- model-checking/verify-rust-std, SUMMARY do livro listando as quatro Ferramentas de Verificação (Kani, GOTO Transcoder, VeriFast, Flux). model-checking.github.io/verify-rust-std
Nota. Esta página descreve um engajamento de pesquisa publicado. A submissão à trilha Tool Applications e a consequente listagem como Approved Tool no livro model-checking/verify-rust-std são creditadas ao grupo de pesquisa da University of Manchester do qual o fundador da CRC, Lucas Cordeiro, é membro; a CRC Ltd não mantém parceria comercial com a Rust Foundation ou a AWS. O SafeTrans é um artigo independente de pesquisadores da Stony Brook University, UC Davis e AWS que adota o ESBMC como ferramenta de verificação; a CRC não é autora, e o próprio artigo do SafeTrans afirma que "this work does not relate to Baris Coskun's position at Amazon." O fluxo de CI do verify-rust-std é hospedado na organização do GitHub model-checking, não na infraestrutura interna da Amazon.