Stellen Sie sich vor, Sie bauen eine riesige, komplizierte Burg aus LEGO-Steinen. Sie haben tausende Teile und wollen sicherstellen, dass der Turm nicht zusammenbricht, egal wie Sie sie stapeln, und dass die Geheimtür Sie nicht versehentlich einschließt. In der Welt der Informatik ist diese „Burg“ eine komplexe Software, die unsere Banken, Krankenhäuser und das Internet steuert. Die „Blaupausen“, die uns sagen, ob die Burg sicher ist, nennt man formale Spezifikationen. Betrachten Sie dies als ein superpräzises, mathematisches Regelbuch, das genau beschreibt, wie sich die Software verhalten soll. Jahrzehntelang war das Schreiben dieser Regelbücher so, als würde man versuchen, einen Roman in einer Sprache zu schreiben, die nur wenige Genies beherrschen; es dauerte Monate harter Arbeit von Experten, um es richtig zu machen, und wenn man auch nur einen winzigen Fehler machte, war das gesamte Werk unbrauchbar.

Kürzlich ist ein neuer Typ von „Roboter-Schreiber“ namens KI-Agent aufgetaucht. Dies sind Computerprogramme, die von Large Language Models (derselben Technologie hinter Chatbots) angetrieben werden und die in der Lage sind, Code zu lesen und neuen Code zu schreiben. Die Menschen hofften, dass diese Roboter die Regelbücher für uns schreiben könnten, um Zeit und Mühe zu sparen. Aber es gab einen Haken: Diese Roboter neigen zu „Halluzinationen“ (Dinge erfinden) und „Reward Hacking“ (schummeln, um gut auszusehen, ohne tatsächlich richtig zu sein). Sie könnten ein Regelbuch schreiben, das auf dem Papier perfekt aussieht, aber eine Burg beschreibt, die nicht mit den tatsächlichen LEGO-Steinen übereinstimmt. Die große Frage war: Können wir einem Roboter vertrauen, das Sicherheits Handbuch für ein komplexes System zu schreiben, ohne dass ein menschlicher Experte ihm die Hand hält?

Hier kommt Specula ins Spiel, ein neues System, das wie ein superintelligentes, selbstkorrigierendes Roboter-Team fungiert. Anstatt die KI nur zu fragen, „schreibe ein Regelbuch“, behandelt Specula die KI wie einen neugierigen Lehrling, der lernt, indem er tut, scheitert und es erneut versucht. Es nutzt eine geschickte Schleife, in der der Roboter ein Regelbuch schreibt, es gegen den tatsächlichen Code prüft, Fehler findet und dann sein eigenes Verständnis korrigiert. Die Forscher fanden heraus, dass dieses System autonom hochwertige Regelbücher für 48 verschiedene komplexe Softwareprojekte generieren kann. Es fand nicht nur offensichtliche Fehler, sondern deckte 249 Bugs auf, von denen 89 an Entwickler gemeldet wurden, 68 davon bestätigt wurden und 24 bereits behoben wurden. Am wichtigsten ist: Das System fand diese Bugs, ohne dass menschliche Experten die ursprünglichen Regelbücher schreiben mussten, was beweist, dass wir Sicherheitsprüfungen für Software mithilfe von KI skalieren können – vorausgesetzt, wir geben der KI die richtigen Werkzeuge, um aus ihren eigenen Fehlern zu lernen.

Die Geschichte von Specula: Ein Roboter-Detektiv, der lernt zu denken

Stellen Sie sich vor, Sie sind ein Detektiv, der versucht, ein Verbrechen in einer Stadt zu lösen, die niemals schläft. Die Stadt ist ein Stück komplexer Software, und das Rätsel lautet: „Wo ist die versteckte Falle, die dazu führen wird, dass die Stadt zusammenbricht?“ In der Vergangenheit hätten Sie ein Team von menschlichen Experten benötigt, um eine Karte der Stadt zu zeichnen (ein formales Modell) und die Regeln aufzuschreiben, wie die Stadt funktioniert (Invarianten). Das dauerte Monate. Stellen Sie sich nun vor, Sie haben einen Roboter-Detektiv. Sie denken vielleicht: „Großartig! Sagen Sie dem Roboter einfach, er soll die Karte zeichnen.“ Aber hier liegt das Problem: Wenn Sie einem Roboter einfach sagen, er soll eine Karte zeichnen, zeichnet er vielleicht eine wunderschöne Stadt, die wie ein Cartoon aussieht, aber nicht zu den echten Straßen passt. Er könnte eine Brücke erfinden, die gar nicht existiert, oder ein Verkehrsschild vergessen, das einen Crash verursacht. Das ist das, was passiert, wenn eine KI versucht, formale Spezifikationen eigenständig zu schreiben – sie erfasst zwar die „Vibe“, aber die Details sind falsch.

Specula ist die Lösung für dieses Problem. Es ist nicht nur ein Roboter, der Karten zeichnet; es ist ein Roboter, der ein strenges, selbstkorrigierendes Trainingsprogramm durchläuft. Stellen Sie es sich wie ein Videospiel vor, in dem der Roboter die Rolle eines Architekten spielt, aber jedes Mal, wenn er eine Wand baut, prüft ein „Schiedsrichter“, ob diese Wand in der realen Welt auch tatsächlich existiert. Wenn die Wand eine Fälschung ist, muss der Roboter sie wieder abreißen und es erneut versuchen.

Wie das Roboter-Team arbeitet

Das Specula-System ist wie ein Team spezialisierter Roboter, die in einer Schleife zusammenarbeiten:

1. Der neugierige Leser: Zuerst liest der Roboter den Softwarecode, die Dokumentation und sogar die Fehlerberichte (als würde er die Geschichtsbücher der Stadt lesen). Er versucht, die Regeln der Stadt zu erraten. Zum Beispiel könnte er raten: „Wenn eine Nachricht gesendet wird, muss sie schließlich auch empfangen werden.“ Dies nennt man ein Invariant.
2. Der Architekt: Als Nächstes versucht der Roboter, ein vereinfachtes Modell der Stadt unter Verwendung einer speziellen Sprache namens TLA+ zu bauen. Dieses Modell ist wie eine Blaupause, die winzige Details (wie die Farbe der Steine) ignoriert, aber die wichtigen Teile (wie den Verkehrsfluss) beibehält.
3. Der Realitätscheck (Trace Validation): Dies ist der kritischste Schritt. Der Roboter nimmt die Blaupause und vergleicht sie mit dem tatsächlichen Code. Er führt den Code aus und zeichnet einen „Trace“ auf (ein Video dessen, was der Code tatsächlich tut). Dann prüft er: „Erlaubt meine Blaupause dieses Video?“ Wenn die Blaupause sagt: „Ja, das ist möglich“, das Video aber etwas Unmögliches zeigt, ist die Blaupause falsch.
4. Die Selbstkorrektur-Schleife: Wenn die Blaupause falsch ist, gibt der Roboter nicht einfach auf. Er erhält einen Hinweis: „Du hast diesen Teil übersehen!“ oder „Du hast eine Regel erfunden, die nicht wahr ist.“ Der Roboter geht dann zurück, liest den Code erneut und korrigiert seine Blaupause. Er erkennt vielleicht: „Oh, ich dachte, die Ampel sei grün, aber der Code sagt, sie ist rot.“ Er macht dies so lange, bis die Blaupause perfekt mit der Realität des Codes übereinstimmt.
5. Der Bug-Jäger: Soblich die Blaupause perfekt ist, nutzt der Roboter einen „Model Checker“ (einen superschnellen Simulator), um jeden möglichen Szenario in der Blaupause durchzuspielen. Er sucht nach jeder Situation, in der die Regeln gebrochen werden. Wenn er einen Bruch findet, sagt er nicht einfach nur „Fehler“. Er geht zurück zum echten Code und versucht, den exakten Moment zu rekonstruieren, in dem der Absturz passierte, um den abstrakten Fehler in einen realen, reproduzierbaren Testfall zu verwandeln, den Entwickler sehen und beheben können.

Das große Experiment

Die Forscher testeten Specula an 48 verschiedenen Open-Source-Softwareprojekten. Dies waren keine einfachen Programme, sondern komplexe Systeme wie MongoDB (eine Datenbank), GCC libgomp (ein Werkzeug für paralleles Computing) und verschiedene Raft-Implementierungen (Protokolle, um Computer synchron zu halten). Diese Systeme sind in Sprachen wie C++, Go, Rust und Java geschrieben.

Die Ergebnisse waren beeindruckend. Specula fand insgesamt 249 Bugs.

• 207 dieser Bugs waren völlig neue Fehler, von denen niemand wusste.
• 42 waren bekannte Bugs, die noch nicht behoben worden waren.
• Das Team hat 89 dieser Bugs an die Entwickler gemeldet.
• Bisher wurden 68 als echte Bugs bestätigt und 24 bereits behoben.

Eines der coolsten Merkmale von Specula ist, dass es nicht nur einfache Fehler fand. Es fand „tiefe“ Bugs – Probleme, die nur auftreten, wenn Dinge auf sehr spezifische, seltene Weise schieflaufen. Zum Beispiel fand Specula in einer Bibliothek namens libgomp einen Deadlock (eine Situation, in der das Programm ewig einfriert), der mindestens fünf Jahre lang im Code verborgen war. Der Bug trat nur auf, wenn ein bestimmter Thread im exakt falschen Moment aufwachte. Ein menschlicher Tester hätte dies fast nie entdeckt, da es vergleichbar ist mit dem Versuch, ein ganz bestimmtes Sandkorn in einem Sandsturm zu fangen. Aber der Model Checker von Specula betrachtete jeden möglichen Weg, wie der Sand fallen konnte, und fand genau den, der den Absturz verursachte.

Ein weiteres Beispiel stammt aus SONiC, einem Netzwerk-Betriebssystem, das in Rechenzentren eingesetzt wird. Specula fand einen Bug, bei dem ein System aufhörte, zwei Switches zu koordinieren, aufgrund eines winzigen Fehlers in der Art und Weise, wie sie ihren Status aktualisierten. Dieser Bug war so subtil, dass die eigenen Tests des Projekts ihn nie erfassten.

Warum das wichtig ist (und warum es keine Magie ist)

Sie fragen sich vielleicht: „Warum haben sie nicht einfach die KI genutzt, um den Code direkt zu schreiben?“ Das Paper argumentiert, dass es eine Falle ist, eine KI einfach nur eine formale Spezifikation schreiben zu lassen. Wenn man eine KI nur bittet, „ein Regelbuch zu schreiben“, könnte sie schummeln. Sie könnte ein Regelbuch schreiben, das so vage oder so einfach ist, dass es alle Tests besteht, aber das reale System eigentlich gar nicht beschreibt. Dies nennt man Reward Hacking.

Specula löst dies, indem es die KI zwingt, ihre Arbeit zu beweisen. Es nutzt eine „selbstentwickelnde Schleife“. Wenn die KI einen Fehler macht, fängt das System sie ab und zwingt sie zu lernen. Die Forscher fanden heraus, dass diese Schleife essenziell war. In ihren Tests musste das System die Modelle 60,5 % der Zeit reparieren, die Code-Instrumentierung 22,2 % der Zeit anpassen und die Regeln (Invarianten) 17,3 % der Zeit überarbeiten. Oh}$, wäre die KI ohne diese Schleife zu fehlerhaft gewesen, um nützlich zu sein.

Das Paper zeigt auch, dass die „Qualität“ der KI entscheidend ist. Sie testeten Specula mit verschiedenen Versionen der KI (Claude Opus, Sonnet und Haiku). Die stärkste Version (Opus) fand 62 Bugs. Eine etwas schwächere Version (Sonnet) fand nur 10. Die schwächste Version (Haiku) fand gar keine. Dies zeigt uns, dass das System (Specula) zwar mächtig ist, aber dennoch ein intelligentes KI-Gehirn benötigt, um gut zu funktionieren. Es ist wie ein großartiges Auto (Specula) zu haben, aber einen geschickten Fahrer (die KI) zu benötigen, um ans Ziel zu kommen.

Die Kosten der Sicherheit

Ist das teuer? Die Forscher berechneten, dass der Betrieb von Specula auf einem System zwischen 1,43 und 9,86 Stunden dauerte und zwischen 19 $ und 168 $ an Rechenleistung (Token-Kosten) kostete. Während dies im Vergleich zu einem kostenlosen Tool viel Geld klingen mag, weist das Paper darauf hin, dass ein menschlicher Experte Monate bräuchte, um ein ähnliches Regelbuch von Hand zu schreiben. Im großen Ganzen betrachtet ist es also eigentlich ein Schnäppchen.

Das Paper ist vorsichtig damit zu sagen, dass dies kein „Zauberstab“ ist, der alles löst. Das System ist immer noch darauf angewiesen, dass die KI den Code liest, und wenn die KI einen großen Teil des Codes übersieht, könnte das Modell unvollständig sein. Jedoch bedeutet die „selbstentwickelnde“ Natur von Specula, dass das System selbst dann, wenn die KI einen Fehler macht, darauf ausgelegt ist, ihn zu erkennen und zu korrigieren, was es viel zuverlässiger macht, als eine KI einfach nur die Regeln „raten“ zu lassen.

Am Ende zeigt Specula uns eine Zukunft, in der wir keine Experten in formaler Mathematik sein müssen, um unsere Software sicher zu halten. Wir können KI nutzen, um die schwere Arbeit zu erledigen, solange wir ein System bauen, das die Arbeit der KI überprüft, ihre Fehler korrigiert und sie niemals durch Schummeln durchkommt. Es ist ein Schritt in Richtung einer Welt, in der unsere digitalen Burgen mit Blaupausen gebaut werden, die nicht nur schön, sondern auch absolut präzise sind.