Rust-Verifikationstechnologie für Low-Level-Systemcode

Verus-Tool zur Verifikation der Korrektheit von Rust-Code

• Verus ist ein Tool zur Verifikation der Korrektheit von in Rust geschriebenem Code
• Entwickler schreiben Spezifikationen, die der Code erfüllen muss, und Verus prüft statisch, ob ausführbarer Rust-Code in allen möglichen Ausführungen immer die Spezifikation erfüllt
• Statt Laufzeitprüfungen hinzuzufügen, stützt sich Verus auf einen starken Solver, um zu beweisen, dass der Code korrekt ist
• Verus unterstützt derzeit eine Teilmenge von Rust (derzeit in Erweiterung), und in manchen Fällen können Entwickler die Korrektheit von Code über das Standard-Rust-Typsystem hinaus statisch prüfen (z. B. bei Rohzeiger-Manipulationen)

Zustand von Verus

• Verus befindet sich in aktiver Entwicklung
• Funktionen können kaputtgehen oder fehlen, und die Dokumentation ist noch unvollständig
• Wer Verus ausprobieren möchte, sollte damit rechnen, in Zulip um Hilfe zu bitten

Verus ausprobieren

• Um Verus im Browser auszuprobieren, besuchen Sie den Verus Playground
• Für komplexere Entwicklung sollten Sie die Installationsanweisungen befolgen und mit Tutorials sowie Referenz beginnen und die folgenden Dokumente prüfen

Verus-Dokumentation

• Tutorials und Referenz
• API-Dokumentation der Verus-Standardbibliothek
• Leitfaden zur Verifikation von nebenläufigem Code
• Projektziele
• Beitrag zu Verus leisten
• Lizenz

Kontaktaufnahme, Problem melden und Diskussionen starten

• Melden Sie auf GitHub Probleme oder starten Sie Diskussionen. Für Echtzeit-Diskussionen und bei Bedarf an Unterstützung treten Sie Zulip bei
• Für reproduzierbare Probleme in bestehenden Funktionen verwenden Sie GitHub Issues; für offenere Diskussionen zu Feature-Anfragen und geplanten Features verwenden Sie GitHub Discussions
• Beiträge sind willkommen: Wenn Sie Code beitragen möchten, lesen Sie die Tipps unter „Contributing to Verus“

GN⁺-Meinung

• Rust ist allgemein als Sprache für Systemprogrammierung bekannt, die Sicherheit und Leistung gewährleistet; Verus scheint ein Projekt zu sein, das diese Vorteile von Rust noch weiter verstärken kann. Besonders die Verifikation von Nebenläufigkeitsprogrammierung wirkt sehr interessant

• Es ist jedoch noch in einem frühen Entwicklungsstadium und die unterstützte Rust-Syntax scheint begrenzt, sodass für den produktiven Einsatz offenbar noch etwas Entwicklung nötig ist. Da die Sicherstellung der Codesicherheit durch statische Analyse im Voraus wichtig ist, erscheint das Entwicklungspotenzial jedoch hoch

• Auch wenn in dieser frühen Phase noch Verbesserungsbedarf bei der Dokumentation, bei der Unterstützung der Syntax und ähnlichem besteht, könnte es langfristig zu einem wichtigen Projekt im Rust-Ökosystem werden. Besonders in Bereichen wie Systemprogrammierung oder Blockchain, in denen hohe Vertrauenswürdigkeit entscheidend ist, wird ein hoher Nutzen erwartet

[GN⁺]

Hacker News Kommentar

• Ein formal verifizierter Kubernetes-Controller wurde mit Verus erstellt.
  • Man kann beweisen, dass der Controller die Liveness-Eigenschaft besitzt, also dass er den Cluster letztlich in den angeforderten gewünschten Zustand bringt.
  • Bei der Spezifikation der Korrektheit gibt es zahlreiche Nuancen und Feinheiten (schnelle Änderungen der Anforderungen an den gewünschten Zustand, Asynchronität, Ausfälle usw.).
  • Der Code ist auf GitHub verfügbar und mit einem in OSDI 2024 geplanten Paper verknüpft.
• Als kleiner Zwischenschritt zu Verus kann man mit Rusts debug_assert Vorbedingungen und Nachbedingungen hinzufügen.
  • Der Rust-Compiler entfernt diese standardmäßig in Produktions-Builds.
  • Im Verus-Tutorial gibt es Beispiele sowie Beispiele für Laufzeitprüfungen mit debug_assert.
• Anfängerfrage zum Unterschied zwischen „Code-Korrektheitsprüfung“ und „Code-Korrektheitsbeweis“.
  • Gibt es gute Lernmaterialien zu Code-0Beweisen für praktische Entwickler mit begrenztem CS-/Mathe-Hintergrund?
  • Warum sind „Zero-Knowledge“-Beweise so wichtig und warum sind sie so relevant?
• Für Rust gibt es noch keinen Standard wie bei C/C++, Common Lisp und Ada/SPARK2014.
  • Im Vergleich zu Verifikationstools, die für Ada/SPARK2014 entwickelt wurden, ist das ein bewegliches Ziel.
• Dafny ist eine verifikationsbewusste Programmiersprache, die nach Rust kompilieren kann (GitHub-Link).
• Einer der Hauptmitwirkenden hat auf dem Rust Meetup in Zürich einen ausgezeichneten Vortrag zu Verus gehalten (YouTube-Link).
  • Es war beeindruckend, wie sauber der „ghost“-Code in ein Programm passt (erinnert etwas an Ada).
• Vergleich zwischen Verus und SPARK.
  • Sind das Verifizierer derselben allgemeinen Klasse? Welche Unterschiede gibt es außer der Tatsache, dass Verus ein Verifizierer für Rust und nicht für Ada ist?
• Kann jemand, der sich gut mit Verus auskennt, Verus mit Lean4 hinsichtlich Leistung und Ausdruckskraft vergleichen?
  • Ich verstehe, dass Verus ein SMT-basiertes Verifikationswerkzeug ist und Lean ein interaktiver Beweiser sowie SMT-basiertes Werkzeug.
  • Da mein Verständnis formaler Verifikation jedoch begrenzt ist, wäre es sinnvoll, die Sichtweise einer Person zu hören, die sich mit formalen Methoden für Software auskennt.
• Besteht eine Beziehung zwischen Verus und Kani, oder arbeiten sie auf unterschiedliche Weise? (Kani GitHub-Link)
• Gibt es einen Weg, Verus so zu implementieren, dass der resultierende Code weiterhin gültiger Rust-Code bleibt, der mit Vanilla-Rust-Tools kompiliert werden kann?