Bug del borrow checker di Rust: cosa vuol dire soundness

Il sistema dei tipi di Rust fa una promessa precisa: se il tuo codice sicuro compila, non può avere dangling pointer, data race o use-after-free. Così, quando una issue su GitHub ha mostrato uno snippet di Rust apparentemente sicurissimo che stampa spazzatura presa da uno stack frame morto, e si è scoperto che la falla era rimasta nel borrow checker di Rust per undici anni, molti si sono sentiti mancare la terra sotto i piedi. Il bug permette che i requisiti di lifetime di una struct sfuggano tramite un'assegnazione di campo covariante e, con un'implementazione malevola di Drop, puoi nascondere un riferimento a una variabile locale in una global e leggerlo dopo che la variabile non esiste più. AddressSanitizer lo chiama stack-use-after-scope. Il compilatore lo ha considerato a posto.

Le reazioni sono state prevedibili. Qualcuno ha dichiarato morta la storia della sicurezza di Rust. Altri hanno alzato le spalle: i bug capitano. Entrambe le posizioni perdono ciò che è davvero interessante. Questo bug è un esperimento naturale pulito su quanto valgano le garanzie statiche, su dove il ragionamento informale si rompe e sul perché la distanza tra «il sistema dei tipi è corretto» e «il compilatore applica un sistema dei tipi corretto» è dove vivono i bug più interessanti. Quindi andiamo a verificare una per una le convinzioni comuni che questa storia ha fatto emergere.

Mito 1: un bug di unsoundness significa che il modello di sicurezza di Rust ha fallito

La prima reazione è trattarlo come una crepa nella teoria. Non lo è. Nessuno ha riscritto le regole dei lifetime. Nessuno ha scoperto che ownership e borrowing sono fondamentalmente rotti. Il sistema dei tipi di Rust, così come è stato progettato su lavagne e nelle RFC, dice che questo programma va rifiutato. Il compilatore semplicemente non è riuscito a rifiutarlo.

Questa distinzione, tra specifica e implementazione, è una delle faglie più antiche del nostro campo. Tony Hoare ci ha regalato una bellissima teoria dei processi sequenziali comunicanti; per decenni, i compilatori C hanno poi compilato in modo errato codice perfettamente valido secondo lo standard. La teoria regge mentre l'artefatto perde. Abbiamo già scritto di come il divario tra specifica e implementazione è dove vivono i bug, e questo è un caso da manuale. Le regole sui lifetime non erano sbagliate. Il codice di inferenza della varianza in rustc, la parte che decide quando è legittimo sostituire un &'a T dove ci si aspetta un &'static T, aveva un buco quando l'assegnazione passava attraverso un campo covariante.

Ecco, in forma semplificata, la struttura dell'exploit. Costruisci un wrapper il cui impl di Drop copia il suo payload in uno store globale 'static. Normalmente il compilatore obbliga il payload a essere 'static, quindi i riferimenti a variabili locali non possono entrarci. Il bug permette di far passare un riferimento di breve durata attraverso un'assegnazione covariante, così il wrapper finisce per contenere &l dove l è una String locale:

struct Q<T: 'static + Send>(Option<T>);
impl<T: 'static + Send> Drop for Q<T> {
fn drop(&mut self) {
if let Some(t) = self.0.take() {
KEPT.lock().unwrap().push(Box::new(t)); // escapes to 'static!
}
}
}
fn main() {
{
let l = String::from("hello world, this is long enough");
let mut q = Q(None);
q.0 = Some(&l); // should be rejected; 'static required
} // <- drop runs here, stashing &l in KEPT
// l is gone; KEPT now holds a dangling &'static String
}

Ogni singola riga sembra innocente. La unsoundness esiste solo nella composizione: un campo covariante, un'assegnazione che allenta un vincolo di lifetime e un Drop che sposta il payload in un posto dove sopravvive al suo referente. È la firma tipica dei bug di implementazione nei checker: l'invariante è globale, ma l'applicazione è locale, e un percorso di codice ha dimenticato di controllare.

Quindi no, il modello di sicurezza non ha fallito. Ha fallito l'applicazione del modello di sicurezza. È un fallimento più piccolo, ma, come vedremo, non banale.

Mito 2: undici anni senza essere scoperto significano che il bug è innocuo

Il ragionamento di triage del team di Rust è andato più o meno così: sarebbe P-critical se la gente lo incontrasse, ma undici anni senza segnalazioni significano che non deve essere facile da innescare, quindi è P-high. C'è del vero. Per causare davvero memory unsafety serve un'implementazione di Drop deliberatamente cattiva che sposti i dati in una locazione 'static. Quasi nessuno la scrive. La superficie di esposizione accidentale è minuscola.

Ma «raramente innescato per errore» sta facendo molto lavoro in quella frase. Le garanzie di sicurezza non riguardano solo gli incidenti: riguardano ciò su cui puoi contare quando il codice attorno a te non è amichevole. Il senso di un sistema dei tipi corretto è proprio che puoi ragionare in modo modulare: non devo controllare il tuo impl di Drop, perché il compilatore ha già dimostrato che certe composizioni sbagliate sono inesprimibili. Una volta che c'è una falla, quella modularità scompare. Una dipendenza malevola, o una dipendenza sbagliata in modo sottile da un autore ben intenzionato, ora può fare qualcosa che il linguaggio prometteva impossibile.

La storia è piena di bug «non sfruttabili» diventati molto sfruttabili nel momento in cui è comparso il gadget giusto. La domanda pratica, come ha osservato un commentatore, è se correggere questo romperà qualche crate reale dell'ecosistema, e la risposta è probabilmente «pochissimi o nessuno», che è una buona notizia. Ma la lezione corretta da undici anni silenziosi non è «il bug era innocuo». È che l'assenza di prove non è prova di assenza, soprattutto per i guasti che richiedono intenzione invece del caso.

Mito 3: con abbastanza occhi, tutti i bug diventano superficiali

Questo è il mito che dovrebbe imbarazzarci di più. rustc è uno dei compilatori più scrutinati mai scritti. È open source, ha un team dedicato ai tipi, una comunità accademica attiva (RustBelt ci ha dato anni fa un modello formale di un nucleo di Rust) e milioni di utenti che lo testano ogni giorno. Eppure una falla di soundness è rimasta nell'inferenza dei lifetime per più di un decennio, attraverso riscritture complete del codice circostante.

La Legge di Linus presuppone che gli occhi guardino il punto giusto con il modello giusto in testa. Le unsoundness del sistema dei tipi smentiscono entrambe le ipotesi. Vivono all'intersezione di più funzionalità (varianza, ordine di drop, coercizione, vincoli di trait) e ciascuna funzionalità è localmente corretta. I revisori leggono il codice e vedono l'invariante voluto, perché il codice è stato scritto da persone che vedevano anch'esse quell'invariante. Il bias di conferma è incorporato nel processo. Il controesempio richiede di pensare come un avversario, e ragionare in modo avversariale sulle proprie astrazioni è davvero difficile.

Esiste un intero sito, counterexamples.org, che cataloga i modi in cui regole di tipo dall'aspetto plausibile si rompono, e il filo comune è la mutabilità combinata con qualcos'altro di complicato, esattamente la forma di questo bug. Non sono lezioni nuove. Il sistema dei tipi di ML aveva una famosa unsoundness tra riferimenti mutabili e polimorfismo, risolta con la value restriction. Gli array di Java sono covarianti e possono lanciare ArrayStoreException a runtime perché i progettisti del linguaggio hanno scelto la comodità invece della soundness. Più le cose cambiano, più le stesse tre funzionalità (subtyping, mutazione e generici) si combinano per morderci. Se ti piace questo tipo di archeologia, la storia sessantennale del Lisp mostra quanto a lungo queste idee si siano evolute, e le vecchie regole di Rob Pike sulla semplicità suonano diversamente quando capisci che è nella complessità che proliferano le falle di soundness.

Gli occhi aiutano. Non bastano. La posizione onesta, che ho sentito da qualcuno che sta costruendo il proprio linguaggio, è più o meno questa: nessuna quantità di review risolve ogni problema, quindi servono metodi meccanici che non si stancano e non condividono le tue assunzioni.

Mito 4: il ragionamento informale è sostanzialmente una dimostrazione

Quando le regole sui lifetime di Rust sono state progettate, sono state discusse con attenzione, da persone brillanti, con molti esempi. Questo è ragionamento informale, ed è il modo in cui sono costruiti essenzialmente tutti i compilatori di produzione. Il risultato è un sistema corretto per quanto chiunque possa dire, che, lo abbiamo ormai imparato due volte, non è la stessa cosa che essere corretto.

Il divario tra le due cose è dove entrano in gioco progetti come RustBelt e il lavoro in corso su un solver di trait di nuova generazione. RustBelt, costruito in Coq (ora Rocq) sul framework di separation logic Iris, ha verificato meccanicamente un modello delle regole di tipizzazione del nucleo di Rust, comprese le parti più delicate come i confini di astrazione unsafe. È stato un traguardo. Ma nota cosa ha dimostrato: un modello di Rust, non rustc. La prova copre il calcolo λRust, e il compilatore di produzione si è discostato, ha accumulato funzionalità e decisioni implementative che nessuno ha riverificato. Questa issue è il conto che arriva da quella deriva.

Formalizzare l'intero compilatore di produzione è terribilmente costoso. CompCert, il compilatore C formalmente verificato, ha richiesto anni di sforzi esperti per un linguaggio molto più piccolo di Rust, e verifica i passi di compilazione invece di dimostrare che il sistema dei tipi sorgente cattura ogni programma sbagliato. Nessuno scriverà una dimostrazione in Coq per i due milioni di righe di rustc. La strada realistica assomiglia piuttosto a una difesa in profondità:

• Modelli verificati meccanicamente delle regole fondamentali (in stile RustBelt), così la teoria stessa non ha buchi.
• Fuzzing sistematico e strumenti di analisi dei casi che generano programmi avversariali, cioè gli angoli dell'interazione tra funzionalità a cui le persone non pensano di testare.
• Mutation e property-based testing del checker: se cambiare un vincolo dovrebbe far fallire un programma, verifica che fallisca. La cultura di test di SQLite è il modello da seguire qui.
• Un elenco mantenuto di problemi di unsoundness noti (Rust ne ha oltre cento etichettati) trattato come un backlog con priorità ingegneristica, non come folklore.

Curiosamente, la ricerca basata su LLM potrebbe rivelarsi un vantaggio netto: uno strumento che combina instancabilmente le funzionalità in modi perversi è esattamente l'avversario che al ragionamento informale manca. La meta che molti di noi sperano è un Rust formalmente specificato con un checker dimostrato rispetto alla specifica, ma nel frattempo il lavoro è duro, poco glamour, risoluzione di vincoli.

Mito 5: se la soundness non è assoluta, la sicurezza statica è una truffa

La lettura cinica va così: Rust prometteva sicurezza, la promessa aveva una scappatoia, quindi la promessa era marketing e tanto valeva tornare a fare YOLO con i puntatori in C. È esattamente l'opposto, e vale la pena spiegare perché con una certa precisione.

La soundness di un sistema dei tipi è un teorema su un oggetto matematico. Ciò che un linguaggio di produzione ti offre è una garanzia statistica ed economica: intere classi di bug (use-after-free, data race, invalidazione degli iteratori) passano da «radiazione di fondo costante della tua codebase» a «eventi abbastanza rari da finire in prima pagina quando vengono trovati dopo undici anni». Confronta i tassi di base. I bug di sicurezza della memoria nelle grandi codebase C e C++ costituiscono la maggioranza dei CVE gravi anno dopo anno, e ormai nessuno si stupisce più di nessuno di essi. I bug di unsoundness di Rust sono così rari che ciascuno ottiene la sua issue su GitHub, il suo thread di discussione e la sua cultura del postmortem. Una rarità che puoi enumerare è un mondo diverso da una rarità che non puoi enumerare.

C'è anche una differenza nel modo in cui i guasti si sommano. In C, ogni riga è un potenziale pericolo per la sicurezza della memoria, quindi il costo della vigilanza cresce con la dimensione del codice per sempre. In Rust, la vigilanza si concentra ai bordi: blocchi unsafe, FFI e (come ora sappiamo) il checker stesso del compilatore. È questa concentrazione che rende praticabili l'audit, strumenti come Miri e i metodi formali. La garanzia non è binaria; è una riconfigurazione drastica del punto in cui vive il tuo rischio.

Un sistema dei tipi con un bug noto che undici anni di traffico di produzione non hanno mai colpito è comunque infinitamente più forte di un linguaggio in cui il bug è il design.

Cosa dovresti portarti davvero a casa

Se scrivi Rust, non devi cambiare nulla. Il tuo codice non era silenziosamente non sicuro prima che questa issue venisse aperta; il percorso di exploit pratico richiedeva intenzione. Se mantieni librerie, la mossa onesta è sempre stata quella: tieni piccola la superficie unsafe, esegui Miri sulle parti delicate e non trattare il borrow checker come un oracolo per il codice malevolo altrui. Consideralo uno strumento estremamente affidabile per catturare i tuoi errori.

Se costruisci linguaggi o compilatori, questo bug è un regalo: un esemplare raro e ben documentato di come la soundness fallisce davvero in produzione. Non nella teoria, ma nell'applicazione; non in una singola funzionalità, ma all'incrocio tra funzionalità; non catturato dalla review, ma dalla costruzione avversariale. I team che lo prendono sul serio, finanziando riscritture del solver di trait, rielaborazioni dei vincoli sulle regioni e strumenti di verifica adiacenti, sono quelli le cui garanzie avranno un senso tra dieci anni.

E per tutti: ricalibrate cosa sia una garanzia. Per decenni abbiamo confuso «dimostrato» con «argomentato in modo convincente e mai ancora smentito», nei sistemi di tipi, nei protocolli crittografici e nel consenso distribuito. La versione adulta della fiducia non consiste nel presumere che il ponte sia perfetto. Consiste nel sapere che il ponte ha ispettori che pubblicano i loro risultati, correggono ciò che trovano e tengono una lista pubblica delle crepe che non hanno ancora sistemato. Da questo punto di vista, undici anni per trovare una falla non sono un'accusa. Sono la prova che il sistema, quello umano attorno al compilatore, funziona più o meno come dovrebbe.