PolyVer : Une Approche Compositionnelle pour la Modélisation et la Vérification de Systèmes Polyglotes

Informations Fondamentales

• ID de l'article : 2503.03207
• Titre : PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
• Auteurs : Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, Sanjit A. Seshia
• Classification : cs.PL (Langages de Programmation)
• Date de publication/Conférence : Formal Methods in Computer-Aided Design 2025
• Lien de l'article : https://arxiv.org/abs/2503.03207

Résumé

Les systèmes logiciels polyglotes (systèmes polyglotes) sont composés de programmes implémentés dans plusieurs langages de programmation, mais les vérificateurs de programmes existants sont généralement adaptés à un seul langage. Pour vérifier les systèmes polyglotes, il est généralement nécessaire de les traduire dans un langage de vérification commun ou une représentation formelle. Cet article propose PolyVer, une approche alternative qui effectue directement la vérification polyglote en utilisant l'abstraction, le raisonnement compositionnel et les techniques de synthèse. PolyVer construit les systèmes polyglotes comme des modèles formels de systèmes de transitions, où les fonctions de mise à jour liées aux transitions sont implémentées dans le langage cible (comme C ou Rust). Pour effectuer la vérification, PolyVer connecte le vérificateur de modèles du système de transitions aux vérificateurs spécifiques au langage par le biais de contrats de précondition/postcondition des fonctions de mise à jour. Ces contrats sont générés automatiquement par synthèse guidée par la syntaxe ou des oracles de synthèse basés sur les modèles de langage volumineux, et vérifiés par les vérificateurs spécifiques au langage.

Contexte de Recherche et Motivation

Définition du Problème

Les systèmes logiciels modernes adoptent de plus en plus des architectures polyglotes, comme les cadres ROS2 et Lingua Franca qui permettent aux développeurs de choisir le langage de programmation le plus approprié pour chaque composant. Cependant, cette flexibilité présente des défis de vérification :

1. Différences de sémantique des langages : Les différents langages de programmation possèdent des syntaxes et des sémantiques différentes. Par exemple, la fonction saturating_add de Rust sature à la valeur maximale en cas de débordement, tandis que l'addition en C peut entraîner un débordement circulaire.
2. Limitations des vérificateurs existants : La plupart des vérificateurs de programmes (comme CBMC pour C, Kani pour Rust) sont spécialement conçus pour un seul langage et ne peuvent pas traiter directement les systèmes polyglotes.
3. Complexité de la traduction : Traduire l'ensemble du système polyglote dans un seul langage de vérification nécessite de supporter la syntaxe et la sémantique complètes de tous les langages, ce qui est prohibitif pour les langages modernes.

Importance de la Recherche

La complexité croissante des systèmes polyglotes augmente le risque de défauts logiciels. Dans les domaines critiques pour la sécurité (comme la conduite autonome et l'aérospatiale), la vérification formelle fournit des garanties fortes, plutôt que de s'appuyer uniquement sur des méthodes incomplètes comme les tests.

Limitations des Approches Existantes

• Approches de traduction monolithique : Nécessitent de développer une infrastructure de compilateur complète pour chaque langage
• Difficultés de préservation sémantique : Difficile de capturer fidèlement toutes les constructions spécifiques au langage source dans le langage de vérification cible
• Problèmes d'évolutivité : Les problèmes de vérification générés peuvent devenir trop volumineux

Contributions Principales

1. Formalisation du problème de vérification polyglote : Première formalisation systématique du problème de vérification polyglote et proposition d'une solution compositionnelle intégrant plusieurs vérificateurs spécifiques au langage.
2. Synthèse automatisée de contrats : Proposition d'une méthode de synthèse et d'affinage automatisés des contrats de précondition/postcondition utilisant un langage intermédiaire et une boucle CEGIS-CEGAR, supportant la synthèse guidée par la syntaxe et les modèles de langage volumineux comme oracles de synthèse.
3. Implémentation d'outil : Implémentation de l'outil PolyVer basé sur UCLID5, supportant C et Rust, via les vérificateurs CBMC et Kani, démontrant que les oracles de synthèse basés sur LLM surpassent les approches de synthèse purement symboliques.
4. Études de cas et évaluation : Développement d'un vérificateur pour le langage de coordination Lingua Franca, vérification de systèmes polyglotes contenant des processus C et Rust, ainsi que des fragments de langage C que les travaux antérieurs ne pouvaient pas supporter.

Explication Détaillée de la Méthode

Définition de la Tâche

Entrée : Modèle polyglote M = (Q,V,I₀,T,F) et propriété système φ Sortie : Résultat de vérification (réussi/échoué) et trace de contre-exemple possible Objectif : Déterminer si M ⊨ φ est vrai

Où :

• Q : Ensemble de modes
• V : Ensemble de variables typées
• I₀ : Ensemble d'états initiaux
• T : Ensemble de transitions de modes
• F : Ensemble de procédures

Architecture du Modèle

1. Machine à États Étendue (ESM)

PolyVer modélise les systèmes polyglotes comme des machines à états étendues, où :

• Les états sont composés de modes et d'assignations de variables
• Les transitions sont associées à des conditions de garde et des relations de mise à jour
• Les relations de mise à jour sont spécialisées en séquences d'appels de procédures

2. Langage de Contrat Intermédiaire L*

L'innovation clé est l'introduction du langage intermédiaire L* comme « colle » entre les différents langages :

• Les contrats sont écrits en L*
• Transformés en langages concrets via une compilation préservant la sémantique compL
• Évite la complexité de la traduction complète du langage

3. Approche Hybride CEGIS-CEGAR

Le cœur de l'algorithme est une boucle itérative à deux niveaux :

Boucle CEGAR externe :

1. Construire un modèle abstrait M' avec les contrats actuels
2. Le vérificateur de modèles vérifie M' ⊨ φ
3. En cas d'échec, vérifier si le contre-exemple est faux
4. S'il est faux, affiner le contrat ; sinon, signaler le vrai contre-exemple

Boucle CEGIS interne :

1. L'oracle de synthèse génère des contrats candidats
2. Le vérificateur d'oracle vérifie la validité du contrat
3. S'il n'est pas valide, ajouter des exemples positifs et resynthétiser

Points d'Innovation Technique

1. Stratégie de Vérification Compositionnelle

Contrairement à la traduction monolithique, PolyVer adopte une stratégie « diviser pour régner » :

• Utiliser l'abstraction par contrat pour les procédures individuelles
• Les vérificateurs spécifiques au langage vérifient la validité des contrats
• Le vérificateur de modèles vérifie les propriétés au niveau du système

2. Génération Automatisée de Contrats

Support de multiples oracles de synthèse :

• Synthétiseur basé sur LLM : Utilise des invites de chaîne de pensée et DSL Python
• Synthétiseur SyGuS/SyMO : Encode le problème comme un problème de programmation par exemple

3. Vérification de Fausseté

Vérifier la réachabilité des traces de contre-exemple par {V = d} C {V' ≠ d'}, distinguant les vrais contre-exemples des faux.

Configuration Expérimentale

Ensemble de Données

1. Ensemble de tests LFVerifier : 22 programmes Lingua Franca avec syntaxe C restreinte
2. Exemples LF complets : Contrôleur LED, robot grimpeur, contrôleur d'attitude de satellite et autres systèmes embarqués
3. Systèmes polyglotes : Programmes LF mixtes C/Rust, applications ROS2, programmes d'appels FFI

Métriques d'Évaluation

• Nombre d'itérations de synthèse (IS : itérations CEGIS, AR : itérations CEGAR)
• Temps d'exécution (SOT : temps d'oracle de synthèse, VOT : temps d'oracle de vérification, UT : temps UCLID5)
• Taux de réussite de vérification

Méthodes de Comparaison

Comparaison avec LFVerifier15, le seul outil connu de vérification automatisée end-to-end de programmes LF.

Détails d'Implémentation

• Utilisation d'OpenAI o1-mini comme synthétiseur LLM, 3 requêtes parallèles par procédure
• CBMC-6.3.1, Kani-0.56.0, z3-4.8.7 comme backends de vérification
• Machine Intel Core i9 3.7GHz, 62GB RAM

Résultats Expérimentaux

Résultats Principaux

RQ1 : Comparaison avec les Travaux de Vérification LF Existants

Sur 22 tests de référence :

• PolyVer vérifie avec succès tous les tests de référence, LFVerifier ne peut pas vérifier l'exemple TrafficLight
• 18 tests de référence synthétisent correctement les contrats en une seule itération CEGIS, temps moyen 37 secondes
• Bien que le temps d'exécution total soit plus lent (dominé principalement par le temps de synthèse de contrats), il fournit des améliorations qualitatives significatives

RQ2 : Traitement des Exemples LF Complets

Vérification réussie de systèmes embarqués contenant du code C complet :

• Contrôleur LED : 1 procédure, 123 lignes de code C, 31,0 secondes de temps de synthèse
• Robot grimpeur : 12 procédures, 75 lignes de code C/Rust, 685,4 secondes de temps de synthèse
• Contrôleur satellite : 6 procédures, 424 lignes de code C, 729,0 secondes de temps de synthèse

RQ3 : Vérification de Systèmes Polyglotes

Vérification de vrais systèmes polyglotes :

• Programmes LF mixtes C/Rust
• Applications de service ROS2
• Programmes d'appels FFI entre langages

Découvertes Importantes

1. LLM surpasse les méthodes symboliques : Les solveurs SyGuS/SyMO nécessitent de nombreuses itérations CEGAR et échouent souvent à terminer
2. Défis de la synthèse de contrats : Les procédures avec flux de contrôle complexe et dépendances de données nécessitent plus d'itérations
3. Vérification de praticité : Capable de traiter du code d'implémentation réel plutôt que des exemples jouets

Travaux Connexes

Vérification de Systèmes Polyglotes

• Méthodes de traduction manuelle : Cook et al. traduisent le code assembleur en C pour vérifier l'hyperviseur Xen
• Traduction automatisée de fragments : LFVerifier traduit automatiquement les fragments C en langage de vérification
• Approches boîte noire : Déduire les résumés du comportement entrée-sortie

Vérification Compositionnelle

• La vérification compositionnelle basée sur la logique de Hoare est largement appliquée aux grands programmes monolingues
• Utilisation de l'interprétation abstraite et CEGAR pour automatiser l'apprentissage des préconditions/postconditions

Inférence de Contrats

• Méthodes d'inférence de contrats guidées par les propriétés
• Solveurs de clauses Horn de contrainte
• Applications récentes des LLM dans l'apprentissage de spécifications

Conclusion et Discussion

Conclusions Principales

1. PolyVer résout avec succès les défis clés de la vérification de systèmes polyglotes
2. L'approche compositionnelle évite la complexité de la traduction complète du langage
3. La synthèse automatisée de contrats rend la méthode pratique
4. Les synthétiseurs basés sur LLM surpassent les méthodes symboliques traditionnelles

Limitations

1. Terminaison : L'algorithme ne garantit pas la terminaison, dépendant de la qualité de l'oracle de synthèse
2. Support linguistique : Actuellement limité à C et Rust, nécessite le développement d'oracles de vérification pour d'autres langages
3. Expressivité des contrats : La capacité d'expression du langage intermédiaire L* limite la complexité des propriétés vérifiables
4. Évolutivité : Le temps de synthèse de contrats pour les grands systèmes peut devenir un goulot d'étranglement

Directions Futures

1. Extension à d'autres systèmes logiciels polyglotes distribués et systèmes robotiques
2. Application à la vérification formelle de la traduction de code (comme la traduction C vers Rust)
3. Amélioration de l'efficacité et de la précision de la synthèse de contrats
4. Support de propriétés logiques temporelles plus complexes

Évaluation Approfondie

Avantages

1. Importance du problème : La vérification de systèmes polyglotes est un problème pratique et important
2. Innovativité de la méthode : La combinaison de vérification compositionnelle + synthèse automatisée de contrats est nouvelle
3. Fondations théoriques : Définitions formelles claires, garanties de correction explicites
4. Valeur pratique : Capable de traiter des systèmes réels plutôt que des exemples jouets
5. Implémentation d'outil : Fournit une implémentation d'outil utilisable

Insuffisances

1. Surcharge de performance : Le temps de synthèse de contrats est relativement long, pouvant limiter les applications pratiques
2. Couverture linguistique : Actuellement limité à C et Rust, l'extensibilité reste à vérifier
3. Benchmarks limités : Bien que contenant des exemples réels, l'échelle est relativement petite
4. Dépendance aux LLM : Dépend des services LLM commerciaux, pouvant affecter la reproductibilité

Impact

1. Contribution académique : Ouvre une nouvelle direction de recherche pour la vérification de systèmes polyglotes
2. Valeur pratique : Fournit un outil de vérification pour les systèmes polyglotes critiques pour la sécurité
3. Inspiration technique : L'idée d'utiliser les contrats comme interface entre langages a une valeur universelle

Scénarios d'Application

1. Systèmes embarqués : Systèmes temps réel mixtes C/Rust
2. Systèmes distribués : Cadres multilingues comme ROS2, gRPC
3. Applications critiques pour la sécurité : Systèmes nécessitant les garanties de vérification formelle
4. Intégration de systèmes hérités : Systèmes avec mélange de code ancien et nouveau

Références Bibliographiques

L'article cite 50 références connexes, couvrant plusieurs domaines incluant les systèmes polyglotes, la vérification formelle, l'inférence de contrats, la synthèse guidée par la syntaxe et d'autres travaux importants, fournissant une base théorique solide pour la recherche.

Évaluation Globale : Ceci est un article de recherche systématique de haute qualité qui résout un problème important et pratique. La méthode est innovante, l'expérimentation est complète et l'implémentation de l'outil est achevée. Bien qu'il y ait encore de la place pour l'amélioration en termes de performance et d'évolutivité, il apporte une contribution importante au domaine de la vérification de systèmes polyglotes.