Bug du borrow checker de Rust : la soundness en question

Le système de types de Rust est censé tenir une promesse forte : si votre code sûr compile, il ne peut pas avoir de pointeurs pendouillants, de data races ni d'utilisation après libération. Quand une issue GitHub a montré un extrait de Rust à l'air parfaitement sûr qui affiche des données absurdes extraites d'une frame de pile morte, et qu'il s'est avéré que la faille était là, dans le borrow checker de Rust, depuis onze ans, beaucoup de gens ont senti le sol trembler. Le bug laisse passer les exigences de durée de vie d'une struct via une affectation de champ covariante, et avec un impl Drop malveillant, on peut stocker une référence à une variable locale dans une globale et la lire après la disparition de la variable. AddressSanitizer parle de stack-use-after-scope. Le compilateur, lui, n'a rien trouvé à redire.

Les réactions étaient prévisibles. Certains ont déclaré que l'argument de sûreté de Rust était mort. D'autres ont haussé les épaules : les bugs, ça arrive. Les deux passent à côté de ce qui est vraiment intéressant. Ce bug est une expérience naturelle très claire sur ce que valent les garanties statiques, sur l'endroit où le raisonnement informel montre ses limites, et sur le fait que c'est dans l'écart entre « le système de types est sûr » et « le compilateur applique effectivement un système de types sûr » que se cachent les bugs les plus intéressants. Alors examinons les idées reçues que cette histoire a fait remonter, une par une.

Mythe 1 : une faille d'unsoundness prouve que le modèle de sûreté de Rust a échoué

Le premier réflexe consiste à y voir une fissure dans la théorie. Ce n'est pas le cas. Personne n'a réécrit les règles des durées de vie. Personne n'a découvert que la propriété et l'emprunt sont fondamentalement cassés. Le système de types de Rust, tel qu'il a été conçu sur des tableaux blancs et dans les RFC, dit que ce programme doit être rejeté. Le compilateur n'a simplement pas réussi à le rejeter.

Cette distinction entre spécification et implémentation est l'une des plus anciennes lignes de fracture de notre domaine. Tony Hoare nous a offert une belle théorie des processus séquentiels communicants ; pendant des décennies, des compilateurs C ont ensuite mal compilé du code parfaitement valide selon la norme. La théorie tient alors que l'artefact fuit. Nous avons déjà expliqué pourquoi l'écart entre spécification et implémentation est l'endroit où naissent les bugs, et ce cas en est un exemple d'école. Les règles de durée de vie n'étaient pas fausses. Le code d'inférence de variance de rustc, celui qui décide quand il est légal de substituer un &'a T à un &'static T attendu, avait un trou lorsque l'affectation passait par un champ covariant.

Voici, en version simplifiée, la forme de l'exploit. Vous construisez un wrapper dont l'impl Drop copie sa charge utile dans un stockage global 'static. Normalement, le compilateur force la charge utile à être 'static, donc des références à des locales ne peuvent pas y entrer. Le bug permet de blanchir une référence de courte durée via une affectation covariante, si bien que le wrapper finit par contenir &l où l est une 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
}

Chaque ligne, prise isolément, paraît innocente. L'unsoundness n'existe que dans la composition : un champ covariant, une affectation qui relâche une borne de durée de vie, et un Drop qui déplace la charge utile vers un endroit où elle survit à son référent. C'est la signature typique des bugs d'implémentation dans les vérificateurs : l'invariant est global, mais son application est locale, et un chemin de code a oublié de vérifier.

Donc non, le modèle de sûreté n'a pas échoué. C'est l'application de ce modèle qui a échoué. C'est un échec plus petit, mais, comme on le verra, pas anodin pour autant.

Mythe 2 : onze ans sans détection, donc le bug est inoffensif

Le raisonnement de triage de l'équipe Rust est en gros le suivant : ce serait P-critique si des gens le rencontraient, mais onze ans sans aucun signalement signifient qu'il doit être difficile à déclencher, donc il est P-high. Il y a du vrai là-dedans. Pour provoquer réellement une corruption mémoire, il faut une impl Drop délibérément vicieuse qui déplace des données vers un emplacement 'static. Presque personne n'écrit ça. La surface d'exposition accidentelle est minuscule.

Mais « rarement déclenché par accident » porte beaucoup de poids dans cette phrase. Les garanties de sûreté ne concernent pas seulement les accidents : elles concernent ce sur quoi on peut compter quand le code autour de nous n'est pas bienveillant. Le principe même d'un système de types sûr est de pouvoir raisonner de manière modulaire : je n'ai pas besoin d'auditer votre impl Drop, parce que le compilateur a déjà prouvé que certaines mauvaises compositions sont inexprimables. Dès qu'il y a une faille, cette modularité disparaît. Une dépendance malveillante, ou une dépendance subtilement fausse écrite par un auteur bien intentionné, peut alors faire ce que le langage promettait être impossible.

L'histoire regorge de bugs « inexploitables » qui sont devenus très exploitables dès qu'est apparu le bon gadget. La question pratique, comme l'a fait remarquer un commentateur, est de savoir si la correction cassera un crate réel de l'écosystème, et la réponse est probablement « très peu, voire aucun », ce qui est une bonne nouvelle. Mais la bonne leçon de onze années silencieuses n'est pas « le bug était inoffensif ». C'est que l'absence de preuve n'est pas la preuve de l'absence, surtout pour des modes de défaillance qui requièrent une intention plutôt que le hasard.

Mythe 3 : avec assez de regards, tous les bugs deviennent superficiels

C'est le mythe qui devrait le plus nous gêner. rustc est l'un des compilateurs les plus scrutés jamais écrits. Il est open source, il a une équipe types dédiée, une communauté académique active (RustBelt nous a donné il y a des années un modèle formel d'un noyau de Rust), et des millions d'utilisateurs qui le sollicitent chaque jour. Et pourtant, une faille de solidité est restée dans l'inférence des durées de vie pendant plus de dix ans, à travers des réécritures complètes du mécanisme environnant.

La loi de Linus suppose que les regards se portent au bon endroit, avec le bon modèle en tête. Les unsoundness du système de types mettent ces deux hypothèses en échec. Elles naissent à l'intersection de plusieurs fonctionnalités (variance, ordre de drop, coercition, bornes de traits), et chaque fonctionnalité est localement correcte. Les relecteurs lisent le code et voient l'invariant voulu, parce que le code a été écrit par des personnes qui voyaient aussi cet invariant. Le biais de confirmation est intégré au processus. Le contre-exemple exige de penser en adversaire, et raisonner ainsi sur ses propres abstractions est franchement difficile.

Il existe tout un site, counterexamples.org, qui recense les façons dont des règles de types d'apparence plausible se cassent, et le point commun est la mutabilité combinée à autre chose de subtil, exactement la forme de ce bug. Ces leçons ne sont pas nouvelles. Le système de types de ML a eu une célèbre unsoundness autour des références mutables et du polymorphisme, corrigée par la restriction de valeur. Les tableaux Java sont covariants et peuvent lever une ArrayStoreException à l'exécution, parce que les concepteurs du langage ont préféré la commodité à la solidité. Plus les choses changent, plus les mêmes trois ingrédients (sous-typage, mutation et génériques) se combinent pour mordre quelqu'un. Si ce genre d'archéologie vous plaît, l'histoire de soixante ans de Lisp montre depuis combien de temps ces idées évoluent, et les anciennes règles de Rob Pike sur la simplicité se lisent autrement quand on réalise que la complexité est le terreau des failles de solidité.

Les regards aident. Ils ne suffisent pas. La position honnête, celle d'une personne qui conçoit son propre langage et que j'ai entendue, est plutôt la suivante : aucune quantité de revue ne résout tous les problèmes, donc il faut des méthodes mécaniques qui ne se fatiguent pas et ne partagent pas vos hypothèses.

Mythe 4 : le raisonnement informel vaut à peu près une preuve

Quand les règles de durée de vie de Rust ont été conçues, elles ont été argumentées avec soin, par des gens intelligents, sur la base de nombreux exemples. C'est du raisonnement informel, et c'est ainsi que sont construits pratiquement tous les compilateurs de production. Le résultat est un système sûr pour autant que quiconque puisse en juger, ce qui, nous venons de le réapprendre une deuxième fois, n'est pas la même chose que sûr.

L'écart entre les deux est précisément là où interviennent des projets comme RustBelt et les travaux en cours sur un solveur de traits de nouvelle génération. RustBelt, écrit en Coq (désormais Rocq) sur le cadre de logique de séparation Iris, a vérifié mécaniquement un modèle des règles de typage du cœur de Rust, y compris les parties délicates comme les frontières d'abstraction unsafe. C'était une étape majeure. Mais remarquez ce qu'elle a prouvé : un modèle de Rust, pas rustc. La preuve porte sur le calcul λRust, et le compilateur de production a dérivé, gagné des fonctionnalités et accumulé des choix d'implémentation que personne n'a revérifiés. Ce problème est la facture de cette dérive.

Formaliser l'intégralité d'un compilateur de production coûte terriblement cher. CompCert, le compilateur C formellement vérifié, a demandé des années d'effort expert pour un langage bien plus petit que Rust, et il vérifie les passes de compilation plutôt que de prouver que le système de types source attrape tous les programmes incorrects. Personne ne va écrire une preuve en Coq des deux millions de lignes de rustc. La voie réaliste ressemble plutôt à une défense en profondeur :

• Des modèles vérifiés mécaniquement des règles de base (à la manière de RustBelt), pour que la théorie elle-même n'ait pas de trous.
• Du fuzzing systématique et des outils d'analyse de cas qui génèrent des programmes adverses : les coins d'interaction entre fonctionnalités auxquels les humains ne pensent pas à tester.
• Des tests de mutation et des tests basés sur les propriétés du vérificateur : si modifier une borne doit faire échouer un programme, on vérifie qu'il échoue. La culture de test de SQLite est ici le modèle.
• Une liste maintenue des problèmes d'unsoundness connus (Rust en a plus d'une centaine d'étiquetés), traitée comme un backlog avec une priorité d'ingénierie, et non comme du folklore.

Fait intéressant, la recherche assistée par LLM pourrait finir par être un atout net : un outil qui compose inlassablement les fonctionnalités de façon perverse est exactement l'adversaire qui manque au raisonnement informel. La fin de partie que beaucoup d'entre nous espèrent est un Rust formellement spécifié, avec un vérificateur prouvé par rapport à cette spécification. Mais d'ici là, le travail est laborieux, peu glamour, et ressemble à de la résolution de contraintes.

Mythe 5 : si la solidité n'est pas absolue, la sûreté statique est une arnaque

La lecture cynique va ainsi : Rust promettait la sûreté, la promesse comportait une faille, donc la promesse était du marketing et autant revenir à manipuler des pointeurs en C à l'arraché. C'est exactement l'inverse, et il vaut la peine de dire pourquoi avec un peu de précision.

La solidité d'un système de types est un théorème portant sur un objet mathématique. Ce qu'un langage de production vous donne, c'est une garantie statistique et économique : des classes entières de bugs (utilisation après libération, data races, invalidation d'itérateurs) passent de « bruit de fond constant de votre base de code » à des événements suffisamment rares pour faire la une quand on les trouve après onze ans. Comparez les taux de base. Les bugs de sécurité mémoire dans les grosses bases C et C++ représentent la majorité des CVE graves, année après année, et plus personne n'est surpris par chacun d'eux. Les bugs d'unsoundness de Rust sont si rares que chacun obtient sa propre issue GitHub, son propre fil de discussion et sa propre culture de postmortem. Une rareté que l'on peut énumérer est un monde différent d'une rareté qu'on ne peut pas énumérer.

Il existe aussi une différence dans la manière dont les défaillances s'accumulent. En C, chaque ligne est un risque potentiel pour la mémoire, donc le coût vigilance croît avec la taille du code, indéfiniment. En Rust, la vigilance se concentre aux bords : les blocs unsafe, le FFI et (comme nous le savons maintenant) le vérificateur du compilateur lui-même. Cette concentration rend possibles l'audit, des outils comme Miri, et les méthodes formelles. La garantie n'est pas binaire ; c'est une refonte radicale de l'endroit où se situe votre risque.

Un système de types qui présente un bug connu, que onze ans de trafic en production n'ont jamais atteint, reste infiniment plus solide qu'un langage où le bug fait partie du design.

Ce qu'il faut vraiment retenir

Si vous écrivez du Rust, vous n'avez rien à changer. Votre code n'était pas silencieusement dangereux avant le dépôt de cette issue ; le chemin d'exploitation pratique exigeait une intention malveillante. Si vous maintenez des bibliothèques, la démarche honnête est toujours la même : gardez une surface unsafe réduite, lancez Miri sur les parties délicates, et ne considérez pas le borrow checker comme un oracle face au code malveillant des autres. Traitez-le comme un outil extrêmement fiable pour attraper vos propres erreurs.

Si vous concevez des langages ou des compilateurs, ce bug est un cadeau : un spécimen rare et bien documenté de la façon dont la solidité échoue réellement en production. Non pas dans la théorie, mais dans l'application ; non pas dans une seule fonctionnalité, mais à l'intersection de fonctionnalités ; non pas attrapé par la revue, mais par une construction adverse. Les équipes qui prennent cela au sérieux, en finançant la réécriture des solveurs de traits, le retravail des contraintes de régions et les outils proches de la vérification formelle, sont celles dont les garanties auront un sens dans dix ans.

Et pour tout le monde : recalibrez ce qu'est une garantie. Pendant des décennies, nous avons confondu « prouvé » et « argumenté de façon convaincante et jamais contredit jusqu'ici », dans les systèmes de types, les protocoles cryptographiques et le consensus distribué. La version adulte de la confiance ne consiste pas à supposer que le pont est parfait. Elle consiste à savoir que le pont a des inspecteurs qui publient leurs constats, corrigent ce qu'ils trouvent et tiennent une liste publique des fissures qu'ils n'ont pas encore réparées. De ce point de vue, onze ans pour trouver une faille ne sont pas un réquisitoire. C'est la preuve que le système, le système humain autour du compilateur, fonctionne à peu près comme il le devrait.