Amazon og Rust Foundation har introdusert et initiativ som tar sikte på å forbedre sikkerheten til Rust-standardbiblioteket. Det uttalte målet er å sjekke påliteligheten og sikkerheten til funksjoner som bruker nøkkelordet «usikkert», som tillater operasjoner som fungerer usikkert med minne, for eksempel dereferensing av pekere, endring av statiske variabler og oppkalling av eksterne biblioteker i C/C++. Det bemerkes at for øyeblikket har standard Rust-biblioteket omtrent 35 tusen funksjoner, hvorav 7500 inneholder kodeblokker utført i den "usikre" konteksten. I løpet av de siste tre årene er det identifisert 57 problemer med korrekt drift i biblioteket, hvorav 20 ble flagget som sårbarheter.
Bibliotekverifiseringsarbeidet er organisert i form av en konkurranse, der deltakerne tilbys ulike oppgaver knyttet til å utføre visse kontroller for å bekrefte sikker drift av Rust-biblioteker med minne eller til å utvikle verktøy for å automatisere slike kontroller. Vellykket fullføring av verifiseringsmålet (gi formelle bevis på pålitelighet) innebærer utbetaling av en belønning. For å gjennomføre eksperimenter og publisere resultatene av arbeidet er det opprettet et depot, som er en gren av standard Rust-depot.
Foreløpig er 13 oppgaver foreslått for løsning. For eksempel, i en av oppgavene foreslås det å verifisere sikkerheten ved å jobbe med råpekere i funksjonene til kjernen::ptr-modulen og gi et formelt bevis på riktigheten av operasjoner med pekere. For verifisering kan du bruke eksisterende verktøy som Aeneas, Kani, Gillian, Verus og Creusot, eller foreslå nye. Eksempler på utførte oppgaver.
Kilde: opennet.ru
