Contexte et motivations
Le développement de logiciels système, où la sûreté et la performance sont critiques, impose des exigences de vérification très strictes. Malgré l’existence d’outils de vérification avancés, les programmeurs traditionnels restent largement exclus du processus, ce qui augmente les coûts de développement et de maintenance. L’article identifie le principal obstacle comme étant la fracture entre les environnements de programmation (C) et les cadres de preuve (Coq, Isabelle, etc.). Cette dissociation empêche une vérification en temps réel et décourage l’implication directe des développeurs.
Pour combler ce fossé, les auteurs proposent C*, un langage qui prolonge le C avec des constructions de preuve intégrées. L’objectif est de rendre la vérification accessible sans quitter l’environnement de codage habituel, tout en conservant la capacité d’exprimer les idiomes bas‑niveau propres à C.
Architecture de C* et mécanismes de preuve
C* repose sur deux piliers techniques : un moteur d’exécution symbolique et un noyau de preuve de type LCF. Le moteur explore les chemins d’exécution du code C en générant des expressions symboliques qui représentent les valeurs d’entrée possibles. Ces expressions alimentent le noyau LCF, qui garantit la cohérence logique des preuves grâce à une petite base d’inférences vérifiées à la main.
Le langage introduit des proof‑code blocks que l’on écrit directement à côté du code d’implémentation. Par exemple, une annotation @assume ou @assert peut être placée avant ou après une instruction, ce qui déclenche une mise à jour immédiate de l’état de preuve. Cette approche permet une interaction itérative : chaque modification du code entraîne une recomposition partielle du graphe de preuve, évitant ainsi la recompilation complète du modèle.
En outre, C* offre un système de bibliothèques logiques réutilisables. Les développeurs peuvent déclarer des définitions, des théorèmes et des tactiques d’automatisation dans le même fichier source, ce qui simplifie la construction de preuves complexes et favorise le partage de connaissances entre projets.
Évaluation expérimentale et limites
Les auteurs ont implémenté un prototype fonctionnel et l’ont testé sur deux ensembles : (i) un benchmark de petits programmes C couvrant les constructions de boucle, les pointeurs et les structures, et (ii) une étude de cas réelle portant sur la fonction attach du buddy allocator de pKVM. Le benchmark montre que C* accepte la majorité des idiomes C courants, tout en générant des preuves complètes pour chaque assertion insérée.
Dans le cas de pKVM, la fonction attach implique une gestion fine de la mémoire et des invariants de fragmentation. Le moteur symbolique a pu explorer les chemins critiques, tandis que le noyau LCF a produit une preuve de l’absence de débordement de tampon et de la préservation des invariants d’allocation. Le temps de vérification, mesuré en dizaines de secondes, reste compatible avec un cycle de développement itératif, bien que la charge augmente proportionnellement à la profondeur des boucles imbriquées.
Les limites signalées concernent principalement la prise en charge des constructions C les plus avancées, telles que les macros variadiques et les appels indirects via des pointeurs de fonction. Le prototype ne supporte pas encore les extensions GNU spécifiques, ce qui restreint son applicabilité aux projets purement conformes au standard C11. De plus, la dépendance à un moteur d’exécution symbolique impose un coût mémoire non négligeable pour les programmes de grande taille, ce qui pourrait freiner l’adoption dans des bases de code très volumineuses.
