Исправление стандартной библиотеки Rust

Amazon и Rust Foundation планируют повысить безопасность стандартной библиотеки языка Rust. Речь идет о проверке функций, в которых используется слово «unsafe», допускающее операции, небезопасно работающие с памятью, такие как разыменование указателей, изменение статических переменных и обращение к внешним библиотекам на С/C++. Из 35 тысяч функций таких почти 20% – 7500 штук. За последние три года в библиотеке выявлено 57 проблем с корректностью работы, из которых 20 были помечены как уязвимости.

Работа по проверке библиотеки организована в форме конкурса, в котором сейчас 13 заданий. Участники, которые их выполнят, получат денежное вознаграждение. Для верификации можно использовать существующие инструменты, такие как Aeneas, Kani, Gillian, Verus и Creusot, или предложить новые.

Linux Club