Rust Borrow Checker Bug: Was Soundness wirklich bedeutet

Rusts Typsystem gibt ein klares Versprechen: Wenn dein sicherer Code kompiliert, kann er keine hängenden Pointer, Data Races oder Use-after-free enthalten. Als ein GitHub-Issue ein Snippet zeigte, das völlig sicher aussieht und Müll aus einem toten Stack-Frame ausgibt, und sich herausstellte, dass die Lücke seit elf Jahren im Rust Borrow Checker steckte, geriet bei vielen der Boden ins Wanken. Der Bug lässt die Lifetime-Anforderungen eines Structs durch covariante Feldzuweisung durchrutschen. Mit einer bösartigen Drop-Implementierung kann man eine Referenz auf eine lokale Variable in einem globalen Speicher ablegen und sie lesen, nachdem die Variable verschwunden ist. AddressSanitizer nennt das stack-use-after-scope. Der Compiler fand das in Ordnung.

Die Reaktionen waren vorhersehbar. Manche erklärten Rusts Sicherheitsversprechen für tot. Andere zuckten mit den Schultern: Bugs passieren eben. Beide verpassen, was hier wirklich spannend ist. Dieser Bug ist ein sauberes natürliches Experiment darüber, was statische Garantien wert sind, wo informelles Schlussfolgern versagt und warum die Distanz zwischen „das Typsystem ist sound“ und „der Compiler erzwingt ein soundes Typsystem“ der Ort ist, an dem die interessantesten Bugs leben. Schauen wir uns also die gängigen Überzeugungen an, die diese Geschichte aufgewirbelt hat, und testen jede einzelne.

Mythos 1: Ein Unsoundness-Bug bedeutet, dass Rusts Sicherheitsmodell versagt hat

Der erste Instinkt ist, das als Riss in der Theorie zu behandeln. Ist es aber nicht. Niemand hat die Lifetime-Regeln umgeschrieben. Niemand hat entdeckt, dass Ownership und Borrowing grundlegend kaputt sind. Das Rust-Typsystem, so wie es auf Whiteboards und in RFCs entworfen wurde, sagt: Dieses Programm muss abgelehnt werden. Der Compiler hat es nur nicht abgelehnt.

Diese Unterscheidung, Spezifikation versus Implementierung, ist eine der ältesten Bruchlinien in unserem Feld. Tony Hoare lieferte uns eine wunderschöne Theorie sequenzieller kommunizierender Prozesse; Jahrzehnte später miscompilierten C-Compiler Code, der nach dem Standard völlig gültig war. Die Theorie hält, während das Artefakt leckt. Wir haben schon früher geschrieben, dass die Lücke zwischen Spezifikation und Implementierung der Ort ist, an dem Bugs leben, und das hier ist ein Lehrbuchbeispiel. Die Lifetime-Regeln waren nicht falsch. Der Varianz-Inferenzcode in rustc, also der Teil, der entscheidet, wann es legal ist, ein &'a T dort einzusetzen, wo ein &'static T erwartet wird, hatte eine Lücke, wenn die Zuweisung über ein covariantes Feld lief.

So sieht der Exploit vereinfacht aus. Du baust einen Wrapper, dessen Drop-Implementierung seine Nutzlast in einen globalen 'static-Speicher kopiert. Normalerweise zwingt der Compiler die Nutzlast dazu, 'static zu sein, sodass Referenzen auf lokale Variablen nicht hineinkommen. Der Bug erlaubt es, eine kurzlebige Referenz über eine covariante Zuweisung einzuschleusen, sodass der Wrapper am Ende &l hält, wobei l ein lokaler String ist:

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
}

Jede einzelne Zeile wirkt harmlos. Die Unsoundness existiert nur in der Komposition: ein covariantes Feld, eine Zuweisung, die eine Lifetime-Schranke lockert, und ein Drop, das die Nutzlast an einen Ort verschiebt, an dem sie ihren Referenzpunkt überlebt. Das ist die typische Signatur von Implementierungsfehlern in Checkern: Die Invariante ist global, die Durchsetzung aber lokal, und ein Codepfad hat die Prüfung vergessen.

Das Sicherheitsmodell ist also nicht gescheitert. Die Durchsetzung des Sicherheitsmodells ist gescheitert. Das ist ein kleineres Versagen, aber, wie wir gleich sehen werden, kein triviales.

Mythos 2: Elf Jahre unentdeckt heißt, der Bug ist harmlos

Die eigene Triage-Argumentation des Rust-Teams lief ungefähr so: Das wäre P-critical, wenn Leute darauf stoßen würden, aber elf Jahre ohne Sichtung heißen, dass er nicht leicht auszulösen ist, also ist es P-high. Da steckt etwas Wahres drin. Um tatsächlich Speicherunsicherheit zu verursachen, braucht man eine bewusst fiese Drop-Implementierung, die Daten an eine 'static-Stelle verschiebt. Das schreibt praktisch niemand. Die Angriffsfläche für versehentliche Exposition ist winzig.

Aber „selten durch Zufall ausgelöst“ leistet in diesem Satz einiges an Arbeit. Sicherheitsgarantien betreffen nicht nur Zufälle, sondern das, worauf du dich verlassen kannst, wenn der Code um dich herum nicht freundlich ist. Der ganze Sinn eines soliden Typsystems ist modulares Schlussfolgern: Ich muss deine Drop-Implementierung nicht prüfen, weil der Compiler bereits bewiesen hat, dass bestimmte schlechte Kombinationen nicht ausdrückbar sind. Sobald es ein Loch gibt, ist diese Modularität weg. Eine bösartige Abhängigkeit, oder eine subtil falsche aus der Feder eines wohlmeinenden Autors, kann nun etwas tun, von dem die Sprache versprochen hat, dass es unmöglich ist.

Die Geschichte ist voll von „nicht ausnutzbaren“ Bugs, die sehr ausnutzbar wurden, sobald das passende Gadget auftauchte. Die praktische Frage, wie ein Kommentator es formulierte, ist, ob das Beheben irgendeine echte Crate im Ökosystem brechen wird. Die Antwort lautet wahrscheinlich „sehr wenige oder keine“, was gute Nachricht ist. Die richtige Lehre aus elf stillen Jahren ist aber nicht „der Bug war harmlos“. Sondern: Fehlende Belege sind kein Beleg für Abwesenheit, besonders bei Fehlermodi, die Absicht statt Zufall erfordern.

Mythos 3: Viele Augenpaare machen alle Bugs flach

Das ist der Mythos, der uns am meisten beschämen sollte. rustc gehört zu den meistbeobachteten Compilern, die je geschrieben wurden. Er ist Open Source, hat ein eigenes Types-Team, eine aktive akademische Community (RustBelt lieferte vor Jahren ein formales Modell eines Kerns von Rust) und Millionen Nutzer, die ihn täglich belasten. Und doch saß eine Soundness-Lücke in der Lifetime-Inferenz über ein Jahrzehnt, durch komplette Neuschreibungen der umgebenden Maschinerie hindurch.

Linus' Gesetz setzt voraus, dass Augenpaare am richtigen Ort mit dem richtigen Modell im Kopf schauen. Typsystem-Unsoundnesses unterlaufen beide Annahmen. Sie leben an der Schnittstelle mehrerer Features, etwa Varianz, Drop-Reihenfolge, Coercion und Trait-Schranken, und jedes Feature ist für sich lokal korrekt. Reviewer lesen den Code und sehen die beabsichtigte Invariante, weil der Code von Leuten geschrieben wurde, die ebenfalls die beabsichtigte Invariante sahen. Bestätigungsfehler sind im Prozess eingebaut. Das Gegenbeispiel erfordert, wie ein Angreifer zu denken, und adversariales Denken über die eigenen Abstraktionen ist wirklich schwer.

Es gibt eine ganze Website, counterexamples.org, die Wege katalogisiert, wie plausibel aussehende Typregeln brechen. Der gemeinsame Nenner ist Veränderlichkeit, kombiniert mit etwas anderem Tückischem, genau die Form dieses Bugs. Das sind keine neuen Lektionen. Das Typsystem von ML hatte eine berühmte Unsoundness rund um veränderliche Referenzen und Polymorphie, die mit der Value Restriction behoben wurde. Javas Arrays sind kovariant und können zur Laufzeit eine ArrayStoreException werfen, weil die Sprachdesigner Bequemlichkeit über Soundness stellten. Je mehr sich ändert, desto mehr beißen dieselben drei Features, Subtyping, Mutation und Generics, in Kombination jemanden. Wenn du diese Art Archäologie magst, zeigt Lisps sechzigjährige Geschichte, wie lange sich diese Ideen schon entwickeln, und Rob Pikes alte Regeln zur Einfachheit lesen sich anders, wenn man erkennt, dass Komplexität der Nährboden für Soundness-Lücken ist.

Augenpaare helfen. Sie reichen aber nicht. Die ehrliche Position, eine, die ich von jemandem hörte, der an einer eigenen Sprache baut, lautet eher: Kein Review löst jedes Problem, also braucht man mechanische Methoden, die nicht müde werden und eure Annahmen nicht teilen.

Mythos 4: Informelles Schlussfolgern ist praktisch ein Beweis

Als die Lifetime-Regeln von Rust entworfen wurden, wurden sie sorgfältig von klugen Leuten mit vielen Beispielen durchdiskutiert. Das ist informelles Schlussfolgern, und so werden im Grunde alle produktiven Compiler gebaut. Das Ergebnis ist ein System, das soweit irgendjemand weiß sound ist. Was, wie wir nun zweimal gelernt haben, nicht dasselbe ist wie sound.

Die Lücke zwischen beidem ist der Ort, an dem Projekte wie RustBelt und die laufende Arbeit an einem Trait-Solver der nächsten Generation ins Spiel kommen. RustBelt, in Coq (heute Rocq) auf dem Iris-Separation-Logic-Framework gebaut, hat maschinell ein Modell der zentralen Typregeln von Rust geprüft, inklusive der heiklen Teile wie unsafe-Abstraktionsgrenzen. Das war ein Meilenstein. Aber beachte, was er bewiesen hat: ein Modell von Rust, nicht rustc. Der Beweis deckt den λRust-Kalkül ab, und der Produktionscompiler ist abgedriftet, hat Features gewonnen und Implementierungsentscheidungen angesammelt, die niemand erneut verifiziert hat. Dieses Issue ist die Rechnung für diese Drift, die nun fällig wird.

Einen ganzen Produktionscompiler zu formalisieren ist brutal teuer. CompCert, der formal verifizierte C-Compiler, brauchte jahrelangen Expertenaufwand für eine Sprache, die viel kleiner ist als Rust, und er verifiziert Kompilierungspässe, statt zu beweisen, dass das Quell-Typsystem jedes schlechte Programm abfängt. Niemand wird einen Coq-Beweis für die zwei Millionen Zeilen von rustc schreiben. Der realistische Weg sieht eher nach Defense in Depth aus:

• Maschinell geprüfte Modelle der Kernregeln (im Stil von RustBelt), damit die Theorie selbst keine Löcher hat.
• Systematisches Fuzzing und Werkzeuge zur Fallanalyse, die adversariale Programme erzeugen, also die Ecken der Feature-Interaktionen, auf die Menschen beim Testen nicht kommen.
• Mutations- und Property-Based-Testing des Checkers: Wenn das Umlegen einer Schranke ein Programm scheitern lassen sollte, prüfe, dass es das tut. Die Testkultur von SQLite ist hier das Vorbild.
• Eine gepflegte Liste bekannter Unsoundness-Probleme (Rust hat über hundert markiert), behandelt als Backlog mit technischer Priorität statt als Folklore.

Interessanterweise könnte LLM-basierte Suche sich als Nettogewinn erweisen: Ein Werkzeug, das unermüdlich Features auf perverse Weise kombiniert, ist genau der Gegner, den informelles Schlussfolgern fehlt. Das Endziel, das viele von uns hoffen, ist ein formal spezifiziertes Rust mit einem gegen die Spezifikation bewiesenen Checker. Bis dahin ist die Arbeit aber mühsam, unglamourös und besteht aus Constraint-Solving.

Mythos 5: Wenn Soundness nicht absolut ist, ist statische Sicherheit ein Schwindel

Die zynische Lesart geht so: Rust hat Sicherheit versprochen, das Versprechen hatte ein Schlupfloch, also war das Versprechen Marketing, und wir können genauso gut zurück zu YOLO-Pointern in C. Das ist genau verkehrt herum, und es lohnt sich, präzise zu erklären, warum.

Soundness in einem Typsystem ist ein Theorem über ein mathematisches Objekt. Was eine produktive Sprache dir gibt, ist eine statistische und ökonomische Garantie: Ganze Bug-Klassen wie Use-after-free, Data Races und Iterator-Invalidierung wandern von „konstanter Hintergrundstrahlung deiner Codebasis“ zu „Ereignissen, selten genug, um auf der Startseite zu landen, wenn sie nach elf Jahren gefunden werden“. Vergleiche die Basisraten. Speichersicherheitsbugs in großen C- und C++-Codebasen machen Jahr für Jahr den Großteil der schweren CVEs aus, und niemand wundert sich mehr über einen einzelnen. Rusts Unsoundness-Bugs sind so selten, dass jeder sein eigenes GitHub-Issue, seinen eigenen Diskussionsthread und seine eigene Postmortem-Kultur bekommt. Seltenheit, die du aufzählen kannst, ist eine andere Welt als Seltenheit, die du nicht aufzählen kannst.

Es gibt außerdem einen Unterschied darin, wie sich Fehler aufschaukeln. In C ist jede Zeile eine potenzielle Speichersicherheitsgefahr, daher skaliert der Aufwand für Wachsamkeit für immer mit der Codegröße. In Rust konzentriert sich die Wachsamkeit an den Rändern: unsafe-Blöcke, FFI und (wie wir jetzt wissen) der eigene Checker des Compilers. Diese Konzentration macht Auditing, Werkzeuge wie Miri und formale Methoden überhaupt erst handhabbar. Die Garantie ist nicht binär; sie verlagert radikal, wo dein Risiko liegt.

Ein Typsystem mit einem bekannten Bug, den elf Jahre Produktionsverkehr nie getroffen haben, ist immer noch unendlich stärker als eine Sprache, in der der Bug das Design ist.

Was du wirklich mitnehmen solltest

Wenn du Rust schreibst, musst du nichts ändern. Dein Code war vor diesem Issue nicht stillschweigend unsicher; der praktische Exploit-Pfad erforderte Absicht. Wenn du Bibliotheken pflegst, ist der ehrliche Schritt der gleiche wie immer: Halte die unsafe-Oberfläche klein, lass Miri über die kniffligen Stellen laufen und behandle den Borrow Checker nicht als Orakel für fremden bösartigen Code, sondern als außergewöhnlich verlässliches Werkzeug, um deine eigenen Fehler zu finden.

Wenn du Sprachen oder Compiler baust, ist dieser Bug ein Geschenk: ein seltenes, gut dokumentiertes Exemplar dafür, wie Soundness in der Produktion tatsächlich versagt. Nicht in der Theorie, sondern in der Durchsetzung; nicht in einem einzelnen Feature, sondern an einer Feature-Schnittstelle; nicht durch Review entdeckt, sondern durch adversariale Konstruktion. Die Teams, die das ernst nehmen und Trait-Solver-Neuschreibungen, Überarbeitungen der Region-Constraints und verifikationsnahe Werkzeuge finanzieren, sind diejenigen, deren Garantien in zehn Jahren etwas bedeuten werden.

Und für alle: Kalibriere neu, was eine Garantie ist. Wir haben jahrzehntelang „bewiesen“ mit „überzeugend argumentiert und bisher nie widerlegt“ verwechselt, bei Typsystemen, kryptografischen Protokollen und verteiltem Konsens. Die erwachsene Form des Vertrauens besteht nicht darin anzunehmen, dass die Brücke perfekt ist. Sondern darin zu wissen, dass die Brücke Prüfer hat, die ihre Befunde veröffentlichen, gefundene Risse beheben und eine öffentliche Liste der Risse führen, die sie noch nicht geflickt haben. Gemessen daran ist ein elf Jahre währendes Finden einer Lücke keine Anklage. Es ist ein Beleg dafür, dass das System, das menschliche System rund um den Compiler, ungefähr so funktioniert, wie es soll.