Společnost Amazon a organizace Rust Foundation představily iniciativu zaměřenou na zvýšení bezpečnosti standardní knihovny jazyka Rust. Cílem je prověřit spolehlivost a bezpečnost funkcí, ve kterých se používá klíčové slovo „unsafe“, umožňující operace, které nebezpečně pracují s pamětí, jako je dereference ukazatelů, změna statických proměnných a přístup k externím knihovnám v C/C++. Je poznamenáno, že v současné době standardní knihovna Rust obsahuje přibližně 35 tisíc funkcí, z nichž 7500 obsahuje bloky kódu prováděné v kontextu „unsafe“. Během posledních tří let bylo v knihovně identifikováno 57 problémů s funkčností, z nichž 20 bylo označeno za zranitelnosti.
Práce na prověřování knihovny je organizována ve formě soutěže, jejímž účastníkům jsou nabízena různá zadání týkající se provádění konkrétních kontrol k potvrzení bezpečného zacházení s pamětí knihoven Rust nebo vývoje nástrojů pro automatizaci podobných kontrol. Úspěšné splnění cíle prověřování (poskytnutí formálního důkazu spolehlivosti) zahrnuje vyplacení odměny. Pro provádění experimentů a publikaci výsledků byla vytvořena repozitář, představující odnož od standardního repozitáře Rust.
V současné době bylo navrženo 13 úkolů. Například v jednom z úkolů se požaduje ověření bezpečnosti práce s raw ukazateli ve funkcích modulu core::ptr a poskytnout formální důkaz správnosti operací s ukazateli. K verifikaci lze použít existující nástroje, jako jsou Aeneas, Kani, Gillian, Verus a Creusot, nebo navrhnout nové. Příklady realizovaných úkolů.
Zdroj: opennet.ru
