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

(kirancodes.me)

1 points par GN⁺ 14 일 전 | Aucun commentaire pour le moment. | 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) »

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

Aucun commentaire pour le moment.