Lean hat die Korrektheit des Programms bewiesen, doch darin wurde ein Bug gefunden

 (kirancodes.me)
1 Punkte von GN⁺ 14 일 전 | 1 Kommentare | Auf WhatsApp teilen
  • Beim Fuzzing einer formal verifizierten zlib-Implementierung wurde in lean_alloc_sarray der Lean-4-Runtime ein Heap-Buffer-Overflow entdeckt
  • Mithilfe des KI-Fuzzers Claude sowie AFL++ und AddressSanitizer wurden nach mehr als 100 Millionen Tests 4 Crashes und 1 Speicher-Schwachstelle bestätigt
  • Die gefundenen Probleme lassen sich in zwei Typen einteilen: einen Runtime-Overflow und eine Out-of-Memory-basierte Denial-of-Service-(DoS)-Schwachstelle in Archive.lean
  • Die verifizierten Kompressions- und Dekompressionsalgorithmen waren sicher, doch in dem nicht verifizierten Archiv-Parser und der Runtime-Schicht existierten Schwachstellen
  • Formal Verification ist damit zwar mächtig, kann aber ohne die Absicherung der Trusted Computing Base (TCB) nicht die Stabilität des Gesamtsystems garantieren

Bug in einem Programm gefunden, das die Lean-Verifikation bestanden hat

  • Beim Fuzzing einer mit Lean formal verifizierten zlib-Implementierung wurde in der Lean-4-Runtime ein Heap-Buffer-Overflow entdeckt
    • Im verifizierten Anwendungscode gab es keine Speicher-Schwachstellen
    • Allerdings trat in der Funktion lean_alloc_sarray der Lean-Runtime ein Overflow auf, der alle Lean-4-Versionen betrifft
  • Mit dem KI-basierten Fuzzer Claude sowie AFL++, AddressSanitizer, Valgrind, UBSan usw. wurden mehr als 100 Millionen Fuzzing-Durchläufe durchgeführt
    • 16 parallele Fuzzer liefen gegen 6 Angriffsflächen von lean-zip, darunter Kompression, Dekompression und Archivverarbeitung
    • Innerhalb von 19 Stunden wurden 4 Crash-Eingaben und 1 Speicher-Schwachstelle gefunden
  • Zwei wesentliche Bugs wurden bestätigt
    • Heap-Buffer-Overflow in lean_alloc_sarray der Lean-Runtime
    • Out-of-Memory-basierte Denial-of-Service-(DoS)-Schwachstelle im Modul Archive.lean von lean-zip
  • Die Grenzen der formalen Verifikation wurden sichtbar
    • Die Kompressions- und Dekompressionsalgorithmen von lean-zip waren vollständig verifiziert, der Archiv-Parser (Archive.lean) jedoch nicht, wodurch eine DoS-Schwachstelle bestehen konnte
    • Der Runtime-Bug ist ein Problem innerhalb der Trusted Computing Base, das alle Lean-Programme betrifft
  • Fazit: Die formale Verifikation von Lean belegte die Stabilität des Anwendungscodes, doch in Komponenten außerhalb des Verifikationsumfangs bestehen weiterhin Schwachstellen
    • Verifikation ist nur in dem Bereich stark, auf den sie angewendet wurde; die Sicherheit der grundlegenden Vertrauensebene ist daher essenziell

Überblick über das Fuzzing-Experiment

  • Die Codebasis war die verifizierte zlib-Implementierung von lean-zip
    • Alle Theoreme, Spezifikationen, Dokumentation und C-FFI-Bindings wurden entfernt, sodass nur reiner Lean-Code übrig blieb
    • Claude sollte nicht erkennen, dass der Code verifiziert war, um Verzerrungen zu vermeiden

  • Testumgebung

    • 16 parallele Fuzzer liefen gegen 6 Angriffsflächen, darunter ZIP, gzip, DEFLATE, tar, tar.gz und Kompression
    • AddressSanitizer, UndefinedBehaviorSanitizer, Valgrind memcheck, cppcheck und flawfinder wurden parallel eingesetzt
    • Einschließlich 48 manuell erstellter Exploit-Dateien wurden insgesamt 105.823.818 Ausführungen mit 359 Seed-Dateien durchgeführt
    • Innerhalb von 19 Stunden wurden 4 Crash-Eingaben und 1 Speicher-Schwachstelle gefunden

Bug 1: Heap-Buffer-Overflow in der Lean-Runtime

  • Verwundbare Funktion: lean_alloc_sarray
    • Eine Funktion zum Allokieren aller Skalar-Arrays wie ByteArray und FloatArray
    • Bei der Berechnung sizeof(lean_sarray_object) + elem_size * capacity kann es zu einem Integer-Overflow kommen

  • Ursache des Problems

    • Wenn capacity nahe bei SIZE_MAX liegt, läuft die Addition über und es wird ein zu kleiner Buffer allokiert
    • Danach liest der Aufrufer n Bytes ein, wodurch ein Heap-Buffer-Overflow entsteht

  • Trigger-Bedingungen

    • Tritt in lean_io_prim_handle_read auf, wenn nbytes einen sehr großen Wert hat
    • Lässt sich mit einer 156-Byte-Datei reproduzieren, deren ZIP64-Header compressedSize auf 0xFFFFFFFFFFFFFFFF setzt
    • Betrifft alle Versionen von Lean 4, einschließlich des neuesten Nightly-Builds
    • Beispielcode zur Reproduktion
    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
    • Beim Ausführen dieses Codes tritt der Overflow in lean_alloc_sarray auf
    • Ein Fix-PR wurde eingereicht

Bug 2: Denial of Service (DoS) im Archiv-Parser von lean-zip

  • Verwundbare Funktion: readExact (Archive.lean)
    • Das Feld compressedSize im ZIP Central Directory wird ungeprüft übernommen
    • Beim Aufruf von h.read wird eine abnormal große Größe angefordert, was zu übermäßiger Speicherallokation und OOM führt

  • Reproduktion des Problems

    • Wenn eine 156-Byte-ZIP-Datei behauptet, mehrere Exabyte groß zu sein, beendet sich der Prozess mit INTERNAL PANIC: out of memory
    • Das System-unzip validiert die Header-Größe, lean-zip tut dies jedoch nicht

Was die formale Verifikation übersehen hat

  • Ursache der DoS-Schwachstelle

    • Das Modul Archive.lean ist ein nicht verifizierter Bereich
    • Die Kompressions- und Dekompressions-Pipeline (z. B. DEFLATE, Huffman, CRC32) ist vollständig verifiziert und unauffällig
    • Die Schwachstelle entstand in einem Bereich, auf den keine Verifikation angewendet wurde

  • Das Wesen des Runtime-Overflows

    • Die Lean-Runtime gehört zur Trusted Computing Base (TCB)
    • Alle Lean-Beweise setzen die Korrektheit der Runtime voraus
    • Daher beeinflusst ein Runtime-Bug die Sicherheit aller Lean-Programme

Stabilität des verifizierten Codes

  • Ergebnis nach 105 Millionen Ausführungen

    • Im von Lean erzeugten C-Code gab es keine Heap-Overflows, kein use-after-free, keine Stack-Overflows, kein UB und keine Array-Out-of-Bounds-Fehler
    • Laut der Bewertung von Claude handelt es sich um „eine der speichersichersten Codebasen überhaupt“

  • Wirkung des Typsystems von Lean

    • Abhängige Typen (dependent types) und well-founded recursion verhindern strukturell Schwachstellenklassen (CVE-Klassen), die in C/C++-basierten zlib-Implementierungen häufig sind

  • Fazit

    • Der verifizierte Codebereich war äußerst robust, und der Fuzzer konnte dort nur schwer Fehler finden
    • In nicht verifizierten Bereichen und in der Runtime-Schicht bestehen jedoch weiterhin Schwachstellen
    • Verifikation ist durch ihren Anwendungsbereich und die Sicherheit der Vertrauensbasis begrenzt

Zentrale Lehre

  • Formale Verifikation ist innerhalb des angewendeten Codebereichs äußerst stark, doch nicht verifizierte umgebende Komponenten oder die Runtime-Schicht können die Gesamtstabilität weiterhin gefährden
  • Die Absicherung der Trusted Computing Base ist unverzichtbar, und selbst bei verifizierten Systemen bleibt die Frage: „Wer bewacht die Wächter? (Quis custodiet ipsos custodes)“

Weiterführende Links

Verwandte Beiträge

1 Kommentare

 
GN⁺ 14 일 전
Hacker-News-Kommentare

  • Titel und Framing dieses Artikels wirkten etwas seltsam
    Tatsächlich stellt der Autor ausdrücklich klar, dass er im bewiesenen Code keine Bugs oder Fehler finden konnte
    Die beiden entdeckten Bugs lagen außerhalb des Beweisumfangs: einer war eine fehlende Spezifikation, der andere ein Heap-Overflow in der C++-Laufzeit
    Ich möchte betonen, dass der Bug in der Laufzeitumgebung von Lean gefunden wurde, nicht im Kernel, der die Verifikation ausführt
    Siehe Lean-Dokumentation

    • Ich denke, wenn man in einem verifizierten System über Bugs spricht, muss man das gesamte Binärprogramm betrachten
      Wenn man durch einen Buffer Overflow Bitcoin verliert, ist es kein Trost, dass der Bug in der Laufzeit lag
      Und wenn ein Programm abstürzt, werden die meisten Nutzer das als Bug ansehen
      Es dürfte auch einige geben, die Lean tatsächlich in Produktionsumgebungen einsetzen
    • Nur anhand des Titels dachte ich, es gäbe einen Bug im Lean-Kernel, tatsächlich wurden die Probleme aber in der Lean-Laufzeit und in lean-zip gefunden
      Wenn nicht der Kernel betroffen ist, hat das auf die Vertrauenswürdigkeit des Beweises selbst keine großen Auswirkungen
    • Die fehlende Spezifikation in lean-zip ist aus Sicht der Verifikationsphilosophie ein wichtiges Problem
      Selbst wenn man ein „Hello world“-Programm verifiziert, muss man nicht nur die Ausgabe, sondern auch die Nebenwirkungen spezifizieren
      Wenn an der Grenze zwischen Laufzeit und Kernel Speicherbeschädigung entsteht, kann das die Vertrauenswürdigkeit des Beweises mindern
      Letztlich ist entscheidend, klar zu definieren, was verifiziert werden soll
    • Als ich die Artikelliste auf dieser Website gesehen habe, fand ich es interessant, wie clickbait-artig sie zunehmend wirkt
      Verwandte Artikelliste
    • Einen Bug in der Lean-Laufzeit als Bug in lean-zip zu bezeichnen, ist so, als würde man einen Bug in der JRE einen Bug in einer Java-App nennen
      Es wirkt, als habe der Autor absichtlich Missverständnisse provoziert

  • Ich hatte mit bewiesenem Code eine ähnliche Erfahrung
    In meinem Fall war nicht ein Overflow das Problem, sondern ein Spezifikationsfehler (spec bug)
    Wenn die Spezifikation falsch ist, können Code und Beweis perfekt sein und trotzdem anders arbeiten als beabsichtigt
    Letztlich liegt die Schwierigkeit der Verifikation darin, menschliche Absichten präzise auszudrücken
    Der Glaube, KI werde Verifikation perfekt lösen, kann zu falscher Sicherheit führen

    • Ich habe etwas Ähnliches erlebt
      Spezifikationen, die sich mit Werkzeugen wie Lean, TLA+ oder Z3 beweisen lassen, sind vereinfacht und erfordern viele Annahmen
      Trotzdem ist das ein mächtiges Werkzeug
      Es hilft dabei, Bugs in komplexen Algorithmen einzugrenzen und die Grenzen der Spezifikation klar zu erkennen
      Dank KI ist diese Art von Beweisarbeit viel einfacher geworden
    • Die Frage, die sich immer stellt, ist: Wie kann man dem Verifikationssystem selbst vertrauen?
      Auch ein weiteres Programm, das ein Programm verifiziert, kann am Ende Bugs haben
      Dass vollständige Selbstverifikation unmöglich ist, erinnert an Heisenbergs Unschärferelation
      Letztlich ist Verifikation ein Prozess, das Vertrauen über eine „zweite unabhängige Implementierung“ zu erhöhen
    • Die Bugs in meinem Code lassen sich in zwei Arten einteilen
      (1) Fälle, in denen er anders arbeitet als beabsichtigt
      (2) Fälle, in denen er wie beabsichtigt arbeitet, aber diese Absicht falsch ist
      Beweisassistenten verhindern (1), aber nicht (2)
      Das heißt, die Solidität des Entwurfs lässt sich nicht beweisen
      So etwas wie bei seL4 alles zu verifizieren, ist zu teuer und dauert zu lange
    • Ich denke, wir brauchen eine Möglichkeit, die Spezifikation selbst zu verifizieren
      Ideal wäre eine Kombination aus formaler Logik + adversarial thinking, um vollständig aufzulisten, was ein Programm tun und was es nicht tun darf

  • Der Titel wirkte wie Clickbait
    Im bewiesenen Teil gab es keine Bugs, daher verstehe ich nicht, warum es so formuliert wurde
    Auf HN möchte ich faktenbasierte Beiträge sehen, und das hier war Zeitverschwendung

    • Ist es fair, bei verifizierter Software zu sagen, nur Bugs, die den Beweis verletzen, seien überhaupt Bugs?
      Man wirbt mit „keine Bugs“, aber in Wirklichkeit gilt das nur „innerhalb des Bereichs, in dem die Spezifikation vollständig ausgedrückt wurde“
      Man kann vollkommen richtig und in der Realität trotzdem tot richtig sein — also theoretisch korrekt, aber praktisch kaputt
    • Der Titel ist technisch gesehen richtig, stellt aber ein Problem in nicht verifiziertem Code von lean-zip so dar, als wäre es ein Bug im bewiesenen Teil
    • Am Ende ist die Botschaft, „den Umfang des bewiesenen Teils klar zu machen“, interessant und berechtigt
    • Der zweite Bug wirkt so, als sei er ohne Grundlage erfunden worden
      Es gibt keinen Codeverweis, und wenn man sich den tatsächlichen Code ansieht, erkennt man, dass es ein Missverständnis ist
    • Letztlich ist lean-zip nur ein einfaches Zlib-Binding

  • Dieses Problem taucht auch bei der Verifikation verteilter Systeme häufig auf
    Beweise gelten nur unter bestimmten Bedingungen (im Betriebsbereich), und interessante Fehler treten an dieser Grenze auf
    Bei TLA+ ist es genauso: Wenn die Realität von den Annahmen abweicht, wird der Beweis bedeutungslos
    Ich hätte gern eine Funktion, die den Betriebsbereich maschinell festhält und ihn zur Laufzeit überwacht

    • Ich habe selbst schon direkt einen Hardware-Bug in einer CPU entdeckt
      Aber die meisten Bugs entstehen nicht durch Hardware, sondern dadurch, dass Menschen die Dokumentation nicht lesen
      Schon formale Modellierung allein kann die Zahl der Bugs massiv senken

  • Das sind vorhersehbar gute Nachrichten
    Es bedeutet, dass LLMs Code erzeugen können, der formale Verifikation besteht
    Künftig werden Bugs immer stärker in die Hardware-Schicht wandern
    Am Ende wird man die Formalisierung von Hardwarespezifikationen brauchen
    Wenn Hersteller das nicht offenlegen, könnte es Konflikte mit der Community geben
    Langfristig wird sich das entweder in Richtung Aussterben von Schwachstellen oder absichtlicher Einfügung entwickeln

  • Zuerst dachte ich, der Autor habe den bewiesenen Teil gar nicht getestet
    Beim Lesen stellte sich aber heraus, dass die Bugs außerhalb des Beweisumfangs gefunden wurden
    Deshalb wirkte der Titel etwas übertrieben

    • Der Autor des Beitrags meldet sich selbst zu Wort
      Er argumentiert, dass bei Bugs in einem verifizierten System das gesamte Binärprogramm betrachtet werden müsse
      Tatsächlich, so sagt er, habe er Eingaben gefunden, die im Parsing der komprimierten Header in Archive.lean Abstürze verursachen

  • Das erinnert mich an Donald Knuths berühmtes Zitat
    „Vorsicht, im obigen Code könnten Bugs sein. Ich habe nur bewiesen, dass er korrekt ist, ich habe ihn nicht ausgeführt“

  • Den Parser nicht verifiziert zu haben erscheint mir als großer Fehler
    Das Parsen von Binärformaten ist immer ein riskanter Bereich

  • Der Kernpunkt ist, dass ein KI-Agent in Zusammenarbeit mit einem Fuzzer in Lean einen Heap Buffer Overflow gefunden hat
    Das ist ein ziemlich großer Erfolg

    • Ich halte das für einen wirklich nützlichen Fund

  • Bemerkenswert fand ich die Stelle, an der Claude sagte, dies sei „eine der speichersichersten Codebasen, die ich je analysiert habe“
    Das klang aber fast wie der Witz, dass dies die erste Codebasis sei, die Claude je analysiert habe

    • Es kann nicht sein, dass eine mit RL breit trainierte Claude zum ersten Mal Code analysiert
      Genau deshalb ist er schließlich so gut darin
    • Vielleicht tut Claude heimlich etwas, von dem wir nichts wissen 😄