Four Ways to Forge a Bundle My Own Verifier Calls Clean: Refusal-Site Mutation Testing of an Evidence-Bundle Verifier

In der modernen digitalen Welt verlassen sich Softwaresysteme oft auf eine einfache, aber kraftvolle Idee: Vertrauen, aber Verifizieren. Wenn ein Computerprogramm behauptet, ein schwieriges Problem gelöst oder einen massiven Datensatz analysiert zu haben, erstellt es einen Bericht. Um sicherzustellen, dass dieser Bericht ehrlich ist, fungieren andere Programme als Auditoren. Diese Auditoren prüfen die Mathematik, verifizieren, ob die Datendateien manipuliert wurden, und bestätigen, dass die Zahlen in der Zusammenfassung mit den Rohdaten übereinstimmen. Wenn alles korrekt ist, gibt der Auditor ein grünes Licht, und das Ergebnis wird der Welt präsentiert. Dieser Prozess ist das Rückgrat zuverlässiger Software und ermöglicht es Fremden, das Werk anderer zu vertrauen, ohne einander kennen zu müssen. Doch damit dieses System funktioniert, muss der Auditor selbst perfekt sein. Wenn der Auditor versagt, eine Lüge zu erkennen, oder schlimmer noch, wenn er eine Lüge als wahr erklärt, ohne tatsächlich die Beweise geprüft zu haben, bricht das gesamte System zusammen. Die Gefahr besteht nicht nur darin, dass ein schlechtes Ergebnis durchrutscht, sondern dass der Auditor so fehlerhaft sein könnte, dass er einen Test besteht, ohne den Test überhaupt ausgeführt zu haben.

Ein Forscher namens Erik Hill setzte sich zum Ziel, einen solchen Auditor zu untersuchen, ein Programm, das darauf ausgelegt ist, Bündel von Beweisen für ein Offline-System zu verifizieren. Er wollte eine spezifische, beunruhigende Frage beantworten: Wie oft sagt dieses Programm „bestanden“, ohne tatsächlich etwas geprüft zu haben? Um dies herauszufinden, suchte er nicht bloß nach Fehlern; er baute ein Werkzeug, um seinen eigenen Auditor systematisch zu brechen. Er nahm jede einzelne Zeile Code in dem Programm, die dazu gedacht war, ein fehlerhaftes Bündel abzulehnen, und schaltete sie nacheinander aus. Dann beobachtete er, ob die Testsuite des Programms dies bemerken würde. Wenn die Tests immer noch bestanden, nachdem eine Ablehnungszeile entfernt worden war, bedeutete dies, dass diese Ablehnungszeile totes Gewicht war – sie hatte nie wirklich eine Funktion erfüllt. Die Ergebnisse waren erschreckend. Zu Beginn der Studie waren zwei Drittel der Ablehnungspunkte des Auditors unsichtbar für die Tests. Das Programm konnte der Großteil seiner Fähigkeit, „Nein“ zu sagen, verlieren und würde dennoch ein perfektes Ergebnis melden. Es war, als wäre ein Sicherheitsmann darauf trainiert worden, nach gestohlenen Gegenständen zu suchen, aber die Trainingsübungen hatten niemals einen gestohlenen Gegenstand beinhaltet, sodass der Wachmann nie gelernt hatte, tatsächlich danach zu suchen.

Die Studie begann mit einem Schock durch einen externen Experten. Ein unabhängiger Ingenieur reichte ein Bündel von Beweisen ein, bei dem die Schlagzeilen-Zahlen völlig falsch waren, und dennoch druckte der Auditor ein perfektes „Bestanden“. Der Betrug kostete lediglich vier Bytes zur Erstellung. Der Ingenieur hatte eine Datei durch einen winzigen, leeren Platzhalter ersetzt, und weil der Auditor versäumte zu prüfen, ob diese Datei tatsächlich vorhanden war, nahm er an, dass alles in Ordnung sei. Hill behob diese spezifische Lücke, wandte dann aber sein eigenes systematisches Werkzeug auf das reparierte Programm an. Er fand heraus, dass das Problem nicht nur ein einzelner Fehler war, sondern ein Muster. Er entdeckte vier weitere Wege, den Auditor zu täuschen, wobei er jedes Mal feststellte, dass das Programm eine Prüfung komplett übersprang. Einer dieser Tricks beinhaltete das Ändern eines einzelnen Großbuchstabens in einem Schweregrad-Label, was dazu führte, dass das Programm das Gewicht einer fehlgeschlagenen Prüfung ignorierte. Ein anderer beinhaltete das Löschen eines Schlüssels aus einer Liste, was dazu führte, dass das Programm einen Vergleich übersprang, weil das Element, das es vergleichen sollte, fehlte. In jedem Fall versagte das Programm nicht bei einer schwierigen Berechnung, sondern es versagte schlichtweg daran, die Berechnung überhaupt zu starten.

Um zu messen, wie weit verbreitet dieses Problem war, ließ Hill sein Löschwerkzeug gegen den Code des Auditors laufen. Er fand 112 Stellen, an denen das Programm „Nein“ sagen sollte. Als er diese nacheinander entfernte, konnten 7ene von ihnen gelöscht werden, ohne dass ein Test fehlschlug. Dies bedeutete, dass 75 von 112 Ablehnungspunkten effektiv unsichtbar für die Sicherheitsprüfungen des Systems waren. Das Programm hatte einen Wert von 0,330, was darauf hindeutete, dass nur etwa ein Drittel seiner Verwehrmechanismen tatsächlich getestet wurde. Die verbleibenden zwei Drittel waren „vakuöse Bestätigungen“ – Prüfungen, die Erfolg meldeten, obwohl sie die Beweise nie untersucht hatten. Dies ist kein seltener Glitch; es ist ein struktureller Fehler, bei dem das Sicherheitsnetz Löcher hat, durch die niemand je gefallen ist. Die Tests prüften, ob das Programm lief, nicht ob es tatsächlich die Daten betrachtete.

Hill testete dann einen gängigen Ansatz zur Behebung solcher Probleme: einfach die spezifischen Fehler zu beheben, die gefunden wurden, und einen Test für jeden davon hinzuzufügen. Er behob die vier Fälschungen, die er entdeckt hatte, und fügte neue Tests hinzu, um sicherzustellen, dass diese spezifischen Tricks nicht mehr funktionieren würden. Überraschenderweise verbesserte dies den allgemeinen Sicherheitswert nicht. Das Programm hatte immer noch dieselben 75 unsichtbaren Ablehnungspunkte. Die neuen Tests deckten nur die neuen Lücken ab, die er gerade gepatcht hatte, wodurch der Rest des Systems genauso blind blieb wie zuvor. Erst als er seine Strategie änderte, bewegten sich die Zahlen. Anstatt Bugs zu beheben, schrieb er einen neuen Test für jeden einzelnen der 75 unsichtbaren Ablehnungspunkte und zwang das Programm dadurch, zu beweisen, dass es jeden einzelnen Punkt tatsächlich auslösen konnte. Dieser systematische Ansatz hob den Wert von 0,330 auf 1,000 und bewies, dass jeder Ablehnungspunkt tatsächlich ausgelöst werden konnte. Die Lektion war klar: Das Beheben bekannter Bugs macht ein System nicht sicher; man muss beweisen, dass jeder einzelne Sicherheitsmechanismus tatsächlich funktionieren kann.

Die Studie enthüllte auch ein tiefer liegendes Problem bei der Erstellung dieser Systeme. Der Forscher fand heraus, dass der Auditor menschenlesbare Berichte oft anders behandelte als die Rohdatendateien, die für die Prüfung verwendet wurden. Wenn ein Bündel einen Bericht enthielt, der für einen Menschen bestimmt war, versäumte es der Auditor häufig zu verifizieren, ob der Bericht mit den zugrunde liegenden Daten übereinstimmte. Es war, als würde der Auditor die Zusammenfassung vertrauen, aber die Quittungen ignorieren. Dies geschah in mehreren verschiedenen Projekten, was auf eine verbreitete Gewohnheit unter Entwicklern hindeutete: Sie binden die Daten, die der Computer prüft, aber sie lassen die Daten, die Menschen lesen, unverifiziert. Der Forscher fand heraus, dass diese Lücke es ermöglichte, dass falsche Behauptungen durchrutschten, wobei ein Bericht sagen konnte: „Alle Defekte behoben“, während die Daten etwas anderes zeigten.

Im Laufe der gesamten Studie versagten die eigenen Werkzeuge des Forschers in einer Weise, die das Problem widerspiegelte, das er gerade untersuchte. Seine Messinstrumente meldeten manchmal Erfolg, selbst wenn sie gar nichts maßen. In einem Fall meldete ein Werkzeug, das darauf ausgelegt war, Fehler zu erkennen, einen perfekten Wert, weil die Basis-Testsuite bereits fehlgeschlagen war, was dazu führte, dass das Werkzeug den Fehler als Erfolg interpretierte. Dies geschah siebenmal während der Forschung, einmal sogar, als das Werkzeug einen perfekten Wert angab, während das System defekt war. Diese Fehler wurden nicht verborgen; sie wurden im Paper dokumentiert, um zu zeigen, dass die Werkzeuge, die zur Softwareverifizierung eingesetzt werden, denselben „Empty Pass“-Fehlern unterliegen wie die Software, die sie eigentlich prüfen sollen.

Die abschließende Schlussfolgerung der Arbeit ist ein Aufruf zu einer anderen Art des Testens. Der Forscher argumentiert, dass wir uns nicht auf eine Liste bekannter Bugs verlassen können, um ein System sicher zu halten. Wenn ein System ein Sicherheitsgate besitzt, das noch nie beim Scheitern beobachtet wurde, wurde es noch nie beim Funktionieren beobachtet. Der einzige Weg, um sicher zu sein, besteht darin, jedes einzelne Gate systematisch zu testen, um sicherzustellen, dass es tatsächlich auslösen kann. Die Studie zeigte, dass ein System auf dem Papier perfekt erscheinen kann, während es in der Praxis fundamental defekt ist. Indem er den Auditor zwang, zu beweisen, dass er schlechte Daten auf jede erdenkliche Weise ablehnen kann, verwandelte der Forscher ein System, das blind für seine eigenen Fehler war, in eines, das vollständig verifiziert ist. Das Werk steht als Mahnung, dass im Bereich des digitalen Vertrauens der gefährlichste Fehler nicht eine fehlgeschlagene Prüfung ist, sondern eine Prüfung, die gar nicht stattgefunden hat.