Spoločnosť Amazon a organizácia Rust Foundation predstavili iniciatívu zameranú na zvýšenie bezpečnosti štandardnej knižnice programovacieho jazyka Rust. Cieľom je overenie spoľahlivosti a bezpečnosti funkcií, v ktorých sa používa kľúčové slovo „unsafe“, umožňujúce operácie, ktoré bezpečne nepracujú s pamäťou, ako je dereferencovanie ukazovateľov, zmena statických premenných a volanie externých knižníc v C/C++. Uvádza sa, že v súčasnosti má štandardná knižnica Rust približne 35 tisíc funkcií, z ktorých v 7500 sa nachádzajú bloky kódu vykonávané v kontexte „unsafe“. Za posledné tri roky sa v knižnici objavilo 57 problémov s korektnosťou fungovania, z ktorých 20 bolo označených ako zraniteľnosti.
Práca na overovaní knižnice je organizovaná formou súťaže, v ktorej účastníci dostávajú rôzne úlohy súvisiace s vykonávaním určitých kontrol na potvrdenie bezpečnej práce s pamäťou knižníc Rust alebo s vývojom nástrojov na automatizáciu podobných overení. Úspešné splnenie cieľa overenia (poskytovanie formálneho dôkazu spoľahlivosti) predpokladá vyplatenie odmeny. Na vykonávanie experimentov a publikovanie výsledkov práce bol vytvorený repozitár, ktorý predstavuje odklon od štandardného repozitára Rust.
V súčasnosti je na riešenie navrhnutých 13 úloh. Napríklad v jednej z úloh je potrebné overiť bezpečnosť práce s raw ukazovateľmi vo funkciách modulu core::ptr a poskytnúť formálny dôkaz korektnosti operácií s ukazovateľmi. Na verifikáciu je možné použiť existujúce nástroje, ako sú Aeneas, Kani, Gillian, Verus a Creusot, alebo navrhnúť nové. Príklady vykonaných úloh.
Zdroj: opennet.ru
