Uma abordagem híbrida para verificação semi-autônoma de Rust

Embora os anos recentes tenham testemunhado um grande volume de trabalhos sobre a verificação eficiente e automatizada de código seguro em Rust, possibilitada pelas ricas garantias do sistema de tipos do Rust, muito menos progresso foi feito na razão sobre o código inseguro devido às suas complexidades únicas. Propomos uma abordagem híbrida para a verificação de Rust de ponta a ponta, na qual a poderosa verificação automatizada de Rust seguro é combinada com a verificação semi-automatizada direcionada de Rust inseguro. Para isso, apresentamos o Gillian-Rust, uma ferramenta de verificação semi-automatizada de prova de conceito que é capaz de raciocinar sobre a segurança de tipos e a correção funcional de código inseguro. Construído sobre a plataforma de verificação composicional paramétrica Gillian, o Gillian-Rust automatiza uma lógica de separação rica para o Rust do mundo real, incorporando a lógica de tempo de vida do RustBelt e as propriedades paramétricas do RustHornBelt. Usando a extensibilidade única do Gillian, nossa nova codificação dessas características é ajustada para maximizar a automação e expõe uma API amigável ao usuário, permitindo uma verificação de baixo esforço de código inseguro. Ligamos o Gillian-Rust com o Creusot, um verificador de última geração para Rust seguro, fornecendo uma codificação sistemática das especificações de código inseguro que o Creusot pode usar, mas não verificar, demonstrando a viabilidade de nossa abordagem híbrida.