Lean a prouvé l’exactitude du programme, mais un bug a été découvert à l’intérieur

(kirancodes.me)

1 points par GN⁺ 16 일 전 | 1 commentaires | Partager sur WhatsApp

En fuzzant une implémentation de zlib vérifiée formellement, un heap buffer overflow a été découvert dans lean_alloc_sarray du runtime Lean 4
Après plus de 100 millions de tests à l’aide du fuzzer IA Claude, de AFL++, d’AddressSanitizer et d’autres outils, 4 crashs et 1 vulnérabilité mémoire ont été confirmés
Les problèmes découverts se répartissent en deux catégories : un overflow du runtime et un déni de service (DoS) basé sur l’Out-of-Memory dans Archive.lean
Les algorithmes de compression et de décompression vérifiés étaient sûrs, mais des vulnérabilités existaient dans l’analyseur d’archives non vérifié et la couche runtime
En conséquence, la vérification formelle est puissante, mais sans sécurisation de la base de confiance de calcul (TCB), elle ne peut pas garantir la stabilité de l’ensemble du système

Bug découvert dans un programme ayant passé la vérification Lean

En fuzzant une implémentation de zlib vérifiée formellement avec Lean, un heap buffer overflow a été découvert dans le runtime Lean 4
- Le code applicatif vérifié ne présentait aucune vulnérabilité mémoire
- Mais un overflow s’est produit dans la fonction lean_alloc_sarray du runtime Lean, ce qui affecte toutes les versions de Lean 4
Plus de 100 millions d’itérations de fuzzing ont été effectuées à l’aide du fuzzer IA Claude, de AFL++, d’AddressSanitizer, de Valgrind, d’UBSan, etc.
- 16 fuzzers parallèles ont été lancés sur 6 surfaces d’attaque, dont la compression, la décompression et le traitement d’archives de lean-zip
- En 19 heures, 4 entrées provoquant des crashs et 1 vulnérabilité mémoire ont été découvertes
Deux bugs majeurs ont été confirmés
- Un heap buffer overflow dans lean_alloc_sarray du runtime Lean
- Un déni de service (DoS) basé sur l’Out-of-Memory dans le module Archive.lean de lean-zip
Les limites de la vérification formelle sont ainsi apparues
- Les algorithmes de compression et de décompression de lean-zip ont été entièrement vérifiés, mais l’analyseur d’archives (Archive.lean) ne l’a pas été, d’où la présence d’une vulnérabilité DoS
- Le bug du runtime est un problème interne à la base de confiance de calcul (Trusted Computing Base), qui affecte tous les programmes Lean
En conclusion, la vérification formelle de Lean a démontré la stabilité du code applicatif, mais des vulnérabilités subsistent toujours dans les composants en dehors du périmètre vérifié
- La vérification n’est puissante que dans le champ où elle est appliquée, et la sécurité de la couche de confiance fondamentale reste indispensable

Aperçu de l’expérience de fuzzing

Le code testé était l’implémentation zlib vérifiée de lean-zip
- Tous les théorèmes (theorem), spécifications (specification), documents et bindings C FFI ont été supprimés afin de ne conserver que du code Lean pur
- Claude n’a pas été informé du fait que le code était vérifié, afin d’éviter tout biais
Environnement expérimental
- 16 fuzzers parallèles ont été exécutés sur 6 surfaces d’attaque : ZIP, gzip, DEFLATE, tar, tar.gz et compression
- AddressSanitizer, UndefinedBehaviorSanitizer, Valgrind memcheck, cppcheck et flawfinder ont été utilisés en parallèle
- Avec 48 fichiers d’exploit conçus manuellement, un total de 105,823,818 exécutions a été réalisé à partir de 359 fichiers seed
- En 19 heures, 4 entrées provoquant des crashs et 1 vulnérabilité mémoire ont été découvertes

Bug 1 : heap buffer overflow dans le runtime Lean

Fonction vulnérable : lean_alloc_sarray
- Fonction qui alloue tous les tableaux scalaires comme ByteArray, FloatArray, etc.
- Un overflow d’entier peut se produire lors du calcul sizeof(lean_sarray_object) + elem_size * capacity
Cause du problème
- Lorsque capacity est proche de SIZE_MAX, l’addition déborde et un petit buffer est alloué
- Ensuite, l’appelant lit n octets, ce qui provoque un heap buffer overflow
Conditions de déclenchement
- Le problème survient dans lean_io_prim_handle_read lorsque nbytes a une valeur extrêmement grande
- Il peut être reproduit avec un fichier de 156 octets dont l’en-tête ZIP64 indique compressedSize à 0xFFFFFFFFFFFFFFFF
- Toutes les versions de Lean 4 sont affectées, y compris la dernière nightly
- Exemple de code de reproduction
```
def main : IO Unit := do
  IO.FS.writeFile "test.bin" "hello"
  let h ← IO.FS.Handle.mk "test.bin" .read
  let n : USize := (0 : USize) - (1 : USize)
  let _ ← h.read n
```
- L’exécution du code ci-dessus déclenche un overflow dans lean_alloc_sarray
- Une PR de correction a été soumise

Bug 2 : déni de service (DoS) dans l’analyseur d’archives de lean-zip

Fonction vulnérable : readExact (Archive.lean)
- Le champ compressedSize du répertoire central ZIP est utilisé tel quel, sans validation
- Lors de l’appel à h.read, une taille anormalement grande est demandée, ce qui provoque une allocation mémoire excessive et un OOM
Reproduction du problème
- Si un fichier ZIP de 156 octets prétend avoir une taille de plusieurs exaoctets, le processus se termine avec INTERNAL PANIC: out of memory
- L’outil système unzip vérifie la taille de l’en-tête, mais lean-zip ne le fait pas

Ce que la vérification formelle a laissé de côté

Cause de la vulnérabilité DoS
- Le module Archive.lean se trouve dans une zone non vérifiée
- Le pipeline de compression et de décompression (par ex. DEFLATE, Huffman, CRC32) est entièrement vérifié et ne présente pas de problème
- La vulnérabilité apparaît dans une partie à laquelle la vérification n’a pas été appliquée
Nature de l’overflow du runtime
- Le runtime Lean fait partie de la base de confiance de calcul (TCB)
- Toutes les preuves Lean supposent la correction du runtime
- Par conséquent, un bug du runtime affecte la sûreté de tous les programmes Lean

Stabilité du code vérifié

Résultat après 105 millions d’exécutions
- Dans le code C généré par Lean, aucun heap overflow, use-after-free, stack overflow, UB ou dépassement de borne de tableau n’a été observé
- Selon l’évaluation de Claude, il s’agit de « l’une des bases de code les plus sûres en mémoire »
Effet du système de types de Lean
- Grâce aux types dépendants (dependent types) et à une structure de récursion bien fondée (well-founded recursion), les vulnérabilités courantes (classes de CVE) des implémentations zlib en C/C++ sont bloquées de manière structurelle
Conclusion
- La zone de code vérifiée était très robuste et le fuzzer a eu du mal à y trouver des erreurs
- Mais des vulnérabilités subsistent dans les parties non vérifiées et dans la couche runtime
- La vérification est limitée par son périmètre d’application et par la sûreté de sa base de confiance

Enseignement clé

La vérification formelle est très puissante à l’intérieur du code auquel elle est appliquée, mais les composants périphériques non vérifiés ou la couche runtime peuvent menacer la stabilité de l’ensemble
La sécurisation de la base de confiance de calcul est indispensable, et même pour un système vérifié, la question demeure : « qui surveille les gardiens ? (Quis custodiet ipsos custodes) »

Liens de référence

1 commentaires

GN⁺ 16 일 전

Commentaires Hacker News

Le titre et l’angle de l’article m’ont semblé un peu bizarres
En réalité, l’auteur précise qu’il n’a trouvé ni bug ni erreur dans le code prouvé
Les deux bugs découverts se situaient hors du périmètre de la preuve : l’un était une spécification incomplète, l’autre un dépassement de tas dans le runtime C++
Je tiens à souligner que le bug a été trouvé dans le runtime de Lean, pas dans le kernel qui effectue la vérification
Voir la documentation Lean
- Je pense que lorsqu’on parle de bugs dans un système vérifié, il faut considérer l’ensemble du binaire
  Si vous perdez vos bitcoins à cause d’un buffer overflow, savoir que le bug se trouvait dans le runtime n’est pas très réconfortant
  Et si le programme plante, la plupart des utilisateurs considéreront que c’est un bug
  Il y a probablement pas mal de gens qui font tourner Lean en production réelle
- En lisant seulement le titre, j’ai cru qu’il y avait un bug dans le kernel de Lean, alors qu’en réalité le problème a été trouvé dans le runtime de Lean et dans lean-zip
  Si ce n’est pas dans le kernel, l’impact sur la fiabilité de la preuve elle-même est limité
- La spécification incomplète de lean-zip est un problème important du point de vue de la philosophie de la vérification
  Même si l’on vérifie un programme « Hello world », il faut spécifier non seulement la sortie, mais aussi les effets de bord
  Si une corruption mémoire se produit à la frontière entre le runtime et le kernel, la fiabilité de la preuve peut en pâtir
  En fin de compte, l’essentiel est de définir clairement ce qu’il faut vérifier
- En regardant la liste des articles de ce site, j’ai trouvé amusant qu’elle devienne de plus en plus putaclic
  Liste d’articles liée
- Dire qu’un bug du runtime Lean est un bug de lean-zip, c’est comme dire qu’un bug de la JRE est un bug d’une appli Java
  On a l’impression que l’auteur cherche délibérément à induire en erreur
J’ai eu une expérience similaire avec du code prouvé
Dans mon cas, ce n’était pas un overflow mais un défaut de spécification (spec bug)
Si la spécification est erronée, le code et la preuve peuvent être parfaits tout en produisant un comportement différent de celui qui était voulu
Au fond, la difficulté de la vérification vient du fait qu’il faut exprimer précisément l’intention humaine
Croire que l’IA résoudra parfaitement la vérification peut donner une fausse confiance
- J’ai eu une expérience du même genre
  Les spécifications que l’on peut prouver avec des outils comme Lean, TLA+ ou Z3 sont simplifiées et nécessitent beaucoup d’hypothèses
  Cela reste malgré tout un outil puissant
  Cela permet de réduire le champ des bugs dans des algorithmes complexes et de voir clairement les frontières de la spécification
  Grâce à l’IA, ce type de travail de preuve est devenu bien plus facile
- La question qui revient toujours est : « comment faire confiance au système de vérification lui-même ? »
  Après tout, un autre programme qui vérifie un programme peut lui aussi contenir des bugs
  L’impossibilité d’une auto-vérification complète fait penser au principe d’incertitude de Heisenberg
  Au final, la vérification est un processus qui augmente la confiance via une « seconde implémentation indépendante »
- Les bugs dans mon code se répartissent en deux catégories
  (1) le programme ne fait pas ce qui était prévu
  (2) il fait exactement ce qui était prévu, mais cette intention était mauvaise
  Les assistants de preuve empêchent le cas (1), mais pas le cas (2)
  Autrement dit, on ne peut pas prouver la solidité de la conception
  Tout vérifier comme seL4 coûte trop cher et prend trop de temps
- Je pense qu’il faut un moyen de vérifier la spécification elle-même
  L’idéal serait de combiner logique formelle + pensée adversariale (adversarial thinking) afin d’énumérer complètement ce que le programme doit faire et ne doit pas faire
Le titre m’a semblé putaclic
Il n’y avait pas de bug dans la partie prouvée, donc je ne comprends pas pourquoi cela a été formulé ainsi
Sur HN, j’aimerais lire des articles fondés sur les faits, et là c’était une perte de temps
- Est-il juste, pour un logiciel vérifié, de considérer que « seuls les bugs qui violent la preuve sont de vrais bugs » ?
  On fait la pub du logiciel comme « sans bug », mais en réalité c’est seulement « dans la mesure où la spécification est parfaitement exprimée »
  Même parfaitement correct, cela peut être correct mais mort dans le monde réel — autrement dit, théoriquement juste mais pratiquement cassé
- Le titre est techniquement exact, mais il présente un problème survenu dans le code non vérifié de lean-zip comme s’il s’agissait d’un bug de la partie prouvée
- Au final, le message « clarifiez le périmètre de ce qui est prouvé » est intéressant et pertinent
- Le deuxième bug donne l’impression d’avoir été inventé sans fondement
  Il n’y a pas de référence au code, et dès qu’on regarde le code réel, on comprend qu’il s’agit d’un malentendu
- Au final, lean-zip n’est qu’un simple binding Zlib
Ce problème apparaît souvent aussi dans la vérification des systèmes distribués
Une preuve n’est valable que dans certaines conditions précises, et les défaillances intéressantes se produisent à ces frontières
Avec TLA+ aussi, dès que la réalité s’écarte des hypothèses, la preuve devient inutile
Ce que je voudrais, c’est une façon de spécifier mécaniquement le domaine de validité et de le surveiller à l’exécution
- Il m’est déjà arrivé de découvrir moi-même un bug matériel sur un CPU
  Mais la plupart des bugs ne viennent pas du matériel, ils viennent du fait que les gens ne lisent pas la documentation
  Rien qu’avec la modélisation formelle, on peut déjà réduire énormément le nombre de bugs
C’est une bonne nouvelle prévisible
Cela signifie que les LLM peuvent produire du code qui passe la vérification formelle
À l’avenir, les bugs vont de plus en plus se déplacer vers la couche matérielle
On finira donc par avoir besoin d’une formalisation des spécifications matérielles
Si les fabricants ne les publient pas, cela pourrait créer des tensions avec la communauté
À long terme, on se dirigera soit vers l’extinction des vulnérabilités, soit vers leur insertion intentionnelle
Au début, j’ai cru que l’auteur n’avait pas testé la partie prouvée
Mais en lisant, j’ai vu que les bugs avaient été trouvés hors du périmètre de la preuve
Du coup, le titre m’a semblé un peu exagéré
- L’auteur du billet est lui-même intervenu
  Il soutient que, pour parler d’un bug dans un système vérifié, il faut considérer le binaire dans son ensemble
  Il précise avoir effectivement trouvé une entrée qui provoque un crash dans la partie d’analyse des en-têtes compressés de Archive.lean
Cela m’a rappelé la célèbre formule de Donald Knuth
« Méfiez-vous des bugs dans le code ci-dessus ; je me suis contenté de prouver qu’il était correct, je ne l’ai pas exécuté. »
Le fait de ne pas avoir vérifié le parseur me semble être une grosse erreur
L’analyse de formats binaires est toujours une zone à risque
Le point essentiel, c’est qu’un agent IA a collaboré avec un fuzzer pour découvrir un heap buffer overflow dans Lean
C’est une réussite assez importante
- Je pense aussi que c’est une découverte vraiment utile
J’ai trouvé frappant le passage où Claude dit : « c’est l’une des bases de code les plus sûres en mémoire que j’aie analysées »
Mais on aurait dit une blague, comme si c’était la première base de code que Claude analysait
- Il est peu probable que Claude, largement entraîné en RL, analyse ici sa première base de code
  C’est précisément pour cela qu’il est aussi bon
- Peut-être que Claude est en train de faire quelque chose de secret dont nous ne savons rien 😄

Lean a prouvé l’exactitude du programme, mais un bug a été découvert à l’intérieur

Bug découvert dans un programme ayant passé la vérification Lean

Aperçu de l’expérience de fuzzing

Environnement expérimental

Bug 1 : heap buffer overflow dans le runtime Lean

Cause du problème

Conditions de déclenchement

Bug 2 : déni de service (DoS) dans l’analyseur d’archives de lean-zip

Reproduction du problème

Ce que la vérification formelle a laissé de côté

Cause de la vulnérabilité DoS

Nature de l’overflow du runtime

Stabilité du code vérifié

Résultat après 105 millions d’exécutions

Effet du système de types de Lean

Conclusion

Enseignement clé

Liens de référence

À lire aussi

1 commentaires

Commentaires Hacker News