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

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

Работа по проверке библиотеки организована в форме конкурса, участникам которого предлагаются различные задачи, связанные с выполнением определённых проверок для подтверждения безопасной работы с памятью библиотек Rust или с разработкой инструментов для автоматизации подобных проверок. Успешное выполнение цели проверки (предоставление формального доказательства надёжности) предусматривает выплату вознаграждения. Для проведения экспериментов и публикации результатов работы создан репозиторий, представляющий собой ответвление от штатного репозитория Rust.

В настоящее время для решения предложено 13 заданий. Например, в одном из заданий предлагается убедится в безопасности работы с raw-указателями в функциях модуля core::ptr и предоставить формальное доказательство корректности операций с указателями. Для верификации можно использовать существующие инструменты, такие как Aeneas, Kani, Gillian, Verus и Creusot, или предложить новые. Примеры выполненных заданий.

Источник: opennet.ru