Компания Amazon и организация Rust Foundation представиха инициатива, насочена към повишаване на сигурността на стандартната библиотека на езика Rust. Целта е да се провери надеждността и безопасността на функциите, в които се използва ключовата дума „unsafe“, допускаща операции, които не са безопасни за работа с паметта, като разіменоване на указатели, промяна на статични променливи и достъп до външни библиотеки на C/C++. Отбелязва се, че в момента стандартната библиотека на Rust съдържа около 35 хиляди функции, от които в 7500 се срещат блокове код, изпълнявани в контекста на „unsafe“. През последните три години в библиотеката са открити 57 проблема с коректността на работата, от които 20 са маркирани като уязвимости.
Работата по проверка на библиотеката е организирана под формата на конкурс, в който участниците получават различни задачи, свързани с извършването на определени проверки за потвърждаване на безопасната работа с паметта на библиотеките Rust или с разработката на инструменти за автоматизация на подобни проверки. Успешното изпълнение на целта за проверка (предоставяне на формално доказателство за надеждност) предвижда изплащане на награда. За провеждане на експерименти и публикуване на резултатите от работата е създаден репозиторий, представляващ клонинг на основния репозиторий на Rust.
В момента за решаване са предложени 13 задачи. Например, в една от задачите се предлага да се уверите в безопасността на работата с raw-указатели в функциите на модула core::ptr и да предоставите формално доказателство за коректността на операциите с указатели. За верификация могат да се използват съществуващи инструменти, като Aeneas, Kani, Gillian, Verus и Creusot, или да се предложат нови. Примери за изпълнени задачи.
Източник: opennet.ru
