- Verus ist ein Tool zur Verifikation der Korrektheit von in Rust geschriebenem Code. Entwickler beschreiben in einer Spezifikation, was der Code tun soll; Verus prüft statisch, ob der ausführbare Rust-Code diese Spezifikation in allen möglichen Ausführungen erfüllt
- Statt Laufzeitprüfungen hinzuzufügen, beweist Verus mithilfe eines leistungsfähigen Solvers, dass der Code korrekt ist; derzeit wird nur ein Teil von Rust unterstützt
- In einigen Fällen kann Verus über das Standard-Typsystem von Rust hinaus auch die Korrektheit von Code statisch prüfen, der raw pointer manipuliert
- Das Projekt wird aktiv entwickelt; Funktionen können defekt sein oder fehlen, und die Dokumentation ist noch nicht vollständig. Nutzer sollten darauf vorbereitet sein, in Zulip um Hilfe zu bitten
- Ein browserbasierter Verus Playground, Installationshinweise, Tutorial und Referenz, API-Dokumentation der Standardbibliothek, ein Leitfaden zur Verifikation von Nebenläufigkeitscode sowie Beispiele und Tests stehen als Wege zum Lernen und Experimentieren bereit
Was Verus verifiziert
- Verus ist ein Tool zur Verifikation der Korrektheit von Rust-Code
- Entwickler beschreiben das Verhalten, das der Code ausführen soll, als Spezifikation
- Verus prüft statisch, ob ausführbarer Rust-Code diese Spezifikation in allen möglichen Ausführungen stets erfüllt
- Statt Laufzeitprüfungen hinzuzufügen, nutzt Verus einen Solver, um zu beweisen, dass der Code korrekt ist
- Der derzeitige Unterstützungsumfang ist eine Teilmenge von Rust; an einer Ausweitung des Umfangs wird gearbeitet
- In einigen Fällen kann Verus über das Standard-Typsystem von Rust hinaus beispielsweise die Korrektheit von Code statisch überprüfen, der raw pointer manipuliert
Entwicklungsstand und Hinweise zur Nutzung
- Verus ist ein Projekt, das aktiv entwickelt wird
- Funktionen können defekt sein oder fehlen
- Die Dokumentation ist noch nicht vollständig
- Wer Verus ausprobieren möchte, sollte bereit sein, auf Zulip um Hilfe zu bitten
- Die Verus-Community hat mehrere Forschungsarbeiten veröffentlicht, und verschiedene Projekte aus Industrie und Wissenschaft nutzen Verus
- Eine entsprechende Liste findet sich auf der Seite publications and projects
Einstieg und Entwicklungstools
- Um Verus im Browser auszuprobieren, kann der Verus Playground genutzt werden
- Für ernsthaftere Entwicklung sollten die Installationshinweise befolgt werden
- Der Einstieg ins Lernen kann über Tutorial and reference erfolgen
- Auch der automatische Formatierer verusfmt für Verus-Code wird unterstützt
Dokumentation und Lernmaterial
- Die in Arbeit befindlichen Dokumentationsressourcen umfassen unter anderem:
- Tutorial and reference: Tutorial und Referenz zu Verus
- API documentation for Verus's standard library: API-Dokumentation der Verus-Standardbibliothek
- Guide for verifying concurrent code: Leitfaden zur Verifikation von Nebenläufigkeitscode
- Contributing to Verus
- Best Practices für die Veröffentlichung von Verus-bezogenen Crates auf crates.io
- Verus License
- Verus Logos
Beispiele und Beteiligung der Community
- Beispiele für die Nutzung von Verus bieten neben der Dokumentation mehrere Einstiegspunkte
- Publications and projects: Veröffentlichungen und Projekte, die Verus nutzen
- Videos, slides, and exercises: Videos, Folien und Übungen eines eintägigen Verus-Tutorials
- Standalone examples: Eigenständige Beispiele für den Einsatz von Verus bei kleinen, konkreten Aufgaben
- Small and medium-sized examples: Beispiele, die verschiedene Verus-Funktionen zeigen
- Unit tests: Tests mit Beispielen für Verus-Syntax und -Funktionen
- Fehlerberichte und Diskussionen können auf GitHub oder in Zulip erfolgen
- Für Feature Requests und offene Gespräche werden GitHub discussions genutzt; ausführbare Bugs in bestehenden Funktionen werden als GitHub issues behandelt
- Wer Code beitragen möchte, kann die Hinweise in Contributing to Verus beachten
1 Kommentare
Hacker-News-Meinungen
Ich habe mit Verus einen formal verifizierten Kubernetes-Controller geschrieben.
Im Grunde kann man damit Liveness-Eigenschaften beweisen, etwa „irgendwann gleicht der Controller den Cluster an den angeforderten Zielzustand an“.
Wenn man jedoch berücksichtigt, dass sich der Zielzustand schnell ändern kann, sowie Asynchronität, Fehler usw., gibt es schon bei der Spezifikation dessen, was „korrekt“ bedeutet, viele Feinheiten.
Code: https://github.com/vmware-research/verifiable-controllers/, das zugehörige Paper soll auf der OSDI 2024 erscheinen.
Als kleinen Schritt in Richtung Verus kann man Rusts debug_assert für Vor- und Nachbedingungen verwenden.
Der Rust-Compiler entfernt diese standardmäßig aus Produktions-Builds.
In den Verifikationsbeispielen des Verus-Tutorials werden mit
requiresundensuresEingabebereiche und Ergebnisbedingungen angegeben; die Variante mit Laufzeitprüfungen überprüft dieselben Bedingungen während der Ausführung, etwa mitdebug_assert(-16 <= x1)oderdebug_assert(x8 == 8 * x1).Andere Rust-Tools für Beweise/Verifikation/Contracts wie Creusot verwenden eine attributbasierte Syntax, die sich im Allgemeinen schlanker und Rust-typischer anfühlt.
Es wäre schön, wenn eine solche Vorgehensweise in künftigen Verus-Releases ebenfalls möglich würde.
Sie sind hervorragend als Dokumentationswerkzeug und ergänzen Typsystem und Tests sehr gut.
"contracts"ausprobieren: https://docs.rs/contracts/latest/contracts/Ich versehe die meisten Funktionen mit Vor- und Nachbedingungen, und die JVM hat ein Flag, mit dem man sie in Produktions-Builds leicht entfernen kann.
Aus der Perspektive von jemandem ohne viel praktische Informatikerfahrung frage ich mich: Was unterscheidet im README bei „die Korrektheit des Codes verifizieren“ die Verifikation von dem, was anderswo als „Beweis“ bezeichnet wird?
Mich würden auch gute Materialien interessieren, mit denen berufstätige Programmierer ohne starken Informatik-/Mathematikhintergrund lernen können, über Code „Beweise“ zu führen.
Außerdem verstehe ich nicht wirklich, warum Zero-Knowledge-Proofs so wichtig und relevant sein sollen. Ich habe zum Beispiel von Dingen wie x.com/ZorpZK gehört, verstehe aber nicht, was daran so toll ist.
Allerdings verfolgen Verus und das in Software Foundations verwendete Coq unterschiedliche Ansätze.
Verus versucht, Eigenschaften mit einem automatischen Constraint-Solver namens SMT-Solver automatisch zu beweisen, während man in Coq deutlich mehr von Hand beweisen muss und die Automatisierung begrenzt ist.
Beides hat Vor- und Nachteile; Automatisierung ist großartig, wenn sie funktioniert, und frustrierend, wenn nicht.
Zero-Knowledge-Proofs sollte man eher als ein anderes Gebiet betrachten; viele Leute, die an formaler Verifikation/Beweisen arbeiten, befassen sich nicht mit Zero-Knowledge-Proofs. Man versteht sie besser als kryptografisches Primitive.
Zero-Knowledge-Proofs haben viel Overhead und es fehlt ihnen an einer sogenannten „Killer-App“, daher sind praktischer Nutzen, Bedeutung und Relevanz derzeit noch nicht besonders groß; konzeptionell sind sie aber interessant.
Lernmaterialien wünschte ich mir ebenfalls. Die Dafny-Dokumentation ist ziemlich gut, aber formale Software-Verifikation scheint mir noch nicht auf dem Niveau zu sein, auf dem normale Programmierer ohne Informatik-/Mathe-Promotion sie gut nutzen können.
An Beispielen wirkt es relativ einfach, aber bald stößt man auf „kann nicht bewiesen werden“, und die Antwort auf das Warum führt oft in tiefe Implementierungsdetails, die nur die Autoren zu kennen scheinen.
Man kann zum Beispiel verifizieren, dass jemand ein Passwort kennt, ohne das Passwort an den Server zu senden; dadurch wird es für bösartige Server oder Man-in-the-Middle-Angreifer schwieriger, das Passwort auszuspähen.
Auch bei der Identitätsprüfung können sie bessere Optionen bieten. Man kann nachweisen, dass man einen staatlich ausgestellten Ausweis besitzt, ohne das Dokument selbst an den Server zu übergeben, wodurch sich Fälle reduzieren lassen, in denen es „höchstens 2 Jahre/3 Jahre/6 Monate“ aufbewahrt wird und am Ende doch durchsickert.
Beweise über Code sind noch nichts, was berufstätige Programmierer normalerweise tun.
Hoare-Logik ist ein guter Einstieg und wird gelegentlich auch in Einführungskursen der Informatik gelehrt.
Coq hat eine steile Lernkurve und ist besonders schwierig, wenn man nicht mit OCaml oder ähnlichen Sprachen vertraut ist. Why3 könnte einsteigerfreundlicher sein: https://www.why3.org
Beweis und Verifikation können dasselbe bedeuten, aber Beweis klingt eher interaktiv, während Verifikation eher nach etwas klingt, das automatisiert werden kann, etwa durch Model Checking oder SMT-Lösen eines annotierten Programms.
Falls jemand ähnliche Projekte nicht kannte: Dafny ist eine „verifikationsbewusste Programmiersprache“, die nach Rust kompilieren kann: https://github.com/dafny-lang/dafny
Vor ein paar Tagen habe ich einen Einsteigerartikel zu Dafny geschrieben: https://www.linkedin.com/pulse/getting-started-dafny-your-fi...
Sieht wirklich großartig aus. Eine Anleitung oder Beispiele dazu, wie man einer bestehenden Codebasis Beweise hinzufügt, wären für viele vermutlich nützlich.
Nehmen wir zum Beispiel eine minimale GUI-App mit nur einem Textfeld, die per HTTP-Request ein zur Kompilierzeit unbekanntes und nicht vertrauenswürdiges Array abruft, es per Bubble Sort sortiert und anschließend anzeigt.
In Bubble Sort steckt ein absichtlicher Bug, etwa ein Off-by-one-Fehler, durch den das letzte Element unverändert bleibt, und die Unit-Tests erwischen diesen Bug zufällig nicht. Die Sorge, dass Tests unvollständig sind, kann eine wichtige Motivation für den Schritt zu Beweisen sein.
Dann wäre es gut, zu zeigen, wie man die Unit-Tests durch Beweise ersetzt, dabei den Bug entdeckt und behebt.
Der Beweiscode selbst muss nicht im Detail erklärt werden; der Fokus kann auf realistischen Details liegen, etwa der Grenze zwischen bewiesenem mathematischem Code und unbewiesenem Ein-/Ausgabe-Code, den Kommandozeilen für Beweis und Build sowie einem zip-Archiv, mit dem man selbst herumspielen kann.
Eigentlich würde sogar schon Lesen von der Standardeingabe und Schreiben auf die Standardausgabe reichen.
Einer der Hauptbeitragenden hat beim Zürich Rust Meetup einen hervorragenden Vortrag über Verus gehalten: https://www.youtube.com/watch?v=ZZTk-zS4ZCY
Ich fand beeindruckend, wie sauber dieser „ghost“-Code in das Programm passt, und es hat mich ein wenig an Ada erinnert.
Ich frage mich, ob Rust bereits einen Standard wie C/C++, Common Lisp oder Ada/SPARK2014 hat.
Falls nicht, wäre es im Vergleich zu den für Ada/SPARK2014 entwickelten Verifikationswerkzeugen ein bewegliches Ziel.
Auch das Erbe von Ada/SPARK2014, von Bare Metal bis hin zu hochintegren sicherheitskritischen Anwendungen, ist schwer zu ignorieren.
Meinst du das hier?
Ich frage mich, welche Beziehung es zwischen diesem und Kani gibt. Funktionieren sie unterschiedlich?
https://github.com/model-checking/kani
Automatische SMT-basierte Verifikatoren wie Verus, Dafny, F* und mein VCC erfordern Annotationen an fast jeder Funktion und Schleife, bieten dafür aber umfassendere Garantien zur Programmkorrektheit.
Werkzeuge auf Basis interaktiver Theorembeweiser wie Coq oder Lean benötigen meist mehr Anleitung durch den Nutzer, können dafür aber auch komplexere Eigenschaften garantieren.
Ich frage mich, wie Verus im Vergleich zu SPARK abschneidet.
Gehört es zur selben allgemeinen Klasse von Verifikatoren? Wie unterscheidet sich Verus, abgesehen davon, dass es ein Verifikator für Rust und nicht für Ada ist?
Es wäre schön, wenn jemand, der Verus gut kennt, die Unterschiede zwischen Verus und Lean4 bei Performance und Ausdrucksstärke erklären könnte.
Ich verstehe Verus als SMT-basiertes Verifikationswerkzeug, während Lean ein interaktiver Theorembeweiser und zugleich ebenfalls ein SMT-basiertes Werkzeug ist.
Da mein Verständnis des Bereichs formaler Verifikation aber begrenzt ist, wäre ich an der Einschätzung von jemandem interessiert, der sich mit formalen Methoden für Software gut auskennt.
Man kann zum Beispiel, wie im Coq-Buch „Software Foundations“, Aussagen über C-Code formulieren und beweisen, aber mit Lean scheint das kaum jemand zu tun, und die Werkzeuge dafür fehlen ebenfalls.
Man kann Programme in Lean4 schreiben und Beweise über diese Programme führen; einige Leute tun das in sehr kleinem Umfang.
Reine Mathematik zu formalisieren und darüber Papers zu veröffentlichen, ist derzeit die Hauptanwendung von Lean4 und Coq.
Die Art von Dingen, die Lean/Coq tatsächlich formulieren und beweisen können, ist allgemeiner, aber für reale Programme ist dieses Maß an Allgemeinheit möglicherweise nicht unbedingt nötig.