RustyDL: A Program Logic for Rust

Probleemstelling

Rust is een moderne programmeertaal die memory safety en de afwezigheid van data races garandeert via een sterk typesysteem met eigenaarschaps- (ownership) en borrowing-mechanismen. Hoewel er reeds diverse tools bestaan voor het formeel verifiëren van Rust-code, vertonen deze een gemeenschappelijke beperking: ze werken voornamelijk op basis van vertaling naar een tussenliggende taal (zoals Viper of Why3).

• Nadeel van vertaling: Deze aanpak vereist dat men de complexiteit van de vertaling naar een tussenliggende taal moet vertrouwen. Bovendien maakt het interactieve bewijzen (Human-in-the-Loop of HIL) moeilijk, omdat fouten in een SMT-oplosser niet direct gekoppeld kunnen worden aan de broncode.
• Het gat: Er ontbreekt een deductieve verifiër voor Rust die op broncode-niveau werkt en menselijke interactie toelaat om complexe functionele eigenschappen te bewijzen, vergelijkbaar met wat er voor Java mogelijk is met tools zoals KeY.

Methodologie

De auteurs introduceren RustyDL, een programmalogica specifiek ontworpen voor Rust, die als basis dient voor een deductieve verifiër. De kern van de methodologie is het modelleren van Rust's unieke kenmerken direct in een dynamische logica, zonder vertaling naar een tussenliggende taal.

1. RustyDL (Dynamic Logic):

   • Het is een extensie van getypeerde first-order logica.
   • Het gebruikt een sequent calculus om correctheid te bewijzen.
   • Het modelleert Rust's typesysteem, inclusief bool, gehele getallen, arrays, en crucialer: shared (&) en mutable (&mut) referenties.
   • Het focust op Safe Rust, waarbij unsafe-code als afgescheiden wordt beschouwd.

2. Belangrijkste Uitbreidingen ten opzichte van bestaande logica (zoals JavaDL):

   • Mutating Updates: Om mutable referenties te modelleren zonder expliciet geheugen of "loans" (leningen) te hoeven bijhouden, introduceert RustyDL een nieuw type update: t1 ∗→ t2. Dit betekent dat de waarde op de locatie die door t1 wordt gehuurd, wordt gewijzigd naar t2. Dit vermijdt de complexiteit van het handmatig bijwerken van een set actieve leningen bij elke state change.
   • Ownership en Move Semantics: Bij toewijzingen waarbij een waarde wordt verplaatst (move), wordt de bronvariabele niet als "ongedefinieerd" gemarkeerd, maar wordt deze vervangen door een Skolem-constante (een anonieme waarde). Dit voorkomt dat de logica constant moet controleren of een variabele nog geldig is.
   • Integer Overflow: De logica hanteert de debug-semantiek van Rust, waarbij integer overflow leidt tot een panic. De calculus splitst bewijzen in gevallen: of de som valt binnen de bereiksgrenzen (update), of er treedt een panic op.
   • Loop Scopes: Om complexe loop-controle (zoals break met een waarde, continue, en panic) te hanteren, gebruiken de auteurs het concept van "loop scopes". Dit stelt de logica in staat om een generieke iteratie symbolisch uit te voeren en de reden voor het verlaten van de lus te registreren via een indexvariabele.

3. Implementatie:

   • De logica is geïmplementeerd als een prototype op het bestaande deductieve verificatie-platform KeY.
   • De regels zijn geschreven in de taal "taclets", wat het mogelijk maakt om ze te reviewen en mechanisch te valideren.

Kernbijdragen

• RustyDL: De eerste programmalogica voor Rust die werkt op het niveau van de broncode en geschikt is voor Human-in-the-Loop (HIL) verificatie.
• Modellering van Ownership en Referenties: Een elegante oplossing voor het modelleren van Rust's borrowing-mechanismen via "mutating updates" in plaats van complexe geheugenmodellen.
• Sequent Calculus: Een volledig gedefinieerde calculus die symbolische executie ondersteunt voor Rust-specifieke constructies (if-else, loops, arrays, referenties).
• Proof-of-Concept: Een werkend prototype ("Rusty KeY") dat diverse voorbeelden kan verifiëren, waaronder binaire zoekalgoritmes met loops en referenties.

Resultaten

• Het prototype is succesvol gebruikt om diverse Rust-functies te verifiëren, waaronder functies met loops, arrays, tuples en referenties.
• Een opvallend resultaat is de verificatie van een binaire zoekopdracht, waarbij een bewijs werd gegenereerd van 4260 regeltoepassingen in slechts 2,1 seconden.
• De aanpak toont aan dat het mogelijk is om complexe, ongewijzigde Rust-broncode te verifiëren met behoud van menselijke controle over het bewijsproces, iets wat met vertalingsgebaseerde systemen tot nu toe niet mogelijk was.

Betekenis en Toekomstperspectief

Dit paper is significant omdat het de brug slaat tussen de krachtige, automatische deductieve verificatie (zoals bij Java met KeY) en de moderne, veilige Rust-taal. Het bewijst dat Rust's complexe typesysteem en eigenaarschapsregels kunnen worden geformaliseerd in een logisch kader dat geschikt is voor interactief bewijzen.

Toekomstig werk omvat:

• Uitbreiding van de ondersteunde Rust-subset (Traits, iterators, pattern matching, generieke functies).
• Onderzoek naar het verifiëren van unsafe Rust, wat waarschijnlijk een explicieter geheugenmodel vereist.
• Verbetering van de implementatie, waaronder een grafische gebruikersinterface en een meer uitgebreide specificatietaal (vergelijkbaar met JML).

Samenvattend biedt RustyDL een fundamentele stap naar betrouwbare, mens-gestuurde formele verificatie van kritieke Rust-software, waarbij de complexiteit van de taal direct in de logica wordt opgelost in plaats van via een omweg.