RustyDL: A Program Logic for Rust

Titolo

RustyDL: Una logica di programma per Rust

1. Il Problema

Rust è un linguaggio di programmazione moderno che garantisce la sicurezza della memoria e l'assenza di race condition attraverso un sistema di tipi forte, basato su proprietà (ownership), prestiti (borrowing) e riferimenti. Nonostante la sua popolarità crescente (incluso l'uso nel kernel Linux), la verifica formale dei programmi Rust presenta sfide significative.

La maggior parte degli strumenti esistenti per la verifica formale di Rust (come Creusot, Prusti, Aeneas) adotta un approccio basato sulla traduzione: il codice sorgente Rust e le specifiche vengono tradotti in un linguaggio intermedio (es. Viper, Why3) che viene poi analizzato da solver SMT (Satisfiability Modulo Theories).
Questo approccio presenta due svantaggi principali:

1. Fiducia nella traduzione: È necessario fidarsi della correttezza della traduzione da Rust a un linguaggio intermedio, che è un processo complesso e non banale.
2. Mancanza di interazione umana (Human-in-the-Loop - HIL): Se la verifica fallisce, è difficile collegare l'output del solver SMT al codice sorgente originale. L'ingegnere di verifica non può interagire direttamente con la prova o applicare passaggi manuali per guidare la verifica di proprietà funzionali complesse.

Attualmente, non esiste un verificatore deduttivo di livello sorgente per Rust che supporti lo stile HIL, a differenza di strumenti per Java come KeY o KIV.

2. Metodologia

Gli autori propongono RustyDL, una logica di programma dinamica (Dynamic Logic) progettata specificamente per il codice sorgente Rust, come base per uno strumento di verifica deduttiva interattiva. La metodologia si articola nei seguenti punti:

• Logica al Livello Sorgente: RustyDL opera direttamente sul codice Rust (o su una sua rappresentazione intermedia ad alto livello, HIR), evitando la traduzione in linguaggi intermedi.
• Estensione della Logica Dinamica: RustyDL è un'estensione della logica dinamica tipizzata di primo ordine, ispirata a JavaDL (per Java). Introduce un calcolo dei sequenti che permette di decomporre i programmi in passi simbolici.
• Gestione delle Sfide di Rust: Il calcolo affronta le caratteristiche uniche di Rust:
  • Ownership e Move Semantics: Gestisce il trasferimento di proprietà delle variabili (es. quando una variabile viene "mossa" e non più accessibile).
  • Riferimenti Mutabili e Condivisi: Introduce un concetto innovativo di aggiornamenti mutanti (mutating updates) per modellare i riferimenti mutabili (&mut) senza dover esplicitamente tracciare lo stato di tutti i prestiti attivi (loans), sfruttando invece le garanzie del borrow checker del compilatore Rust.
  • Semantica degli Interi: Modella il comportamento degli interi in modalità debug (dove l'overflow causa un panic) e release (dove l'overflow è definito come wrap-around), focalizzandosi sulla sicurezza (assenza di overflow).
  • Cicli e Controllo del Flusso: Utilizza il concetto di "loop scope" per gestire cicli che possono terminare tramite break, return o panic, permettendo l'uso di invarianti di ciclo in modo conciso.
• Implementazione Prototipale: L'implementazione è realizzata come un'estensione dello strumento di verifica deduttiva KeY, utilizzando il linguaggio "taclets" per definire le regole del calcolo.

3. Contributi Chiave

1. RustyDL (La Logica): La definizione formale di una logica dinamica per Rust che include:
   • Una gerarchia di tipi (sorts) che mappa i tipi Rust (interi, array, riferimenti condivisi e mutabili) in tipi logici.
   • Operatori modali per la correttezza parziale e totale.
   • Mutating Updates: Un'estensione cruciale che permette di aggiornare direttamente la posizione (place) di un valore preso in prestito, risolvendo il problema di modellare i riferimenti mutabili senza un modello di memoria esplicito e ingombrante.
2. Calcolo dei Sequenti: Un insieme di regole di inferenza per l'esecuzione simbolica che gestisce:
   • Istruzioni condizionali (if-else).
   • Assegnazioni con move e copy.
   • Creazione e dereferenziazione di riferimenti.
   • Accesso agli array (con controllo dei limiti).
   • Cicli con invarianti.
3. Prototipo Rusty KeY: Un'implementazione funzionante basata su KeY che dimostra la fattibilità dell'approccio.
4. Analisi delle Sfide: Una discussione dettagliata su come modellare l'ownership, i riferimenti e la semantica degli interi in un contesto di verifica interattiva.

4. Risultati

• Dimostrazione di Fattibilità: Gli autori hanno dimostrato che è possibile trasferire l'approccio HIL di verifica al livello sorgente nel mondo di Rust.
• Verifica di Esempi Complessi: Il prototipo è stato utilizzato per verificare con successo diverse funzioni Rust, inclusi algoritmi con cicli, riferimenti mutabili e array.
• Caso di Studio: È stata eseguita la verifica di un algoritmo di ricerca binaria, che ha generato una prova di 4260 applicazioni di regole in soli 2,1 secondi, dimostrando l'efficienza del sistema.
• Gestione della Complessità: Il sistema è riuscito a gestire la complessità delle regole di borrowing e ownership senza richiedere all'utente di specificare manualmente lo stato di tutti i prestiti attivi, delegando tale responsabilità al fatto che il codice sia già stato approvato dal compilatore Rust.

5. Significato e Implicazioni

Il lavoro di Drodt e Hähnle è significativo per diversi motivi:

• Superamento delle Limitazioni delle Traduzioni: Offre un'alternativa agli approcci basati sulla traduzione, eliminando il rischio di errori di traduzione e permettendo una tracciabilità diretta tra il codice sorgente e la prova formale.
• Abilitazione della Verifica Interattiva: Permette agli ingegneri di verificare proprietà funzionali altamente complesse che gli strumenti automatici basati su SMT faticano a gestire, offrendo controllo granulare sul processo di prova.
• Modellazione Elegante dei Riferimenti: L'uso degli mutating updates rappresenta un contributo teorico importante per la logica dei programmi, offrendo un modo efficiente per modellare la mutabilità senza sovraccarico computazionale.
• Futuro della Verifica Rust: Stabilisce le basi per un ecosistema di verifica deduttiva per Rust che possa scalare verso librerie complesse e codice critico per la sicurezza, aprendo la strada a futuri lavori su tipi generici, pattern matching e Rust "unsafe".

In sintesi, RustyDL rappresenta un passo fondamentale verso la maturità della verifica formale per Rust, spostando il paradigma da una verifica puramente automatica basata su traduzioni a una verifica collaborativa uomo-macchina basata sul codice sorgente.