iddqd oder die schwierigste Art von unsafe Rust

• iddqd ist eine Rust-Map-Bibliothek, die Schlüssel aus Werten ausleiht, und wird in Oxides Omicron-Control-Plane verwendet, um In-Memory-Indizes für große Datensätze wie Disk- und Sled-Inventare zu pflegen, bei denen Korrektheit entscheidend ist
• Die Standard-BTreeMap speichert Schlüssel und Werte getrennt, was die Übergabe umständlich macht oder zu auseinanderlaufenden doppelten Schlüsseln führen kann; IdOrdMap extrahiert den Schlüssel dagegen aus einem Feld innerhalb des Datensatzes und verwendet ihn für Lookups
• unsafe Rust ist ein Ausweg, um sichere Programme auszudrücken, die der Compiler nicht beweisen kann, und generischer Code, der benutzerdefinierte Trait-Implementierungen aufruft, muss sogar pathologisches sicheres Rust aushalten
• Die mutable Iteration von iddqd erweitert Lifetimes auf Basis der Invariante, dass alle Indizes verschieden sind; eine pathologische Ord-Implementierung konnte jedoch B-Tree und Item-Set auseinanderlaufen lassen und doppelte Indizes auf dasselbe Element erzeugen
• Die Korrektur vergleicht Schlüssel und Index gemeinsam und fällt bei Fehlschlag auf einen linearen Scan zurück, der keinen Benutzercode aufruft; für hinreichendes Vertrauen braucht es Miri, modellbasiertes Testen, Panic-Fault-Injection und adversariales Review durch LLMs

---

Das Problem, das iddqd löst

• iddqd ist eine Rust-Bibliothek, die Maps bereitstellt, deren Schlüssel aus dem Wert ausgeliehen werden, und Oxide verwendet sie breit in der Omicron-Control-Plane
• Omicron ist die Software im Zentrum eines Oxide-Racks, die Ressourcen wie Compute und Storage provisioniert und den laufenden Betrieb des Racks sicherstellt; wenn iddqd fehlfunktioniert, kann die Control-Plane auf unvorhersehbare und schwer zu diagnostizierende Weise falsch arbeiten
• Eine Struktur wie BTreeMap<Email, User> aus der Rust-Standardbibliothek speichert den Schlüssel, hier die E-Mail, getrennt vom Wert
• Um Schlüssel und Wert gemeinsam weiterzugeben, muss man mit get_key_value (email, user) holen; erstellt man stattdessen beim Fetch einen separaten Record-Typ wie UserRecord, wird das bei vielen Record-Typen unhandlich
• Dupliziert man die E-Mail auch innerhalb von User, entsteht das Risiko, dass der Schlüssel der Map und die E-Mail im Wert voneinander abweichen
• IdOrdMap verwendet das Trait IdOrdItem, um den Schlüssel aus dem Record zu extrahieren; der Schlüsseltyp kann dabei aus dem Wert ausgeliehen werden, etwa type Key<'a> = &'a Email
• Bei Oxide passte dieses Muster gut zu großen Records wie Datenbankabfrage-Ergebnissen und erwies sich als nützlich für die Indizierung großer Records in der gesamten Control-Plane

Zusätzliche Funktionen

• iddqd unterstützt komplexe Schlüssel, die aus mehreren Feldern ausgeliehen werden, als First-Class-Konzept und kann sie ohne Umwege wie Dynamic Dispatch verarbeiten
• BiHashMap und TriHashMap indizieren einen Eintrag jeweils über zwei oder drei Schlüssel und vermeiden so das übliche Muster, mehrere Maps von Hand synchron zu halten
• Die Serde-Implementierung serialisiert als Sequenz statt als Map, sodass in JSON auch Nicht-String-Schlüssel serialisiert werden können, und lehnt doppelte Schlüssel ab
• Aus Gründen der Abwärtskompatibilität wird auch die Serialisierung im Map-Format unterstützt

Wo unsafe Rust schwierig wird

• Das zentrale Risiko in Rust ist undefiniertes Verhalten (undefined behavior, UB); wenn sicherer Code auf keine Weise UB auslösen kann, ist er sound, andernfalls unsound
• In sicherem Rust lehnt der Compiler Programme mit UB ab, aber wegen der Grenzen statischer Analyse werden auch manche Programme ohne UB abgelehnt
• Das Schlüsselwort unsafe ist der Ausweg, um solche Programme auszudrücken; der Autor übernimmt die Verantwortung für die Soundness und bittet den Compiler um Vertrauen
• Zu den Rust-Regeln, die unsafe Code einhalten muss, gehören: keine Data Races, kein Lesen von nicht initialisiertem oder freigegebenem Speicher, kein mehrfaches &mut-Aliasing desselben Speicherbereichs und keine Mutation unveränderlicher Daten
• Diese Regeln sind schwer zu durchdenken, besonders wegen mutable Aliasing, weshalb unsafe meist hinter sicheren Abstraktionen gekapselt werden muss

Stufen der Verifikation sicherer Abstraktionen

• split_at_mut ist eine sichere Methode, die einen mutablen Slice in zwei Teile aufspaltet, benötigt intern aber unsafe, weil sich eine solche Aufteilung nicht allein in sicherem Rust ausdrücken lässt
• Die Soundness von split_at_mut hängt von Invarianten im umgebenden sicheren Code ab, etwa ob wirklich &mut [T] übergeben wurde, ob mid <= slice.len() geprüft wurde und ob die verbleibenden Längen korrekt berechnet wurden
• get von MyVec<T> hängt davon ab, dass len korrekt ist und der Zugriff im Bereich liegt; diese Bedingungen müssen von allen anderen Methoden im selben Modul aufrechterhalten werden
• Am schwierigsten wird es, wenn generischer unsafe-Code benutzerdefinierten Code aufruft
• Sicherer Rust-Code darf unsafe-Code niemals dazu bringen, UB auszulösen, egal wie pathologisch oder feindselig er geschrieben ist
• Code wie collect_exact, der len() von ExactSizeIterator vertraut und genau so viel Kapazität beschreibt, ist im Allgemeinen unsound, weil ein Iterator mit gelogener Länge in nicht allokierten Speicher schreiben lassen kann
• Auch std::io::Read ist ein Trait, dessen fehlerhafte Implementierungen eine falsche Zahl gelesener Bytes zurückgeben können; Rust RFC 2930 behandelt dieses Problem
• iddqd gehört in diese schwierigste Kategorie, weil es eine generische Datenstruktur ist, die benutzerdefinierte Trait-Implementierungen aufruft

Interne Struktur von iddqd

• iddqd kombiniert eine Liste von Einträgen, das ItemSet, mit einer Tabelle, die Slot-Indizes speichert
• IdHashMap<T> verwendet ein ItemSet<T> und eine hashbrown::HashTable, die ItemIndex speichert
• ItemSet<T> enthält ein Vec<ItemSlot<T>>, wobei ItemSlot<T> entweder Occupied(T) oder Vacant { next: ItemIndex } ist
• free_head zeigt auf den zuletzt freigegebenen Vacant-Slot oder auf ein Sentinel, das anzeigt, dass es keinen freien Slot gibt; free_head und die Vacant-Slots bilden zusammen die Free-Chain
• Beim Einfügen eines neuen Eintrags prüft man über free_head, ob ein wiederverwendbarer Slot existiert; falls ja, wird der Vacant-Slot mit Occupied überschrieben und free_head auf den nächsten Wert verschoben
• Gibt es keinen freien Slot, wird am Ende ein neuer Occupied-Slot angehängt; danach wird der Schlüssel geholt, der Hash berechnet und der neue Index in der Hash-Tabelle eingetragen
• Beim Entfernen wird umgekehrt zuerst der Index über den Schlüssel in der Hash-Tabelle gesucht und entfernt; anschließend wird der entsprechende ItemSlot in Vacant umgewandelt und der bisherige free_head als next verkettet
• IdOrdMap verwendet statt einer Hash-Tabelle einen B-Tree-Index, und BiHashMap sowie TriHashMap speichern jeweils zwei bzw. drei Hash-Tabellen

Mutable Iteration und Lifetime-Erweiterung

• IdOrdMap::iter_mut iteriert mutabel über Einträge in Schlüsselsortierung
• Ein Rust-Iterator muss Werte zurückgeben, die den Iterator selbst nicht ausleihen; Kombinatoren wie collect können Werte wie Vec<&mut T> behalten, selbst nachdem der Iterator verschwunden ist
• Damit dieses Verhalten sicher ist, darf der Iterator denselben Wert nicht zweimal zurückgeben
• Der Borrow Checker sieht bei einer Liste nur aufeinanderfolgende Zugriffe und kann nicht erkennen, dass alle Indizes verschieden sind
• iddqd nutzt deshalb Lifetime-Erweiterung mit std::mem::transmute::<&mut T, &'a mut T>, was auf der Invariante beruht, dass die von self.iter gelieferten Indizes alle verschieden sind

Der Bug durch eine pathologische Ord-Implementierung

• In einer IdOrdMap mit fünf Einträgen und den Schlüsseln 0 bis 4 in Reihenfolge speichert ein Lookup für Schlüssel 0 über die Entry API ein OccupiedEntry intern mit Index 0
• Wenn danach die Ord-Implementierung von Key so verändert wird, dass sie unabhängig vom Wert immer Equal zurückgibt, kann OccupiedEntry::remove beim erneuten Abstieg im B-Tree anhand des Schlüsselvergleichs den falschen Eintrag entfernen
• Wenn im B-Tree zum Beispiel zuerst (key = 2, index = 2) verglichen wird, wird wegen Equal dieser Entry entfernt, während im Item-Set durch den im OccupiedEntry gehaltenen Index 0 Eintrag 0 entfernt wird
• In diesem Zustand bleibt Index 0 im B-Tree erhalten, während Slot 0 im Item-Set vacant wird; Eintrag 2 bleibt im Item-Set, verliert aber seinen Zeiger im B-Tree
• Wenn Ord danach wieder normal funktioniert und ein Eintrag mit Schlüssel 1000 eingefügt wird, wird der von free_head referenzierte Slot 0 wiederverwendet
• Dadurch entstehen im B-Tree doppelte Indizes, die auf denselben Slot zeigen, und IterMut kann mehrere &mut-Referenzen auf denselben Speicher erzeugen, wodurch die Implementierung unsound wird

Korrektur und Performance-Kompromiss

• Beim Abstieg im B-Tree wird nun nicht nur die Gleichheit des Schlüssels, sondern auch die des Index geprüft
• Wenn nach einem Schlüssel mit bekanntem Index gesucht wird, werden sowohl (key, index) verglichen; selbst wenn pathologisches Ord Equal zurückgibt, wird der Vergleich mit (key = 2, index = 2) und dem gesuchten Index 0 durch den Index als Tie-Breaker zu Less
• Damit diese Suche erfolgreich sein kann, muss der gespeicherte Index tatsächlich mit dem gesuchten Index übereinstimmen
• Der Tie-Breaker verhindert falsche Treffer, garantiert aber nicht, dass der richtige Eintrag immer gefunden wird
• Der B-Tree ist nach Schlüssel sortiert, der Tie-Breaker vergleicht aber Indizes; beide Ordnungen sind im Allgemeinen unabhängig voneinander
• Falls die Baumsuche scheitert, fällt der Code auf einen linearen Scan zurück, der den betreffenden Index aus dem B-Tree entfernt, ohne Benutzercode aufzurufen
• Dieses Fallback macht die Entfernung statt logarithmisch linear, wird aber als akzeptabler Kompromiss betrachtet, da es nur bei fehlerhaftem Benutzercode erreicht wird

Verifikationsschichten

• Weil iddqd als grundlegende Datenstruktur verwendet wird, kommen sowohl analytische Prüfung als auch mehrere empirische Verifikationsmethoden zum Einsatz
• Jeder unsafe-Block und jedes unsafe-Muster wird von ein bis drei Rust-Autoren und Reviewern analysiert
• Über jedem unsafe-Block dokumentieren // SAFETY:-Kommentare die Begründung, und Clippys Lint undocumented_unsafe_blocks prüft, dass diese Kommentare vorhanden sind
• Example-based Tests erstellen Maps, führen Operationen aus und prüfen dann die Ergebnisse; iddqd hat interne Unit-Tests und Integrations-Tests für die öffentliche API
• Diese Tests existieren auch als Doctests und dienen damit zugleich als Dokumentation
• Pathologische Tests liefern fehlerhafte Ord- und andere Trait-Implementierungen ein
• In der CI werden sowohl reguläre Tests als auch pathologische Tests unter Miri ausgeführt, um verschiedene Arten von UB zu erkennen
• Bedingungen wie die Invariante, dass es keine doppelten Indizes geben darf, lassen sich auch in normalen Testumgebungen außerhalb von Miri prüfen

Modellbasiertes Testen und Fault Injection

• iddqd verwendet zwei Ebenen von Randomized Testing: modellbasiertes Testen gegen ein korrektes Oracle und darauf aufbauend Fault Injection
• Model-based Testing oder stateful property-based testing wendet zufällige Operationsfolgen auf eine Typinstanz an und vergleicht die Ergebnisse mit einem als korrekt bekannten Oracle
• iddqd führt umfangreiche modellbasierte Tests gegen das ineffiziente, aber klar korrekte NaiveMap-Oracle aus
• Fault Injection bedeutet hier, zufällig Bugs in Benutzercode einzubauen; bei iddqd erwies sich besonders Panic-Safety als ergiebige Achse
• Selbst wenn Benutzercode mitten in einer Operation panikt, dürfen die Invarianten der Map nicht brechen
• Jede Map-Operation bekommt einen zufälligen Panic-Countdown; bei jedem Aufruf von Benutzercode wird er um 1 verringert, und sobald er 0 erreicht, wird eine Panic ausgelöst, um zufällige Panic-Safety-Tests durchzuführen
• Dieser Ansatz fand in iddqd mehrere subtile Bugs, von denen einige zu Unsoundness führten
• Die modellbasierten Tests prüfen nach jeder Operation auch interne Invarianten wie das Fehlen doppelter Indizes
• Modellbasierte Tests sind zu langsam, um sie unter Miri auszuführen; deshalb werden die Invarianten, von denen Soundness und Korrektheit abhängen, gesondert geprüft

Adversariales LLM-Review und formale Methoden

• Frontier-Modelle der aktuellen Generation fanden mehrere pathologische Benutzercode-Implementierungen, die die Map beschädigen konnten
• In einem bemerkenswerten Fall konstruierte ein LLM einen Pfad, bei dem ein Custom Allocator panikt und beim Unwinding die Map-Invarianten verletzt werden
• Das war ein anderes Panic-Safety-Problem als die bereits abgedeckten Panics in gewöhnlichem Benutzercode wie Ord-Implementierungen
• LLMs können auch plausibel klingende, aber falsche Soundness-Behauptungen erzeugen; als Gegenmaßnahme dient red-green TDD mit Miri als Oracle
• Bei einem Soundness-Bug wird zunächst ein Test erstellt, der unter Miri UB zeigt; nach der Korrektur wird geprüft, dass derselbe Test besteht
• Ein Ansatz, Map-Invarianten mit einem Model Checker wie Kani zu beweisen, scheitert bei iddqd daran, dass die Struktur zu komplex ist und die nötigen Beweise zu groß für das Werkzeug werden
• Creusot kann helfen zu beweisen, dass Rust-Code frei von Panics und anderen Fehlern ist, kann aber derzeit keine Invarianten beweisen, die auch dann erhalten bleiben müssen, wenn Benutzercode panikt oder sich fehlerhaft verhält
• NaiveMap dient als der Spezifikation von iddqd am nächsten kommendes Modell, und in der CI werden die modellbasierten Tests tausendfach ausgeführt, um hohes Vertrauen in die Übereinstimmung von Implementierung und Spezifikation zu gewinnen
• cargo-anneal ist ein in Entwicklung befindliches Werkzeug von Interesse, das erlaubt, neben unsafe-Rust in Doc-Comments Soundness-Beweise in Lean einzubetten
• iddqd hat klare Invarianten und einen begrenzten, aber nicht trivialen Umfang und eignet sich daher als Benchmark-Kandidat für Werkzeuge formaler Verifikation

Fazit

• Generisches unsafe Rust ist extrem schwierig, weil jede Invariante auch gegenüber beliebigen und adversarialen Trait-Implementierungen erhalten bleiben muss
• Der Bug in iddqd zeigt, dass eine pathologische Ord-Implementierung die Map so täuschen kann, dass mutable Aliase auf denselben Speicher entstehen
• Keine einzelne Technik kann alle Bugs finden; deshalb werden zeilenweise menschliche unsafe-Analyse, example-based Tests, pathologische Tests, Randomized Tests und adversariales Review mit Frontier-Modellen kombiniert
• Oxide hält dieses Maß an Strenge für grundlegende Infrastruktur für gerechtfertigt

[GN⁺]

Lobste.rs-Kommentare

• Wenn ich das richtig verstanden habe (bin unterwegs und habe es am Handy gelesen), scheint sich das mit einem Wrapper-Typ und der Verwendung von HashSet/BTreeSet statt HashMap/BTreeMap lösen zu lassen
  Der Wrapper-Typ ist nicht zwingend nötig, aber im Hinblick auf Sicherheit und spätere Wartbarkeit eine gute Wahl
  Man braucht nur einen Wrapper der Größe 0, der das Objekt umhüllt, und darin eine benutzerdefinierte Implementierung von PartialEq/Hash, die nur auf die relevanten Felder schaut. Wenn man suchen will, ohne den vollständigen Wert zu konstruieren, kann man einen zweiten Typ mit einer AsRef-Implementierung für den Werttyp erstellen
  Dieser Ansatz ist eine Möglichkeit, die bestehende HashSet/BTreeSet-Schnittstelle ohne unsafe unverändert wiederzuverwenden. Statt den Wert-/Schlüsseltyp zu wrappen, könnte man auch neue HashSet-/BTreeSet-Wrapper bauen, die dieses Verhalten übernehmen

  • Der Schlüssel ist hier eine beliebige Kombination aus Feldern und Unterfeldern eines Record-Typs und wird mit GAT ausgedrückt. Außerdem lässt sich das Integer-Index-/Slab-Muster ganz natürlich zu einer Multi-Index-Map verallgemeinern
    Dinge wie die Entry-API sowie veränderlicher Zugriff/Iteration sind ebenfalls enthalten. In iddqd wird Mutabilität ziemlich vorsichtig behandelt, und an einigen Stellen werden atomare Werte verwendet, um innere Mutabilität zuzulassen. Ohne Index-Indirektion wäre so etwas ziemlich schwierig gewesen

• Um iddqd formal zu verifizieren, würde ich anfangs vermutlich mit einem Model Checker wie Kani beweisen wollen, dass die Map ihre internen Invarianten nicht verletzt. Mich interessiert aber die Stelle, an der gesagt wird, iddqd sei für Kani etwas zu komplex und die benötigten Beweise würden so groß, dass das Tool damit schwer zurechtkommt
  Könntest du diesen Teil etwas genauer erläutern? Ich frage mich, ob das bedeutet, dass die Rechenkomplexität des Algorithmus in den Worst Case entartet
  Insgesamt ist das als Fallstudie zu formalen Methoden interessant, und ich fand es gut, dass dieser Teil behandelt wurde. Wenn man die Erfolgsgeschichten bestehender Werkzeuge zur formalen Verifikation in großen Projekten sieht, könnte man naiv annehmen, dass sich zumindest die Korrektheit von Datenstrukturen beweisen lässt. In der Praxis zeigt sich aber, dass der Schwierigkeitsgrad je nach Datenstruktur variiert und dass es selbst in Sprachen, die für Beweise günstiger gelten als solche wie Rust mit unbeschränktem Aliasing, praktisch nicht einfach ist
  Etwas am Thema vorbei, aber ich würde auch gern wissen, wie die Diagramme erstellt wurden. Habt ihr dafür Einweg-Skripte geschrieben? Es wirkt eher wie etwas Speziell-Angefertigtes passend zum Design des Oxide-Blogs bzw. der Website und nicht wie ein allgemeines Tool

  • Unten im Artikel steht „Diagrams courtesy Ben Leonard.“, und Ben Leonard ist Designer bei Oxide. Daher scheint es gut möglich, dass es sich um von Hand erstellte Diagramme handelt
  • Selbst als ich versuchte, etwas sehr Grundlegendes für eine konkrete und korrekt funktionierende Trait-Implementierung zu beweisen, lief CBMC mit voller CPU-Auslastung mehr als 10 Minuten, ohne fertig zu werden
    Ich habe auch versucht, den Umfang einzugrenzen. Zum Beispiel habe ich angenommen, dass hashbrown korrekt ist, aber auch das brachte keinen großen Fortschritt. An dem Punkt habe ich fast aufgegeben. Ich bin ziemlich überzeugt, dass iddqd bei gut funktionierenden Trait-Implementierungen korrekt ist, und was mich bei formalen Methoden wirklich interessiert hat, war ein Beweis, der auch für beliebige, fehlerhaft funktionierende Implementierungen gilt
    Ich bin allerdings nicht die Person, die Kani am besten beherrscht. Es wäre wirklich toll, wenn du oder jemand anders das einmal versuchen würdet
    Die Diagramme wurden zuerst in Mermaid skizziert, danach hat der großartige Designer Ben Leonard sie von Hand so ausgearbeitet, dass sie zu unserer Farbpalette und unserem Theme passen

• Das Muster einer feldbasierten Map, bei der ein Objekt anhand eines seiner Felder als Schlüssel indiziert wird, ist etwas, das ich auch in C# jederzeit gern verfügbar hätte
  Ich hatte früher einmal versucht, selbst etwas Einfaches zu bauen, habe es aber wieder aufgegeben, weil die Schnittstelle nicht besonders sauber war. Durch diesen Artikel bekomme ich Lust, es noch einmal zu versuchen

  • Ja, das ist wirklich ein nützliches Muster. Ich habe es wegen einer Aufgabe gebaut, die wir im Unternehmen brauchten, aber seitdem benutze ich es überall – von produktiven Codebases wie cargo-nextest bis hin zu persönlichen Projekten
    Die Verwendung nur eines einzelnen Felds als Schlüssel ist zwar der häufigste Anwendungsfall, aber iddqd ist flexibel genug, um jede Kombination aus Feldern, Unterfeldern oder Funktionen zu verwenden, die sich aus einem Feld rein und günstig berechnen lassen. Such zum Beispiel unter https://docs.rs/iddqd/latest/iddqd/ nach ArtifactKey (bitte sieh es mir nach, falls du nicht an Rust-Syntax gewöhnt bist)
    Beim Entwurf von iddqd war ich fest davon überzeugt, dass Nutzer die volle Stärke des Rust-Typsystems einsetzen können sollten – ganz gleich, wie viele Umwege ich als Bibliotheksautor dafür gehen musste. Ich wollte wirklich, dass iddqd für die Nutzer, besonders für meine Kollegen, eine angenehme Bibliothek ist