- Verus est un outil qui vérifie la correction du code écrit en Rust : lorsque le développeur spécifie ce que le code doit faire, il vérifie statiquement que le code Rust exécutable satisfait cette spécification dans toutes les exécutions possibles
- Il fonctionne en prouvant que le code est correct à l’aide d’un solveur puissant, sans ajouter de vérifications à l’exécution, et ne prend actuellement en charge qu’une partie de Rust
- Dans certains cas, il peut aussi vérifier statiquement la correction de code qui manipule des raw pointers, au-delà de ce que permet le système de types standard de Rust
- Le projet est en développement actif ; certaines fonctionnalités peuvent être cassées ou manquantes, et la documentation n’est pas encore complète, de sorte que les utilisateurs doivent être prêts à demander de l’aide sur Zulip
- Le Verus Playground pour navigateur, les instructions d’installation, le tutoriel et la référence, la documentation API de la bibliothèque standard, le guide de vérification du code concurrent, ainsi que des exemples et des tests, sont proposés comme parcours d’apprentissage et d’expérimentation
Ce que Verus vérifie
- Verus est un outil de vérification de la correction du code Rust
- Le développeur rédige une spécification du comportement que le code doit avoir
- Verus vérifie statiquement que le code Rust exécutable satisfait toujours cette spécification dans toutes les exécutions possibles
- Au lieu d’ajouter des vérifications à l’exécution, il prouve la correction du code à l’aide d’un solveur
- Le périmètre pris en charge est actuellement un sous-ensemble de Rust, et des travaux sont en cours pour l’élargir
- Dans certains cas, il peut vérifier statiquement la correction de code allant au-delà du système de types standard de Rust, par exemple du code qui manipule des raw pointers
État du développement et points d’attention
- Verus est un projet en développement actif
- Certaines fonctionnalités peuvent être cassées ou absentes
- La documentation n’est pas encore complète
- Pour essayer Verus, il faut être prêt à demander de l’aide sur Zulip
- La communauté Verus a publié plusieurs articles de recherche, et divers projets dans l’industrie comme dans le monde académique utilisent Verus
- La liste correspondante est disponible sur la page publications and projects
Comment démarrer et outils de développement
- Pour essayer Verus dans le navigateur, on peut utiliser le Verus Playground
- Pour un usage plus poussé, il faut suivre les instructions d’installation
- L’apprentissage peut commencer avec le Tutorial and reference
- Le formateur automatique verusfmt pour le code Verus est également pris en charge
Documentation et ressources d’apprentissage
- Les ressources documentaires en cours d’élaboration comprennent notamment
- Tutorial and reference : tutoriel et référence Verus
- API documentation for Verus's standard library : documentation API de la bibliothèque standard de Verus
- Guide for verifying concurrent code : guide de vérification du code concurrent
- Contributing to Verus
- Best Practices pour publier des crates liées à Verus sur crates.io
- Verus License
- Verus Logos
Exemples et participation à la communauté
- Les exemples d’utilisation de Verus offrent plusieurs points de départ en plus de la documentation
- Publications and projects : publications et projets utilisant Verus
- Videos, slides, and exercises : vidéos, diapositives et exercices d’un tutoriel Verus sur une journée
- Standalone examples : exemples autonomes utilisant Verus sur des tâches petites et concrètes
- Small and medium-sized examples : exemples montrant diverses fonctionnalités de Verus
- Unit tests : tests contenant des exemples de syntaxe et de fonctionnalités de Verus
- Le signalement d’issues et les discussions peuvent se faire sur GitHub ou sur Zulip
- Pour les demandes de fonctionnalités et les discussions ouvertes, le projet utilise GitHub discussions ; pour les bugs reproductibles touchant des fonctionnalités existantes, il utilise GitHub issues
- Si vous souhaitez contribuer au code, vous pouvez consulter les indications de Contributing to Verus
1 commentaires
Commentaires sur Hacker News
J’ai essayé d’écrire un contrôleur Kubernetes formellement vérifié avec Verus
En gros, on peut prouver des propriétés de vivacité comme « le contrôleur finira par réconcilier le cluster vers l’état cible demandé »
Cela dit, quand l’état cible change rapidement, avec l’asynchronisme, les défaillances, etc., il y a beaucoup de subtilités jusque dans la manière de spécifier ce que signifie « correct »
Code : https://github.com/vmware-research/verifiable-controllers/, l’article associé devrait paraître à OSDI 2024
Comme petit tremplin vers Verus, on peut ajouter des debug_assert Rust aux préconditions et postconditions
Le compilateur Rust les supprime par défaut dans les builds de production
Dans les exemples de vérification du tutoriel Verus, on écrit la plage d’entrée et les conditions sur le résultat avec
requiresetensures, tandis que la version avec vérifications à l’exécution consiste à contrôler les mêmes conditions pendant l’exécution, par exempledebug_assert(-16 <= x1)oudebug_assert(x8 == 8 * x1)D’autres outils de preuve/vérification/conception par contrats pour Rust, comme Creusot, utilisent une syntaxe fondée sur les attributs, généralement plus légère et plus idiomatique pour Rust
Ce serait bien que de futures versions de Verus permettent aussi cette approche
C’est excellent comme outil de documentation, et cela complète très bien le système de types et les tests
"contracts": https://docs.rs/contracts/latest/contracts/J’ajoute des préconditions et postconditions à la plupart des fonctions, et la JVM dispose d’un flag permettant de les retirer facilement des builds de production
N’ayant pas beaucoup d’expérience réelle en informatique, je me demande quelle est la différence entre la vérification dans « vérifier la correction du code » dans le README et la « preuve » dont on parle ailleurs ?
Je serais aussi preneur de ressources adaptées à des programmeurs professionnels sans gros bagage en informatique/théorie ou en maths pour apprendre à « prouver » des choses à propos du code
En plus, je ne comprends pas vraiment pourquoi les preuves à divulgation nulle de connaissance sont si importantes et pertinentes. Par exemple, j’ai entendu parler de choses comme x.com/ZorpZK, mais je ne vois pas ce que cela a de génial
Cela dit, Verus et Coq, utilisé dans Software Foundations, ont des approches différentes
Verus essaie de prouver automatiquement des propriétés à l’aide d’un système automatique de résolution de contraintes appelé solveur SMT, tandis que Coq exige de prouver beaucoup plus de choses manuellement, avec une automatisation limitée
Les deux ont leurs avantages et leurs inconvénients ; l’automatisation est agréable quand elle fonctionne, mais frustrante quand ce n’est pas le cas
Il vaut mieux considérer les preuves à divulgation nulle de connaissance comme un domaine un peu distinct, et beaucoup de personnes travaillant sur la vérification/preuve formelle n’y touchent pas. Il est plus pertinent de les voir comme des primitives cryptographiques
Les preuves à divulgation nulle de connaissance ont un gros overhead et manquent de ce qu’on appelle une « killer app », donc leurs usages pratiques, leur importance et leur pertinence ne sont pas encore énormes, mais le concept est intéressant
Pour les ressources d’apprentissage, j’aimerais aussi qu’il y en ait. La documentation de Dafny est plutôt bonne, mais la vérification formelle de logiciels ne me semble pas encore au stade où elle est facile à utiliser pour un programmeur ordinaire qui n’a pas un doctorat en informatique ou en maths
Les exemples donnent l’impression que c’est relativement simple, mais on se heurte vite à « impossible à prouver », et les réponses au pourquoi plongent souvent dans des détails d’implémentation profonds que seul l’auteur semble pouvoir connaître
Par exemple, on peut vérifier que vous connaissez un mot de passe sans l’envoyer au serveur, ce qui rend plus difficile pour un serveur malveillant ou un attaquant de type homme du milieu de l’intercepter
Cela peut aussi offrir de meilleures options pour la vérification d’identité. On peut prouver que l’on possède une pièce d’identité délivrée par l’État sans transmettre le document lui-même au serveur, ce qui réduit les cas où il est conservé « au maximum 2 ans/3 ans/6 mois » avant de finir malgré tout par fuiter
Les preuves sur le code ne font pas encore partie du travail des programmeurs professionnels
La logique de Hoare est un bon point de départ, et elle est parfois enseignée dans les cours d’introduction à l’informatique
Coq a une courbe d’apprentissage abrupte, surtout si l’on n’est pas familier avec OCaml ou des langages similaires. Why3 pourrait être plus accessible aux débutants : https://www.why3.org
Preuve et vérification peuvent vouloir dire la même chose, mais « preuve » donne davantage l’impression d’un processus interactif, tandis que « vérification » suggère quelque chose qui peut être automatisé, comme du model checking ou la résolution SMT d’un programme annoté
Pour ceux qui ne connaîtraient pas de projets similaires, Dafny est un « langage de programmation conscient de la vérification » qui peut compiler vers Rust : https://github.com/dafny-lang/dafny
J’ai écrit il y a quelques jours un article d’introduction à Dafny pour débutants : https://www.linkedin.com/pulse/getting-started-dafny-your-fi...
Ça a l’air vraiment impressionnant. Des indications ou des exemples sur la façon d’ajouter des preuves à une base de code existante seraient sans doute utiles aux gens
Par exemple, imaginons une application GUI minimale avec une seule zone de texte, qui récupère via une requête HTTP un tableau inconnu au moment de la compilation et non fiable, le trie par tri à bulles, puis l’affiche
Le tri à bulles contient un bug volontaire, du type erreur off-by-one qui laisse le dernier élément inchangé, et les tests unitaires ne détectent pas ce bug par hasard. S’inquiéter du caractère incomplet des tests peut être une motivation majeure pour passer aux preuves
Il serait ensuite intéressant de montrer le processus consistant à remplacer les tests unitaires par une preuve, puis à découvrir et corriger le bug
Il n’est pas nécessaire d’expliquer en détail le code de preuve lui-même ; il suffit de se concentrer sur des détails réalistes comme la frontière entre le code mathématique prouvé et le code d’entrée/sortie non prouvé, les lignes de commande utilisées pour la preuve et le build, ou une archive zip que l’on peut manipuler soi-même
En fait, lire depuis l’entrée standard et écrire sur la sortie standard suffirait probablement
L’un des principaux contributeurs a fait une excellente présentation de Verus au meetup Zürich Rust : https://www.youtube.com/watch?v=ZZTk-zS4ZCY
J’ai été impressionné par la façon dont ce code « ghost » s’intègre proprement dans le programme, et cela m’a un peu rappelé Ada
Je me demande s’il existe déjà un standard pour Rust, comme pour C/C++, Common Lisp ou Ada/SPARK2014
S’il n’y en a pas, cela devient une cible mouvante par rapport aux outils de vérification développés pour Ada/SPARK2014
L’héritage d’Ada/SPARK2014, du bare metal jusqu’aux applications critiques pour la sécurité à haute intégrité, est aussi difficile à ignorer
C’est de ça dont tu parles ?
Je me demande quel est le lien entre ceci et Kani. Fonctionnent-ils différemment ?
https://github.com/model-checking/kani
Les vérificateurs automatiques basés sur SMT comme Verus, Dafny, F* et mon VCC exigent des annotations sur presque toutes les fonctions et boucles, mais offrent des garanties plus larges sur la correction du programme
Les outils basés sur des assistants de preuve interactifs comme Coq ou Lean nécessitent en général davantage de guidage de la part de l’utilisateur, mais peuvent garantir des propriétés plus complexes
Je me demande comment Verus se compare à SPARK
S’agit-il du même type général de vérificateur ? À part le fait que Verus soit un vérificateur pour Rust plutôt que pour Ada, en quoi est-il différent ?
Ce serait bien que quelqu’un qui connaît bien Verus puisse expliquer les différences de performances et d’expressivité entre Verus et Lean4
Je comprends que Verus est un outil de vérification basé sur SMT, tandis que Lean est à la fois un assistant de preuve interactif et un outil basé sur SMT
Mais comme ma compréhension du domaine de la vérification formelle est limitée, j’aimerais avoir l’avis de quelqu’un qui connaît bien les méthodes formelles appliquées au logiciel
Par exemple, comme dans le livre « Software Foundations » de Coq, on peut formuler et prouver des propositions sur du code C, mais presque personne ne semble le faire avec Lean, et l’outillage manque
On peut aussi écrire des programmes en Lean4 et prouver des propriétés à leur sujet, ce que certains commencent à faire très progressivement
Formaliser des mathématiques pures et publier des articles à leur sujet est aujourd’hui l’usage principal de Lean4 et de Coq
Les types de choses que Lean/Coq peuvent effectivement énoncer et prouver sont plus généraux, mais ce degré de généralité n’est peut-être pas nécessaire pour des programmes du monde réel