iddqd, ou la forme la plus difficile d’unsafe Rust

• iddqd est une bibliothèque de map Rust qui emprunte les clés à partir des valeurs, utilisée chez Oxide pour maintenir en mémoire des index de gros enregistrements comme l’inventaire des disques et des sleds dans le plan de contrôle Omicron, où l’exactitude est cruciale
• Le BTreeMap standard stocke séparément la clé et la valeur, ce qui complique la transmission ou peut laisser des clés dupliquées diverger, tandis que IdOrdMap effectue les recherches en extrayant la clé d’un champ du record
• unsafe Rust est une échappatoire permettant d’exprimer des programmes sûrs que le compilateur ne peut pas prouver, et le code générique doit résister même à du Rust sûr pathologique lorsqu’il appelle des implémentations de traits fournies par l’utilisateur
• L’itération mutable de iddqd étend les durées de vie en s’appuyant sur l’invariant selon lequel tous les index sont distincts, mais une implémentation pathologique de Ord pouvait désaligner le B-tree et l’ensemble d’éléments, créant ainsi des index dupliqués vers le même élément
• Le correctif consiste à comparer ensemble la clé et l’index, puis à revenir à un parcours linéaire qui n’appelle pas de code utilisateur si la recherche échoue ; il faut combiner Miri, des tests basés sur un modèle, l’injection de fautes par panic et une revue adversariale par LLM pour obtenir une confiance suffisante

---

Le problème que résout iddqd

• iddqd est une bibliothèque Rust qui fournit des maps dont les clés sont empruntées aux valeurs, et Oxide l’utilise largement dans le plan de contrôle Omicron
• Omicron est le logiciel au cœur du rack Oxide qui provisionne des ressources comme le compute et le storage et maintient le rack en fonctionnement ; si iddqd se comporte mal, le plan de contrôle peut se dérégler de façon imprévisible et difficile à diagnostiquer
• Une structure comme BTreeMap<Email, User> dans la bibliothèque standard Rust stocke l’email, qui est la clé, séparément de la valeur
• Pour transmettre clé et valeur ensemble, il faut récupérer (email, user) avec get_key_value, et si l’on crée au moment du fetch une structure séparée comme UserRecord, cela devient difficile à gérer quand les types d’enregistrements sont nombreux
• Si l’on duplique aussi l’email dans User, on introduit le risque que l’email dans la clé de la map et celui dans la valeur divergent
• IdOrdMap fait extraire la clé depuis le record via le trait IdOrdItem, et le type de clé peut être emprunté à la valeur, comme type Key<'a> = &'a Email
• Chez Oxide, ce modèle convenait bien à de gros enregistrements tels que les résultats de requêtes en base de données, et il s’est révélé utile pour indexer de gros records dans tout le plan de contrôle

Fonctionnalités supplémentaires

• iddqd prend en charge comme concept de première classe des clés complexes empruntées à plusieurs champs, sans recourir à des contournements comme le dynamic dispatch
• BiHashMap et TriHashMap indexent respectivement un élément par deux ou trois clés, ce qui évite le schéma courant consistant à maintenir plusieurs maps à la main
• L’implémentation Serde sérialise en séquence plutôt qu’en map, ce qui permet de sérialiser en JSON des clés non textuelles et rejette les clés dupliquées
• Une sérialisation sous forme de map est aussi prise en charge pour la rétrocompatibilité

Là où unsafe Rust devient difficile

• Dans Rust, le risque fondamental est le comportement indéfini (undefined behavior, UB) ; si du code sûr ne peut en aucun cas provoquer d’UB, il est sound, sinon il est unsound
• En Rust sûr, le compilateur rejette les programmes contenant de l’UB, mais à cause des limites de l’analyse statique, il rejette aussi certains programmes pourtant exempts d’UB
• Le mot-clé unsafe est une échappatoire pour exprimer ce type de programmes : l’auteur prend la responsabilité de la soundness et demande au compilateur de lui faire confiance
• Parmi les règles Rust que le code unsafe doit respecter figurent l’interdiction des data races, des lectures de mémoire non initialisée ou libérée, de plusieurs alias &mut vers la même zone mémoire, et de la mutation de données immuables
• Ces règles sont difficiles à raisonner, en particulier à cause de l’aliasing mutable, ce qui impose généralement d’encapsuler unsafe derrière une abstraction sûre

Les étapes de validation d’une abstraction sûre

• split_at_mut est une méthode sûre qui découpe un slice mutable en deux, mais un tel découpage ne peut pas être exprimé en Rust sûr uniquement et nécessite donc unsafe
• La soundness de split_at_mut dépend d’invariants dans le code sûr environnant : avoir bien reçu un &mut [T], avoir vérifié mid <= slice.len(), et avoir calculé correctement les longueurs restantes
• Le get de MyVec<T> dépend du fait que len soit exact et que l’accès reste dans les bornes ; cette condition doit être maintenue par toutes les autres méthodes du même module
• La catégorie la plus difficile est celle du code unsafe générique qui appelle du code fourni par l’utilisateur
• Du code Rust sûr, même écrit de manière pathologique ou hostile, ne doit jamais pouvoir amener le code unsafe à provoquer de l’UB
• Un code comme collect_exact, qui fait confiance au len() de ExactSizeIterator pour écrire exactement jusqu’à la capacité allouée, est généralement unsound si l’itérateur renvoie une fausse longueur, car il peut alors écrire dans de la mémoire non allouée
• std::io::Read est lui aussi un trait dont une implémentation boguée peut renvoyer un nombre d’octets lus incorrect, problème abordé dans la Rust RFC 2930
• iddqd appartient à cette catégorie la plus difficile, car c’est une structure de données générique qui appelle des implémentations de traits fournies par l’utilisateur

Structure interne d’iddqd

• iddqd combine une liste d’éléments ItemSet et une table contenant des index de slots
• IdHashMap<T> utilise un ItemSet<T> et une hashbrown::HashTable contenant des ItemIndex
• ItemSet<T> contient un Vec<ItemSlot<T>>, où ItemSlot<T> vaut soit Occupied(T), soit Vacant { next: ItemIndex }
• free_head pointe vers le slot Vacant libéré le plus récemment, ou vers un sentinel indiquant qu’il n’y a aucun slot libre ; free_head et les slots Vacant forment une free chain
• Lors de l’insertion d’un nouvel élément, on vérifie via free_head s’il existe un slot réutilisable ; si oui, on remplace le slot Vacant par Occupied, puis on avance free_head vers la valeur suivante
• S’il n’y a pas de slot libre, on ajoute à la fin un nouveau slot Occupied, puis on récupère la clé, on calcule le hash et on inscrit le nouvel index dans la hash table
• La suppression fait l’inverse : on trouve et retire d’abord l’index dans la hash table via la clé, puis on transforme le ItemSlot correspondant en Vacant et on relie l’ancien free_head à next
• IdOrdMap utilise un index B-tree au lieu d’une hash table, tandis que BiHashMap et TriHashMap stockent respectivement deux et trois hash tables

Itération mutable et extension de durée de vie

• IdOrdMap::iter_mut itère de façon mutable sur les éléments dans l’ordre des clés
• Un itérateur Rust ne doit pas emprunter ses valeurs de retour à l’itérateur lui-même, car des combinateurs comme collect peuvent conserver des valeurs comme Vec<&mut T> après la disparition de l’itérateur
• Pour que cela reste sûr, l’itérateur ne doit jamais renvoyer deux fois la même valeur
• Le borrow checker ne voit que les accès successifs à la liste et ne peut pas savoir que tous les index sont distincts
• iddqd utilise une extension de durée de vie via std::mem::transmute::<&mut T, &'a mut T>, ce qui dépend de l’invariant selon lequel tous les index renvoyés par self.iter sont distincts

Le bug causé par une implémentation pathologique de Ord

• Dans un IdOrdMap contenant cinq éléments avec les clés 0 à 4 dans l’ordre, une recherche de la clé 0 via l’Entry API produit un OccupiedEntry qui stocke en interne l’index 0
• Si l’implémentation de Ord de Key est ensuite modifiée pour toujours renvoyer Equal indépendamment des valeurs, OccupiedEntry::remove peut retirer le mauvais élément lorsqu’il redescend dans le B-tree en ne se basant que sur la comparaison des clés
• Par exemple, si le B-tree compare d’abord (key = 2, index = 2), l’entrée correspondante est supprimée à cause de Equal, tandis que l’item set supprime l’élément 0 parce que c’est l’index conservé par OccupiedEntry
• Dans cet état, l’index 0 reste dans le B-tree, mais le slot 0 de l’item set devient vacant, tandis que l’élément 2 reste dans l’item set sans pointeur B-tree
• Si ensuite Ord redevient normal et qu’un élément de clé 1000 est inséré, le slot 0 pointé par free_head est réutilisé
• Le résultat est qu’il existe alors dans le B-tree des index dupliqués pointant vers le même slot, ce qui permet à IterMut de créer plusieurs références &mut vers la même mémoire et rend l’ensemble unsound

La correction et le compromis de performance

• Le parcours du B-tree a été modifié pour vérifier non seulement l’égalité de la clé, mais aussi celle de l’index
• Lorsqu’on cherche une clé avec un index connu, on compare à la fois (key, index) ; ainsi, même si un Ord pathologique renvoie Equal, la comparaison entre (key = 2, index = 2) et l’index recherché 0 devient Less grâce au départage par l’index
• Pour que cette recherche réussisse, l’index stocké doit effectivement correspondre à l’index recherché
• Ce départage empêche d’associer le mauvais élément, mais ne garantit pas toujours de retrouver le bon
• Le B-tree est trié par clé alors que le départage compare les index ; ces deux ordres sont en général indépendants
• Si la recherche dans l’arbre échoue, le code revient à un parcours linéaire du B-tree pour retirer l’index concerné, sans appeler de code utilisateur
• Ce fallback transforme l’opération de suppression de logarithmique en linéaire, mais comme il n’est atteint qu’en présence de code utilisateur bogué, cela est considéré comme un compromis acceptable

Couches de validation

• Comme iddqd sert de structure de données fondamentale, le projet combine revue analytique et plusieurs formes de validation empirique
• Chaque bloc unsafe et chaque motif unsafe sont analysés par un à trois auteurs et relecteurs Rust
• Au-dessus de chaque bloc unsafe, un commentaire // SAFETY: documente le raisonnement, et le lint undocumented_unsafe_blocks de Clippy vérifie la présence de ce commentaire
• Les tests basés sur des exemples créent des maps, exécutent des opérations puis vérifient les résultats ; iddqd dispose à la fois de tests unitaires internes et de tests d’intégration sur l’API publique
• Ces tests existent aussi sous forme de doctests, servant en même temps de documentation
• Des tests pathologiques injectent des implémentations boguées de Ord et d’autres traits
• En CI, les tests réguliers et pathologiques sont exécutés sous Miri pour détecter plusieurs formes d’UB
• Des invariants comme l’absence d’index dupliqués peuvent aussi être vérifiés dans un environnement de test normal, hors Miri

Tests basés sur un modèle et fault injection

• iddqd utilise deux niveaux de tests aléatoires : des tests basés sur un modèle comparés à un oracle correct, puis de la fault injection par-dessus
• Les tests basés sur un modèle, ou stateful property-based testing, appliquent une séquence aléatoire d’opérations à une instance du type et comparent les résultats à un oracle connu comme correct
• iddqd exécute de vastes tests basés sur un modèle en s’appuyant sur l’oracle NaiveMap, inefficace mais manifestement correct
• La fault injection consiste à introduire aléatoirement des bugs dans le code utilisateur ; dans iddqd, l’axe particulièrement utile a été la panic safety
• Même si du code utilisateur panic au milieu d’une opération, les invariants de la map ne doivent pas être brisés
• Chaque opération de map reçoit un compte à rebours de panic aléatoire ; celui-ci est décrémenté à chaque appel de code utilisateur, et lorsqu’il atteint 0, un panic est déclenché, ce qui permet des tests aléatoires de panic safety
• Cette méthode a révélé plusieurs bugs subtils dans iddqd, dont certains menaient à des problèmes de soundness
• Les tests basés sur un modèle vérifient aussi après chaque opération des invariants internes comme l’absence de duplicate index
• Ces tests sont trop lents pour être exécutés sous Miri, donc les invariants dont dépendent la soundness et la correction sont vérifiés séparément

Revue adversariale par LLM et méthodes formelles

• Un frontier model de génération actuelle a trouvé plusieurs implémentations pathologiques de code utilisateur capables de corrompre la map
• Dans un cas notable, le LLM a construit un chemin où un allocateur personnalisé panic pendant l’unwind, cassant les invariants de la map
• Il s’agissait d’un problème de panic safety différent des panics de code utilisateur plus ordinaires, comme ceux déjà couverts dans les implémentations de Ord
• Les LLM peuvent aussi produire des affirmations de soundness plausibles mais fausses ; la défense consiste alors à utiliser une TDD red-green avec Miri comme oracle
• Pour un bug de soundness, on commence par écrire un test qui montre l’UB sous Miri, puis on vérifie qu’après le correctif ce même test passe
• Une approche consistant à prouver les invariants de la map avec un model checker comme Kani bute sur la complexité de iddqd, dont les preuves nécessaires deviennent trop volumineuses pour l’outil
• Creusot peut aider à prouver qu’un code Rust est exempt de panic et d’autres erreurs, mais ne peut pas à ce stade prouver les invariants qui doivent tenir même si le code utilisateur panic ou se comporte mal
• NaiveMap joue le rôle de spécification la plus proche d’iddqd, et la CI exécute les tests basés sur un modèle des milliers de fois pour obtenir une forte confiance dans l’adéquation de l’implémentation à cette spécification
• cargo-anneal est un outil en développement jugé intéressant, car il permettrait d’insérer des preuves de soundness en Lean dans des commentaires de documentation à côté du code unsafe Rust
• iddqd présente des invariants clairs et un périmètre limité mais non trivial, ce qui en fait un bon candidat de benchmark pour les outils de vérification formelle

Conclusion

• L’unsafe Rust générique est extrêmement difficile, car chaque invariant doit être maintenu en tenant compte d’implémentations de traits arbitraires, voire hostiles
• Le bug d’iddqd montre qu’une implémentation pathologique de Ord peut tromper la map au point de créer des alias mutables vers la même mémoire
• Aucune technique seule ne permet d’attraper tous les bugs ; il faut donc combiner un raisonnement humain ligne par ligne sur l’unsafe, des tests basés sur des exemples, des tests pathologiques, des tests aléatoires et une revue adversariale par frontier model
• Oxide considère qu’un tel niveau de rigueur est justifié pour une infrastructure fondamentale

[GN⁺]

Réactions sur Lobste.rs

• Si j’ai bien compris (je regardais ça sur mon téléphone en déplacement), on dirait que ça pourrait se résoudre avec un type wrapper et HashSet/BTreeSet à la place de HashMap/BTreeMap
  Le type wrapper n’est pas strictement nécessaire, mais c’est un bon choix pour la sûreté et la maintenance future
  Il suffit d’un wrapper de taille nulle autour de l’objet, avec des implémentations personnalisées de PartialEq/Hash qui ne regardent que les champs pertinents. Pour faire des recherches sans construire la valeur complète, on peut créer un second type qui implémente AsRef pour le type de valeur
  Cette approche permet de réutiliser telle quelle l’interface existante de HashSet/BTreeSet sans unsafe. Au lieu d’envelopper le type valeur/clé, on pourrait aussi créer un nouveau wrapper de HashSet/BTreeSet qui fournit directement ce comportement

  • Ici, les clés sont des combinaisons arbitraires de champs et de sous-champs d’un type d’enregistrement, exprimées avec des GAT. Et le motif d’index entier / slab se généralise aussi naturellement en map multi-index
    Il y a aussi l’API Entry, l’accès mutable / l’itération, etc. Dans iddqd, la mutabilité est gérée avec beaucoup de prudence, et à certains endroits des valeurs atomiques sont utilisées pour autoriser une mutabilité intérieure. Ce genre de traitement aurait été assez difficile sans indirection d’index

• Pour vérifier formellement iddqd, j’aurais d’abord tendance à essayer un model checker comme Kani pour prouver que la map ne casse pas ses invariants internes. Mais je suis intrigué par le passage disant que iddqd est un peu trop complexe pour Kani et que les preuves nécessaires deviennent trop grosses pour que l’outil les gère
  Pourrais-tu en dire plus là-dessus ? Je me demande si cela signifie que la complexité algorithmique dégénère dans le pire des cas
  Globalement, c’est un cas d’étude intéressant en méthodes formelles, et j’ai apprécié que cet aspect soit abordé. En voyant des réussites sur de gros projets avec les outils de vérification formelle existants, on pourrait naïvement penser qu’on peut au moins prouver la correction d’une structure de données ; en pratique, on voit que la difficulté varie d’une structure à l’autre, et que même dans des langages jugés plus favorables à la preuve que Rust, qui autorise l’aliasing sans restriction, ce n’est pas simple en contexte réel
  Un peu hors sujet, mais je me demande aussi comment les diagrammes ont été faits. Est-ce qu’un script jetable a été écrit, ou bien s’agit-il de créations spécifiques adaptées au design du blog/site d’Oxide, plutôt que d’un outil générique ?

  • En bas de l’article, il est écrit « Diagrams courtesy Ben Leonard. », et Ben Leonard est designer chez Oxide. Donc il est probable qu’il s’agisse de diagrammes faits à la main
  • Même en essayant de prouver quelque chose de très basique sur une implémentation de trait concrète et fonctionnelle, CBMC tournait sur le CPU pendant plus de 10 minutes sans finir
    J’ai aussi essayé de réduire le périmètre. Par exemple, j’ai supposé que hashbrown était correct, mais ça n’a pas apporté de grand progrès. À ce stade, j’ai quasiment abandonné. Je suis assez confiant que iddqd est correct pour des implémentations de trait qui se comportent bien, et ce qui m’intéressait vraiment du point de vue des méthodes formelles, c’était une preuve qui tienne aussi pour des implémentations arbitraires et incorrectes
    Cela dit, je ne suis pas la personne la plus compétente pour utiliser Kani. Ce serait vraiment bien si toi ou quelqu’un d’autre essayait
    Les diagrammes ont d’abord été esquissés avec Mermaid, puis l’excellent designer Ben Leonard les a retravaillés à la main pour les adapter à notre palette de couleurs et notre thème

• Le motif de map basée sur des champs, où l’on indexe un objet à partir d’un de ses champs comme clé, est quelque chose que j’aimerais toujours pouvoir utiliser en C# aussi
  J’avais essayé d’en faire une version simple moi-même il y a quelque temps, mais l’interface n’était pas très propre, donc j’ai laissé tomber. Cet article me donne envie de réessayer

  • Oui, c’est un motif vraiment utile. Je l’ai créé pour un besoin au travail, mais depuis je l’ai utilisé un peu partout, de bases de code de production comme cargo-nextest jusqu’à des projets personnels
    Utiliser un seul champ comme clé est le cas d’usage le plus courant, mais iddqd est suffisamment flexible pour utiliser n’importe quelle combinaison de champs, de sous-champs, ou de fonctions calculables de manière pure et peu coûteuse à partir de champs. Par exemple, on peut chercher ArtifactKey sur https://docs.rs/iddqd/latest/iddqd/ (désolé si vous n’êtes pas familier avec la syntaxe Rust)
    Lors de la conception de iddqd, j’étais convaincu que les utilisateurs devaient pouvoir exploiter toute la puissance du système de types de Rust, quel que soit le nombre de contournements nécessaires de mon côté comme auteur de la bibliothèque. Je voulais vraiment que iddqd soit une bibliothèque agréable à utiliser pour ses utilisateurs, et en particulier pour mes collègues