Microsoft: Formale Verifikation von Rust-Kryptografie in SymCrypt mit KI-Agenten und Lean

Zwei Garantieschichten statt einer

Formale Verifikation ist ein mathematischer Beweis, dass sich Code genau entsprechend seiner Spezifikation verhält — nicht nur für getestete Fälle, sondern für jeden möglichen Eingabewert. Microsoft hat in SymCrypt, seine grundlegende Kryptografiebibliothek, die Windows, Azure und andere Produkte unterstützt, einen doppelten Schutz eingebaut: Die Rust-Sprache eliminiert eine ganze Klasse von Fehlern im Speichermanagement (Memory-Safety-Bugs), während der Lean-Beweisassistent die funktionale Korrektheit bestätigt — dass der Algorithmus genau so arbeitet, wie es der Standard verlangt.

Lean ist ein Werkzeug, das mathematische Beweise durch seinen eigenen vertrauenswürdigen Kernel verifiziert. Im Gegensatz zu Unit-Tests, die ausgewählte Szenarien abdecken, deckt ein Lean-Beweis absolut alle möglichen Eingaben ab. Die Kombination dieser zwei Schichten macht verifizierten Code deutlich robuster als der konventionelle Ansatz.

Was wurde bereits verifiziert?

Microsoft hat verifizierten Code für SHA-3, einen weit verbreiteten Hash-Algorithmus, und für ML-KEM veröffentlicht — einen Post-Quanten-Schlüsselaustausch-Algorithmus, den NIST 2024 standardisiert hat. ML-KEM ist besonders wichtig, weil er so konzipiert ist, Angriffen von Quantencomputern standzuhalten, die RSA und ECDH brechen könnten, die heute den Großteil des Internetverkehrs schützen.

Auf dem Plan stehen AES-GCM (symmetrische Verschlüsselung), FrodoKEM und ML-DSA — zwei weitere Post-Quanten-Algorithmen. Gemeinsamer Nenner all dieser Algorithmen ist ihre Komplexität und die hohen Kosten von Fehlern: Ein Implementierungsfehler in der Kryptografie verursacht typischerweise keinen Programmabsturz, sondern eine stille Schwachstelle, die ausgenutzt werden kann.

KI-Agenten beschleunigen das Schreiben von Beweisen

Das Schreiben von Lean-Beweisen für Kryptografiecode ist langsam und anspruchsvoll. Microsoft setzt KI-Agenten ein, um diesen Prozess zu beschleunigen: Die Agenten schlagen Beweise vor, die dann unabhängig durch Leans vertrauenswürdigen Kernel verifiziert werden. Der entscheidende Unterschied zur gewöhnlichen Codegenerierung besteht darin, dass die KI-Ausgabe eine mathematische Prüfung bestehen muss — es reicht nicht, korrekt auszusehen. Fehler von KI-Agenten können also nicht unbemerkt bleiben.

Die Integration in SymCrypt macht diesen Ansatz heute praktisch relevant und nicht nur zum akademischen Experiment. Die Toolchain, die Microsoft verwendet — Aeneas — übersetzt Rust-Code in eine Form, die Lean analysieren kann, und überbrückt damit die Lücke zwischen Produktionscode und formalen Methoden.