A Amazon e a Rust Foundation apresentaram uma iniciativa voltada para aumentar a segurança da biblioteca padrão da linguagem Rust. O objetivo declarado é verificar a confiabilidade e segurança de funções que utilizam a palavra-chave "unsafe", que permite operações que trabalham de forma insegura com a memória, como desreferenciação de ponteiros, modificação de variáveis estáticas e chamadas para bibliotecas externas em C/C++. Observa-se que atualmente a biblioteca padrão do Rust conta com cerca de 35 mil funções, das quais 7.500 contêm blocos de código executados no contexto de "unsafe". Nos últimos três anos, foram identificados 57 problemas de correção na biblioteca, dos quais 20 foram considerados vulnerabilidades.
O trabalho de verificação da biblioteca está organizado na forma de um concurso, onde os participantes são apresentados a diferentes tarefas relacionadas à realização de certas verificações para confirmar a operação segura com a memória das bibliotecas Rust ou ao desenvolvimento de ferramentas para automatizar essas verificações. A realização bem-sucedida do objetivo de verificação (fornecimento de provas formais de confiabilidade) prevê o pagamento de uma recompensa. Para a realização de experimentos e publicação dos resultados, foi criado um repositório, que é um fork do repositório oficial do Rust.
Atualmente, 13 tarefas foram propostas para resolução. Por exemplo, em uma das tarefas, é sugerido verificar a segurança do trabalho com ponteiros brutos nas funções do módulo core::ptr e fornecer uma prova formal da correção das operações com ponteiros. Para a verificação, podem ser utilizados ferramentas existentes, como Aeneas, Kani, Gillian, Verus e Creusot, ou novas ferramentas podem ser sugeridas. Exemplos de tarefas concluídas.
Fonte: opennet.ru
