{"id":120678,"date":"2024-11-24T15:46:00","date_gmt":"2024-11-24T13:46:00","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/inicziativa-po-verifikaczii-standartnoj-biblioteki-rust"},"modified":"2024-11-24T15:46:00","modified_gmt":"2024-11-24T13:46:00","slug":"inicziativa-po-verifikaczii-standartnoj-biblioteki-rust","status":"publish","type":"post","link":"https:\/\/prohoster.info\/it\/blog\/news\/inicziativa-po-verifikaczii-standartnoj-biblioteki-rust","title":{"rendered":"Iniziativa per la verifica della libreria standard di Rust","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Amazon e la Rust Foundation hanno lanciato un'iniziativa mirata a migliorare la sicurezza della libreria standard del linguaggio Rust. L'obiettivo \u00e8 verificare l'affidabilit\u00e0 e la sicurezza delle funzioni che utilizzano la parola chiave \"unsafe\", che consente operazioni non sicure relative alla memoria, come la dereferenziazione di puntatori, la modifica di variabili statiche e l'accesso a librerie esterne in C\/C++. Si osserva che attualmente la libreria standard di Rust conta circa 35.000 funzioni, di cui 7.500 contengono blocchi di codice eseguiti nel contesto di \"unsafe\". Negli ultimi tre anni sono stati individuati 57 problemi di correttezza nella libreria, di cui 20 sono stati contrassegnati come vulnerabilit\u00e0. <\/p>\n
Il lavoro di verifica della libreria \u00e8 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\u00e0) prevede un premio monetario. \u00c8 stato creato un repository per condurre esperimenti e pubblicare i risultati, che \u00e8 un fork del repository ufficiale di Rust. <\/p>\n
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 \u00e8 possibile proporre nuove soluzioni. Esempi di compiti completati. \n Fonte: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"