🔥 Rust Foundation и Amazon проверят 7500 функций языка Rust на дыры

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

Особое внимание будет уделено функциям, использующим ключевое слово unsafe, которое допускает небезопасные операции с памятью. Сейчас таких функций насчитывается около 7500 из 35 000 функций библиотеки.

Почему это важно

Несмотря на высокую репутацию Rust как безопасного языка программирования, блоки unsafe позволяют выполнять критические операции, такие как разыменование указателей или вызов библиотек на C/C++, что создаёт потенциальные риски.

За последние три года было выявлено 57 проблем в стандартной библиотеке, 20 из которых классифицированы как уязвимости.

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

Как будет организована работа

Проект реализуется в формате конкурса.

Участники могут решать предложенные задачи, связанные с верификацией кода или разработкой инструментов автоматизации проверки. За успешное выполнение задач предусмотрено вознаграждение.

На данный момент доступно 13 заданий, каждое из которых требует предоставления формальных доказательств корректности работы функций.

Например, одна из задач предполагает анализ работы с raw-указателями в модуле core::ptr. Участникам предлагается использовать существующие инструменты, такие как Aeneas, Kani, Verus и Creusot, или предложить собственные подходы.

Что дальше

Для экспериментов создан отдельный репозиторий, где публикуются результаты и прогресс по задачам.

Эта инициатива может стать важным шагом в развитии Rust, сделав его ещё более надёжным инструментом для разработки программного обеспечения.