Compania Amazon și organizația Rust Foundation au lansat o inițiativă vizând creșterea securității bibliotecii standard a limbajului Rust. Scopul acesteia este de a verifica fiabilitatea și securitatea funcțiilor care utilizează cuvântul cheie „unsafe”, permițând operațiuni nesigure cu memoria, cum ar fi dereferentierea pointerilor, modificarea variabilelor statice și accesarea bibliotecilor externe scrise în C/C++. Se observă că în prezent biblioteca standard Rust conține aproximativ 35 de mii de funcții, dintre care în 7500 se întâlnesc blocuri de cod executate în contextul „unsafe”. În ultimii trei ani, în bibliotecă au fost identificate 57 de probleme de corectitudine, dintre care 20 au fost marcate ca vulnerabilități.
Lucrările de verificare a bibliotecii sunt organizate sub forma unui concurs, în care participanții sunt provocați cu diverse sarcini legate de realizarea anumitor verificări pentru a confirma operarea sigură cu memoria bibliotecilor Rust sau de a dezvolta instrumente pentru automatizarea acestor verificări. Realizarea cu succes a scopului de verificare (furnizarea unei dovezi formale a fiabilității) prevede o recompensă. Pentru desfășurarea experimentelor și publicarea rezultatelor lucrării a fost creat un repository, care reprezintă un fork al repository-ului standard Rust.
În prezent, pentru soluționare sunt propuse 13 sarcini. De exemplu, într-una dintre sarcini este solicitată asigurarea că lucrul cu pointerii raw în funcțiile modulului core::ptr este sigur și furnizarea unei dovezi formale a corectitudinii operațiunilor cu pointerii. Pentru verificare, pot fi utilizate instrumente existente, cum ar fi Aeneas, Kani, Gillian, Verus și Creusot, sau pot fi propuse altele noi. Exemple de sarcini finalizate.
Sursa: opennet.ro
