Technologie de vérification de Rust appliquée au code système bas niveau

Outil Verus pour vérifier la correction du code Rust

• Verus est un outil destiné à vérifier la correction du code écrit en Rust.
• Les développeurs définissent les spécifications que le code doit respecter, et Verus vérifie statiquement que le code Rust exécutable satisfait toujours ces spécifications pour toutes les exécutions possibles.
• Plutôt que d’ajouter des vérifications au runtime, Verus s’appuie sur des solveurs puissants pour prouver que le code est correct.
• Verus prend actuellement en charge un sous-ensemble de Rust (en cours d’extension), et permet parfois aux développeurs de vérifier statiquement la correction du code au-delà du système de types standard de Rust (par exemple, la manipulation de pointeurs bruts).

État actuel de Verus

• Verus est en cours de développement actif.
• Certaines fonctionnalités peuvent être cassées ou inexistantes, et la documentation reste encore incomplète.
• Pour essayer Verus, il faut être prêt à demander de l’aide sur Zulip.

Essayez Verus

• Pour essayer Verus dans le navigateur, visitez Verus Playground.
• Pour des développements plus complexes, suivez les instructions d’installation et consultez d’abord les documents de départ, notamment le tutoriel et la référence, puis ceux ci-dessous.

Documentation Verus

• Tutoriels et références
• Documentation de l’API de la bibliothèque standard de Verus
• Guide de vérification du code concurrent
• Objectifs du projet
• Contribution à Verus
• Licence

Contacter, signaler des problèmes et lancer des discussions

• Si vous souhaitez signaler un problème, démarrer une discussion ou échanger en temps réel et obtenir de l’aide, reportez-vous à GitHub ou rejoignez Zulip.
• Utilisez les issues GitHub pour les bogues de fonctionnalités existantes et les discussions GitHub pour les demandes de fonctionnalités et les discussions plus ouvertes sur les fonctionnalités prévues.
• Les contributions sont les bienvenues ; si vous voulez contribuer du code, consultez les conseils de Contributing to Verus.

Opinion de GN⁺

• Rust est bien connu comme un langage adapté à la programmation système, garantissant sécurité et performance, et Verus semble un projet capable de renforcer encore ces atouts de Rust. En particulier, la vérification de la programmation concurrente est très intéressante.

• Cependant, le projet en est encore à ses débuts et le support de la syntaxe Rust semble limité, ce qui laisse penser qu’il faudra encore du travail avant une utilisation en production. Néanmoins, garantir la sûreté du code par analyse statique à l’avance est important, ce qui laisse entrevoir un fort potentiel de croissance.

• Bien que le projet soit encore au stade initial, avec une documentation encore insuffisante et une syntaxe prise en charge limitée, il devrait pouvoir devenir un projet important dans l’écosystème Rust sur le long terme. Son utilité pourrait être élevée notamment dans la programmation système ou la blockchain, où la fiabilité est essentielle.

[GN⁺]

Commentaires Hacker News

• J'ai écrit un contrôleur Kubernetes formellement vérifié avec Verus
  • On peut prouver une propriété de liveness selon laquelle le contrôleur finira par ajuster le cluster vers le desired state demandé
  • Spécifier la correction comporte de nombreuses subtilités et nuances (changement rapide des exigences d'état désiré, asynchronisme, pannes, etc.)
  • Le code se trouve sur GitHub et est lié à un article qui paraîtra à OSDI 2024
• Une petite avancée vers Verus : il est possible d'ajouter des préconditions et des postconditions avec debug_assert en Rust
  • Le compilateur Rust les supprime par défaut dans les builds de production
  • Le tutoriel Verus fournit des exemples, ainsi qu'un exemple de vérification runtime avec debug_assert
• Question de débutant sur la différence entre la vérification de la correction d'un code et la preuve de sa correction
  • Je me demande s'il existe de bonnes ressources d'apprentissage sur la "preuve" de code pour des développeurs praticiens ayant une base limitée en informatique ou en mathématiques
  • Je suis très curieux de comprendre pourquoi la preuve "zero knowledge" est si importante et pourquoi elle est si pertinente
• Rust n'a pas encore de standard pour ça, contrairement à C/C++, Common Lisp, Ada/SPARK2014
  • Par rapport aux outils de vérification développés pour Ada/SPARK2014, etc., c'est une cible qui bouge
• Dafny est un langage de programmation "conscient de la vérification" compilable en Rust (GitHub)
• L'un des principaux contributeurs a fait une excellente présentation de Verus lors d'un meetup Rust à Zurich (YouTube)
  • Le fait que le code ghost s'intègre proprement au programme m'a particulièrement impressionné (ça m'a un peu rappelé Ada)
• Comparaison entre Verus et SPARK
  • S'agit-il d'un vérificateur de la même catégorie ? Quelles sont les différences, en dehors du fait que Verus est un vérificateur pour Rust et non pour Ada ?
• Quelqu'un ayant une bonne maîtrise de Verus peut-il comparer les performances et l'expressivité de Verus et Lean4 ?
  • Je comprends que Verus est un outil de vérification basé sur SMT, et Lean un assistant de preuve interactif et un outil basé sur SMT
  • Cependant, ma compréhension de la vérification formelle est limitée, donc il vaudrait mieux obtenir l'avis de quelqu'un d'expérimenté en techniques formelles logicielles
• Y a-t-il une relation entre Verus et Kani, ou bien fonctionnent-ils différemment ? (GitHub Kani)
• Existe-t-il un moyen d'implémenter cela de façon à ce que le code résultant reste un code Rust valide compilable avec les outils Rust vanilla ?