Масштабный конкурс по Rust для улучшения для улучшение языка

👣 Компания Amazon совместно с Rust Foundation запустили проект, направленный на улучшение безопасности стандартной библиотеки языка Rust.

Основная цель инициативы заключается в проверке надежности и безопасности функций, использующих ключевое слово unsafe, которое позволяет выполнять потенциально опасные операции с памятью, такие как работа с указателями, модификация глобальных переменных и взаимодействие с внешними библиотеками на C/C++.

В настоящий момент в стандартной библиотеке Rust насчитывается около 35 тысяч функций, среди которых примерно 7,5 тысячи содержат код, работающий в режиме unsafe. За последние три года в библиотеке было обнаружено 57 ошибок, связанных с безопасностью, из них 20 признаны уязвимостями.

Проект организован в формате конкурса, где участники получают задания, связанные с проверкой безопасности использования памяти в библиотеках Rust или созданием инструментов для автоматизации таких проверок.

За успешное предоставление формального доказательства безопасности работы с памятью предусмотрены награды. Для выполнения задач и публикации результатов был создан специальный репозиторий, являющийся форком основного репозитория (https://github.com/model-checking/verify-rust-std/issues) Rust.

На данный момент доступно 13 различных заданий (https://model-checking.github.io/verify-rust-std/challenges.html). Одно из них предполагает проверку безопасности работы с сырыми указателями (raw pointers) в модуле core::ptr и предоставление доказательств корректности этих операций. Для этого можно воспользоваться существующими инструментами вроде Aeneas, Kani, Gillian, Verus или Creusot либо разработать собственные.

❤️Поделитесь это новостью с коллегами

▪️Github (https://github.com/model-checking/verify-rust-std/issues)
▪️Задания (https://model-checking.github.io/verify-rust-std/challenges.html)
▪️Примеры (https://github.com/model-checking/verify-rust-std/pulls?q=is%3Apr+is%3Aclosed)