Amazon en de Rust Foundation hebben een initiatief gepresenteerd dat gericht is op het verhogen van de veiligheid van de standaardbibliotheek van de programmeertaal Rust. Het doel is om de betrouwbaarheid en veiligheid van functies te controleren waarin het sleutelwoord 'unsafe' wordt gebruikt, wat operaties toestaat die onveilig met geheugen omgaan, zoals het dereferencen van pointers, het wijzigen van statische variabelen en het aanroepen van externe bibliotheken in C/C++. Momenteel bevat de standaardbibliotheek van Rust ongeveer 35.000 functies, waarvan er in 7.500 codeblokken voorkomen die in de context van 'unsafe' worden uitgevoerd. In de afgelopen drie jaar zijn er 57 problemen met de correctheid van de bibliotheek ontdekt, waarvan 20 als kwetsbaarheden zijn gemarkeerd.
Het werk aan de controle van de bibliotheek is georganiseerd in de vorm van een wedstrijd, waarin deelnemers verschillende taken krijgen aangeboden die verband houden met het uitvoeren van bepaalde controles om veilige geheugenwerking van Rust-bibliotheken te bevestigen of met de ontwikkeling van tools voor het automatiseren van dergelijke controles. Succesvolle voltooiing van de controledoelstelling (het bieden van formeel bewijs van betrouwbaarheid) omvat een beloningspaycheck. Voor het uitvoeren van experimenten en het publiceren van werkresultaten is er een repository aangemaakt, die een tak van de reguliere Rust-repository vertegenwoordigt.
Momenteel zijn er 13 opdrachten voorgesteld. Bijvoorbeeld, in een van de opdrachten wordt gevraagd om de veiligheid van het werken met raw pointers in de functies van de module core::ptr te verifiƫren en formeel bewijs te leveren van de correctheid van pointerbewerkingen. Voor verificatie kunnen bestaande tools worden gebruikt, zoals Aeneas, Kani, Gillian, Verus en Creusot, of nieuwe worden voorgesteld. Voorbeelden van uitgevoerde opdrachten.
Bron: opennet.ru
