Amazon och Rust Foundation har introducerat ett initiativ som syftar till att förbÀttra sÀkerheten för Rust-standardbiblioteket. Det uttalade mÄlet Àr att kontrollera tillförlitligheten och sÀkerheten för funktioner som anvÀnder nyckelordet "osÀkert", vilket tillÄter operationer som fungerar osÀkert med minnet, som t.ex. referenspekare, Àndra statiska variabler och anropa externa bibliotek i C/C++. Det noteras att för nÀrvarande har standardbiblioteket Rust cirka 35 tusen funktioner, varav 7500 innehÄller kodblock som körs i det "osÀkra" sammanhanget. Under de senaste tre Ären har 57 problem med korrekt drift identifierats i biblioteket, varav 20 flaggades som sÄrbarheter.
Biblioteksverifieringsarbetet organiseras i form av en tÀvling, dÀr deltagarna erbjuds olika uppgifter relaterade till att utföra vissa kontroller för att bekrÀfta sÀker drift av Rust-bibliotek med minne eller att utveckla verktyg för att automatisera sÄdana kontroller. FramgÄngsrikt slutförande av verifieringsmÄlet (ge formella bevis pÄ tillförlitlighet) innebÀr betalning av en belöning. För att genomföra experiment och publicera resultatet av arbetet har ett förvar skapats, som Àr en gren av standardförvaret Rust.
För nÀrvarande har 13 uppgifter föreslagits för lösning. Till exempel, i en av uppgifterna föreslÄs det att verifiera sÀkerheten för att arbeta med rÄpekare i funktionerna i kÀrnan::ptr-modulen och tillhandahÄlla ett formellt bevis pÄ riktigheten av operationer med pekare. För verifiering kan du anvÀnda befintliga verktyg som Aeneas, Kani, Gillian, Verus och Creusot, eller föreslÄ nya. Exempel pÄ utförda uppgifter.
KĂ€lla: opennet.ru
