La société franco-américaine AdaCore, fournisseur d'outils et de services de développement logiciel à haute intégrité, annonce le début d’une collaboration avec les chercheurs de l’université américaine Carnegie Mellon University (CMU), située à Pittsburg en Pensylvanie, en vue de travailler sur la vérification formelle du langage Rust.
Et ce en s’appuyant sur Verus, un outil open source permettant de prouver mathématiquement la correction du code Rust.
Cette collaboration associe les trente années d’expérience d’AdaCore en matière d’assurance logicielle pour les systèmes à haute intégrité avec l’outil de vérification formelle Verus, centré sur l’analyse du langage Rust, pour la vérification de codes utilisés dans des systèmes critiques.
Ensemble, AdaCore et les chercheurs de CMU vont ainis proposer aux équipes qui travaillent sur des systèmes à haute intégrité une voie crédible pour une utilisation d’un code Rust “prouvé” qu’il s’agisse de lancer un nouveau projet ou d’intégrer Rust au sein de systèmes existants développés en Ada, SPARK, C ou C++.
Dans le détail, Verus permet notamment de prouver mathématiquement la correction fonctionnelle du code bas niveau et critique sans ajout de coût à l'exécution (zero-cost abstractions).
AdaCore rappelle que sa solution SPARK Pro permet déjà, par des méthodes de preuve statique, de garantir l’absence d’erreurs à l’exécution et de démontrer la correction fonctionnelle de logiciels utilisés dans les secteurs de l’avionique, de la défense, du spatial, du ferroviaire et du médical.
A ce niveau, l’outil Verus apporte des capacités de preuve similaires pour le langage Rust, étendant ses garanties de sécurité - initialement limitées à la gestion de la mémoire - à une approche de correction fonctionnelle complète, sans aucun surcoût à l’exécution.
Selon Bryan Parno, professeur en génie électrique et informatique ainsi qu’en informatique à l’université Carnegie Mellon, et co-développeur de Verus, le “vérificateur d’emprunts” - borrow checker (*) - de Rust applique déjà une forme de vérification statique. Mais l’outil Verus étend cette vérification aux propriétés réellement cruciales pour le système à haute intégrité.
« La demande pour des logiciels formellement prouvés ne cesse de croître dans l’industrie, et l’intelligence artificielle accélère cette tendance sur deux fronts, explique Quentin Ochem, directeur des produits (Chief Product Officer) chez AdaCore. Le code généré par l’IA renforce le besoin d’une vérification rigoureuse, tandis que le développement assisté par l’IA rend les méthodes formelles plus accessibles, en aidant les développeurs à rédiger des spécifications et des annotations de preuve.»
(*) Le “borrow checker “est un composant central du compilateur Rust qui garantit la sécurité mémoire et la sécurité des threads au moment de la compilation, sans nécessiter de ramasse-miettes (garbage collector). Au lieu de suivre l'utilisation de la mémoire pendant l'exécution d’un programme, le “borrow checker” examine la structure du code et les flux de données avant même toute exécution.
-dissolve-basic-fr.jpg)
