Microsoft nutzt KI-Agenten, um mathematisch zu beweisen, dass sein Verschlüsselungscode keine Fehler hat

Wichtigste Punkte

• Microsofts SymCrypt-Bibliothek, die Kryptografie-Engine von Windows und Azure, wird seit Mitte 2024 formal verifiziert, wobei eine Toolchain aus Rust, Lean und Aeneas verwendet wird.
• Die ersten verifizierten Algorithmen sind SHA-3, ein Standard zum Erstellen digitaler Fingerabdrücke von Daten, und ML-KEM, ein Post-Quanten-Verschlüsselungsverfahren, das gegen Angriffe zukünftiger Quantencomputer schützen soll.
• KI-Agenten, Software, die mehrstufige Aufgaben selbstständig ausführen kann, schreiben mathematische Beweisschritte, die dann von menschlichen Ingenieuren überprüft und unabhängig validiert werden.
• Microsoft hat den verifizierten Code, die Spezifikationen und die Beweise in einem öffentlichen Branch von SymCrypt veröffentlicht, um die Arbeit für externe Überprüfungen verfügbar zu machen.
• Zukünftige Algorithmen, die gleich behandelt werden sollen, umfassen AES-GCM, FrodoKEM und ML-DSA, die heute bereits Daten in Windows und Linux schützen.

Kryptografischer Code, die Software, die Daten in jeder App, jedem Browser und jedem Betriebssystem verschlüsselt und schützt, ist notorisch unvergeblich. Eine übersehene Bereichsprüfung – ein Fehler bei der Überprüfung, dass eine Zahl in einem sicheren Bereich bleibt – kann Sicherheit durchbrechen, die oberflächlich solide aussieht. Tests fangen viele Fehler. Sie fangen aber nicht alle.

Microsoft Research verfolgt einen anderen Ansatz: den Code mathematisch zu beweisen, bevor er ausgeliefert wird.

Das Projekt konzentriert sich auf SymCrypt, Microsofts Open-Source-Kryptografie-Bibliothek, die in Windows und Azure Linux läuft. Ingenieure schreiben jetzt neue kryptografische Algorithmen in Rust, einer Programmiersprache, die ganze Kategorien von Speichersicherheitsfehlern von Grund auf ausschließt. Sie führen diese Rust-Programme dann durch ein Tool namens Aeneas, das den Code in eine Form übersetzt, die ein Beweisassistent namens Lean analysieren kann.

Lean ist kein Chatbot. Es ist ein formales Beweisframework, Software, die mathematische Argumente genauso überprüft wie ein Taschenrechner Arithmetik überprüft – nur dass es Beweise überprüft, und es macht niemals arithmetische Fehler.

Das Ziel ist ein Theorem: Für jeden gültigen Input gibt diese Implementierung genau das Ergebnis zurück, das der veröffentlichte Standard verlangt. Nicht normalerweise. Immer.

Die erste öffentliche Veröffentlichung umfasst SHA-3, einen Standard-Algorithmus zum Erstellen eines eindeutigen digitalen Fingerabdrucks jedes Datenstücks, und ML-KEM, ein Post-Quanten-Schlüsselaustauschverfahren. Post-Quanten-Kryptografie bedeutet Algorithmen, die auch gegen Quantencomputer sicher bleiben – Maschinen, die viele heutige Verschlüsselungsmethoden knacken könnten.

Wie passt KI in einen mathematischen Beweis?

Formale Beweise zu schreiben ist zeitaufwändig. Hier kommen KI-Agenten ins Spiel.

Agenten kümmern sich um die wiederholten Zwischenschritte und formulieren Beweisfragmente, die Zwischenergebnisse verbinden. Menschliche Ingenieure konzentrieren sich auf die Teile, die echtes Urteilsvermögen erfordern: zu überprüfen, dass die formale Spezifikation tatsächlich dem veröffentlichten Standard entspricht, und die übergeordneten Eigenschaften zu überprüfen, die der Code erfüllen muss. Die Beweisüberprüfung selbst ist vollständig automatisiert und deterministisch – die Maschine akzeptiert den Beweis oder lehnt ihn ab. Es gibt keinen Spielraum für den Agenten zu bluffieren.

Microsoft beschreibt dies als saubere Aufteilung: Agenten schreiben, Menschen überprüfen, der Beweisüberprüfer entscheidet.

Für Nutzer von Windows, Azure oder einem Service, der auf Microsofts Sicherheitsstack angewiesen ist, ist die praktische Bedeutung unkompliziert. Die Verschlüsselung, die deine Dateien, deine Cloud-Daten und deine Anmeldedaten schützt, wird einem höheren Standard unterworfen als das Testen allein gewährleisten kann. Wenn die Beweise bestehen, tut der Code genau das, was der Standard verlangt.

Der Open-Source-Branch ermöglicht es externen Forschern, sowohl den Rust-Code als auch die Beweise nebeneinander zu inspizieren, sodass die Ansprüche nicht nur Microsofts Wort sind.

Zum Beobachten: Ankündigungen von formal verifizierten Builds, die stabile Windows-Versionen erreichen, und ob andere Kryptografie-Bibliotheken ähnliche KI-gestützte Beweise-Workflows übernehmen. Das würde eine echte Verschiebung in der Denkweise der Industrie über Softwarekorrektheit darstellen.