L'azienda Amazon e l'organizzazione Rust Foundation hanno presentato un'iniziativa finalizzata a migliorare la sicurezza della libreria standard del linguaggio Rust. L'obiettivo dichiarato è la verifica dell'affidabilità e della sicurezza delle funzioni che utilizzano la parola chiave "unsafe", che consentono operazioni che lavorano in modo insicuro con la memoria, come la dereferenziazione di puntatori, la modifica di variabili statiche e l'accesso a librerie esterne in C/C++. Si segnala che attualmente la libreria standard di Rust conta circa 35.000 funzioni, delle quali in 7.500 si trovano blocchi di codice eseguiti nel contesto "unsafe". Negli ultimi tre anni sono stati identificati 57 problemi di correttezza, di cui 20 sono stati contrassegnati come vulnerabilità.
Il lavoro di verifica della libreria è organizzato sotto forma di gara, ai partecipanti vengono proposte diverse sfide legate all'esecuzione di specifiche verifiche per confermare il corretto funzionamento in sicurezza della memoria delle librerie Rust o lo sviluppo di strumenti per l'automazione di tali verifiche. Il successo nel raggiungimento dell'obiettivo di verifica (fornire una prova formale di affidabilità) prevede un premio monetario. È stato creato un repository per condurre esperimenti e pubblicare i risultati, che è un fork del repository ufficiale di Rust.
Attualmente sono stati proposti 13 compiti. Ad esempio, in uno dei compiti si propone di verificare la sicurezza dell'uso di puntatori raw nelle funzioni del modulo core::ptr e di fornire una prova formale di correttezza delle operazioni con i puntatori. Per la verifica possono essere utilizzati strumenti esistenti, come Aeneas, Kani, Gillian, Verus e Creusot, oppure è possibile proporre nuove soluzioni. Esempi di compiti completati.
Fonte: opennet.ru
