Amazon e la Rust Foundation hanno lanciato un'iniziativa per migliorare la sicurezza della libreria standard del linguaggio Rust. L'obiettivo è controllare l'affidabilità e la sicurezza delle funzioni che utilizzano la parola chiave "unsafe", che consente operazioni che non sono sicure nell'interazione con la memoria, come il dereferenziamento di puntatori, la modifica di variabili statiche e l'accesso a librerie esterne in C/C++. Attualmente, si stima che la libreria standard Rust contenga circa 35.000 funzioni, di cui 7.500 comprendono porzioni di codice eseguite nel contesto "unsafe". Negli ultimi tre anni sono stati identificati 57 problemi di correttezza nella libreria, di cui 20 sono stati contrassegnati come vulnerabilità.
Il lavoro di verifica della libreria è organizzato come un concorso, dove i partecipanti sono invitati a svolgere vari compiti legati all'esecuzione di determinate verifiche per garantire un'operazione sicura della libreria Rust in relazione alla memoria, o allo sviluppo di strumenti per l'automazione di simili verifiche. Il successo nel raggiungimento dell'obiettivo di verifica (fornire una prova formale di affidabilità) prevede un premio. Per condurre esperimenti e pubblicare i risultati del lavoro, è stato creato un repository che rappresenta un fork del repository ufficiale di Rust.
Attualmente sono stati proposti 13 compiti. Ad esempio, in uno di questi si chiede di accertarsi della sicurezza del lavoro con i raw-pointer nelle funzioni del modulo core::ptr e fornire una prova formale della correttezza delle operazioni con i puntatori. Per la verifica si possono utilizzare strumenti esistenti come Aeneas, Kani, Gillian, Verus e Creusot, oppure proporre nuovi strumenti. Esempi di compiti completati.
Fonte: opennet.ru
