runtimeverification/kernel-c-to-rust-spikeDurcissement des analyseurs C du noyau via une réécriture en Rust + fuzzing différentiel + vérification formelle. Première cible : UVC (CVE-2024-53104).
Un parseur C du noyau Linux critique pour la sécurité peut-il être durci en le réécrivant en Rust, la réécriture étant démontrée équivalente à l'original puis formellement vérifiée ? Cette analyse exploratoire exécute la boucle complète sur une cible : le parseur de descripteurs vidéo UVC (uvc_parse_format/uvc_parse_frame de drivers/media/usb/uvc/, v7.2-rc2), choisi parce qu'il a porté deux CVE indépendantes de sûreté mémoire à seize ans d'intervalle (CVE-2008-3496, CVE-2024-53104, cette dernière figurant dans le catalogue KEV de la CISA).
Extraction de la feuille C (c/). La logique d'analyse copiée octet pour octet depuis le noyau ; seul l'environnement est remplacé par des stubs (// SPIKE-STUB). Compilée en bibliothèque à ABI C. La feuille extraite inclut la passe de comptage et l'allocation dimensionnée, de sorte que la classe de bug CVE-2024-53104 (l'analyse écrivant au-delà de ce que le comptage a alloué) est atteignable, et non abstraite.
Réécriture en Rust (rust/). La même feuille d'analyse en Rust sûr, même ABI C et même structure de résultat. Chaque écart par rapport au C est marqué // DEVIATION et documenté.
Fuzzing différentiel (fuzz/). Un harnais LibAFL sur rustc stable pilote les deux implémentations à partir d'une même entrée et compare les sorties champ par champ. Résultat : après correction d'une divergence de portage sur un site de dépassement signé dépendant du compilateur, zéro divergence sur 54 019 exécutions à 93 % de couverture des arêtes. Sur le code fidèle v7.2-rc2, aucun accès hors bornes n'est atteignable (les deux CVE sont corrigées). Un contrôle négatif optionnel (--features vuln, reproduit dans les deux langages) réintroduit la discordance CVE-2024-53104 : sur la même entrée, le C effectue une écriture hors bornes sur le tas (ASan), le Rust panique de manière sûre. Détails : fuzz/RESULTS.md.
Vérification formelle (verify/). La feuille Rust fidèle s'extrait via Charon et Aeneas vers Lean 4 sans aucun sorry dans le code généré, et sans blocage lié aux unions (contrairement à l'analyse exploratoire Binder). Deux théorèmes, dans verify/VERIFY-REPORT.md et ROADMAP.md :
ok / fail contrôlé / non-terminaison, jamais une issue de comportement indéfini) : prouvé, sans sorry. Cela rend explicite, sous forme d'énoncé vérifié, la propriété de sûreté mémoire dont le C est dépourvu.sorry, ainsi que deux principes réutilisables de raisonnement sur les boucles Aeneas et l'absence de division pour les 5 boucles à terminaison structurelle. Le reste se réduit à un cœur de correction fonctionnelle nommé, un parcours positionnel (quatre lemmes énoncés) ; voir ROADMAP.md.La boucle est démontrée de bout en bout sur une cible. La réécriture est démontrée équivalente au C par fuzzing différentiel ; la différence de sûreté mémoire est rendue concrète par le contrôle négatif ; le Rust s'extrait proprement vers Lean et sa propriété de sûreté totale est vérifiée par la machine. Pour le théorème d'absence de panique, l'invariant de comptage (le cœur de CVE-2024-53104) est prouvé sans sorry et le travail restant se réduit à un cœur de correction fonctionnelle nommé, énoncé mais pas encore prouvé. L'état complet des preuves et les lemmes ouverts figurent dans ROADMAP.md.
c/ — la feuille C extraite et ses stubsrust/ — la réécriture en Rust sûrfuzz/ — le fuzzer différentiel LibAFL, les résultats et le contrôle de classe CVEverify/ — extraction Charon/Aeneas/Lean et théorèmesROADMAP.md — état des preuves et lemmes ouverts restantsOPEN_CHALLENGES.md — tâches concrètes qu'un contributeur peut prendre en charge*/README.md, fuzz/RESULTS.md, verify/VERIFY-REPORT.md — détails par étapeNoyau v7.2-rc2 (référence en lecture seule). Rust stable 1.94.0. LibAFL 0.15.
Charon 909ff09a (v0.1.220, --preset=aeneas), Aeneas c2015b86, Lean/mathlib
v4.31.0.