Microsoft Research stellt PDD Kit zur Verifizierung von Web-Apps aus Agentenhand vor
Microsoft Research hat PDD Kit vorgestellt, ein Toolkit zur formalen Verifizierung von Code, den Coding-Agenten schreiben. Es wandelt die Absicht eines Entwicklers in eine formale Spezifikation um, beweist nach Möglichkeit für jede Eingabe, dass der Code diese Spezifikation erfüllt, und nutzt für die übrigen Bereiche Tests.
- PDD Kit wandelt die Absicht von Entwicklern in formale Spezifikationen und Tests um.
- Verus beweist für jede vom Beweis abgedeckte Eingabe, dass spezifizierter Rust-Code korrekt ist.
- Tests decken Schnittstellen und andere Bereiche ab, die formale Beweise nicht erreichen können.
- Microsoft Research demonstrierte das Toolkit an der Rust-basierten Pet-Store-App.
- Die Login-Verifizierung deckte laut Microsoft Research bestehende Fehler auf.
Ein Vertrag zwischen Entwicklern und Coding-Agenten
Microsoft Research zufolge können Coding-Agenten inzwischen vollständige Funktionen mit Zehntausenden oder Hunderttausenden Codezeilen erstellen. Eine lückenlose Prüfung Zeile für Zeile lässt sich dadurch nur schwer skalieren. Entwickler verlassen sich häufig auf einen Plan in natürlicher Sprache und Tests. Ein Agent kann jedoch vom Plan abweichen und Tests schreiben, die seine eigene Implementierung statt des vom Entwickler gewünschten Verhaltens überprüfen.
PDD Kit soll diese Lücke mit dem Ansatz schließen, den Microsoft Research Proof-Driven Development oder PDD nennt. Das Toolkit arbeitet mit Entwicklern zusammen, um ihre Absicht zu präzisieren, die formalisierbaren Teile in Spezifikationen in Verus zu überführen und Beweise zu erzeugen, dass der Code diese Spezifikationen erfüllt. Anforderungen, die sich nicht formalisieren lassen, werden in informelle Spezifikationen umgewandelt und durch Tests abgedeckt.
„Eine Prüfung fragt: ‚Sieht das richtig aus?‘ Ein Beweis beantwortet: ‚Ist das richtig?‘“, schreibt Microsoft Research in der Ankündigung. Anders als ein Test, der das Verhalten für die von ihm geprüften Eingaben kontrolliert, kann ein mathematischer Beweis feststellen, dass der Code für jede von der Spezifikation abgedeckte Eingabe deren Vorgaben erfüllt.
Wie PDD Kit Beweise und Tests kombiniert
PDD Kit läuft als Partner innerhalb von Chopin, der Echtzeit-Planungsumgebung mit Mehrbenutzer-Unterstützung von GitHub Next. Der Ablauf beginnt damit, dass Teammitglieder die Absicht in Alltagssprache prüfen. Das Toolkit stellt Fragen, die auch ein sorgfältiger Prüfer stellen könnte, erklärt relevanten Code und hält die Antworten in einem Absichtsdokument fest. Dieses verbindet die Anfrage des Nutzers mit formalen Spezifikationen und Tests.
Für die formale Verifizierung verwendet PDD Kit derzeit Verus, eine Beweissprache für Rust, die von Microsoft Research sowie akademischen und Forschungseinrichtungen mitentwickelt wurde. Die empirische Verifizierung deckt Bereiche ab, die Beweise nicht erreichen können, etwa eine Kryptografiebibliothek eines Drittanbieters oder eine Benutzeroberfläche. Dafür können Unit- und End-to-End-Tests, Terminal-Automatisierung, Browser-Agenten und Computer-Use-Agenten zum Einsatz kommen.
Microsoft Research unterscheidet im Toolkit zwischen Nachweis und Beweis. Ein bestandener Test zeigt, dass der Code für die getesteten Eingaben funktioniert hat, während die formale Verifizierung ein mathematischer Beweis ist, der von einem Verifizierer geprüft wird. PDD Kit macht außerdem die Trusted Computing Base explizit. Dabei handelt es sich um den Code, dessen Verhalten ein Beweis wie beschrieben voraussetzt. Nutzer werden gebeten, jeden Bestandteil abzusegnen.
Pet-Store-Demonstration konzentriert sich auf Login-Sicherheit
Microsoft Research testete PDD Kit am Pet Store, einem vollständig in Rust geschriebenen Full-Stack-Shop. Die Anwendung verwendet im Backend Axum und SQLite, um Lagerbestand, Aktionen, Bestellungen und den Checkout zu verwalten. Der Shop ist eine zu WebAssembly kompilierte Leptos-Anwendung. Die komplette App umfasst etwa 5.000 Rust-Zeilen.
Die Demonstration konzentrierte sich auf die formale Verifizierung der Login-Logik in backend/src/handlers/auth.rs. Der Entwickler gab zwei Anforderungen vor: Ein Nutzer soll nur mit dem richtigen Passwort ein Token erhalten, und nur Administratorkonten sollen Admin-Token bekommen. Bevor PDD Kit den Code änderte, stellte es zunächst Fragen zur Anfrage, unter anderem dazu, ob die Passwortanforderung in beide Richtungen gelten sollte. Diese Unterscheidung schließt sowohl aus, dass ein falsches Passwort ein Token erhält, als auch, dass ein Login jeden Nutzer abweist.
Microsoft Research zufolge härtete Verus den Login-Code ab und deckte bestehende Fehler auf. Zudem bewies das System, dass es im Hinblick auf die Spezifikation keine Login-Fehler gibt. Der Entwickler prüfte die Absicht, ohne den generierten Code Zeile für Zeile zu lesen. Das Forschungsteam empfiehlt, mit den sensibelsten Bereichen einer Anwendung zu beginnen, etwa dem Login, bei dem ein Fehler ein Kundenkonto oder administrative Kontrollen offenlegen könnte, und die Anwendung anschließend schrittweise zu verifizieren.
Microsoft Research: Formally verifying agent-written full-stack web apps with PDD Kit
