Rust typ system garanterar minnet säkerhet: välskrivna Rust program är garanterade att inte uppvisa problem som dingel pekare, data races, och oväntade biverkningar genom aliaserade referenser. För att säkerställa korrekta egenskaper utöver minnessäkerheten, t.ex. den garanterade frånvaron av påståendesfel eller mer allmän funktionell korrekthet, krävs statisk programverifiering. För traditionella systemprogrammeringsspråk är formell verifiering notoriskt svår och kräver komplexa specifikationer och logiker för att resonera om pekare, alias och sidoeffekter på muterbara tillstånd. Denna komplexitet är ett stort hinder för en mer omfattande verifiering av systemprogramvara. I detta dokument presenterar vi en ny verifieringsteknik som utnyttjar Rusts typsystem för att avsevärt förenkla specifikationen och verifieringen av systemprogramvaran skriven i Rust. Vi analyserar information från Rust kompilatorn och syntetiserar ett motsvarande kärnbevis för programmet i en smak av separationslogik skräddarsydd för automatisering. För att verifiera korrekthetsegenskaper bortom minnessäkerhet, kan användare kommentera Rust-program med specifikationer på abstraktionsnivå av Rust-uttryck; vår teknik väver in dem i kärnan bevis för att kontrollera modulärt om dessa specifikationer håller. Avgörande är att våra bevis konstrueras och kontrolleras automatiskt utan att avslöja den underliggande formella logiken, vilket gör det möjligt för användare att arbeta uteslutande på abstraktionsnivå av programmeringsspråket. Som sådan möjliggör vårt arbete en ny typ av verifieringsverktyg, med potential att påverka en bred publik och göra det möjligt för Rust-gemenskapen att dra nytta av toppmoderna verifieringstekniker. Vi har implementerat våra tekniker för en delmängd av Rust; vår utvärdering av flera tusen funktioner från allmänt använda Rust lådor visar dess effektivitet. (4) Vi automatiserar vår verifieringsteknik genom att konstruera en översättning från Rust-programmet och specifikationer till Vipers mellanliggande verifieringsspråk [Müller et al. År 2016 ]. Vår översättning genererar korrekta specifikationer och, avgörande, synteser alla nödvändiga hjälpanteckningar som behövs för att beviskontroll ska vara helt automatisk. (5) Vi tillhandahåller en implementering av vår teknik som en plugin för Rust kompilatorn. Vi använde vår implementering för att automatiskt konstruera kärnproofer för flera tusen oannoterade Rust-funktioner, och för att verifiera en rad starkare egenskaper (via vårt specifikationsspråk) för utvalda Rust-program. Vårt verktyg finns som artefakt [Astrauskas et al. Denna förordning träder i kraft den tjugonde dagen efter det att den har offentliggjorts i Europeiska unionens officiella tidning. Osäker kod och RustBelt. Rust typ system upprätthåller starka regler, men ger en utrymningslucka för när dessa är alltför restriktiva: kodblock och funktioner kan förklaras osäkra, försvaga kompilatorns kontroller, och på motsvarande sätt riskera de garantier de ger. Osäker kod bör inkapslas av bibliotek så att klientkoden inte kan observera dess användning [Rust bidragsgivare 2019b]. Det pågående RustBelt-projektet [Jung et al. 2018 ] syftar till att definiera formella semantiska grunder för att göra detta krav exakt och kontrollerbar. Vårt arbete har i grunden olika (och kompletterande) mål och tekniska bidrag. Vi tar inte upp osäkra koder i detta dokument, utan presenterar en verifieringsteknik som möjliggör användarspecifikationer på en hög nivå av abstraktion och automatiska bevis; RustBelt-verifiering innebär direkt användning av en avancerad separationslogik baserad på Iris [Jung et al. 2015], för vilka bevis är interaktiva (i Coq [Coq Team 2014]), och konstruerade av experter (se även Sec. 8) och av följande skäl:
Astrauskas m.fl. REF föreslog en teknik som kan hjälpa utvecklare att verifiera sina program med formella metoder.
Leveraging rust types for modular specification and verification
{'venue': 'PACMPL', 'journal': None, 'mag_field_of_study': ['Computer Science']}