Инициатива за верификация на стандартната библиотека Rust

Компанията 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