Le CEA-List a développé un savoir-faire reconnu dans les méthodes formelles d’analyse semi-automatique du code informatique. Ces méthodes sont utilisées dans l’univers des systèmes critiques, notamment dans l’aéronautique, pour garantir la sûreté d’un logiciel tant vis-à-vis d’éventuels bugs de fonctionnement que de la présence d’une faille de sécurité. Le CEA-List développe des outils permettant de les rendre utilisables par un public plus large de développeurs.
Le CEA-List a développé une forte compétence dans le domaine des méthodes formelles. Ces techniques permettent de valider l’absence de bug ou failles de sécurité dans un code source, qu’il ait été écrit par un développeur ou généré automatiquement à partir d’un modèle. Utilisée notamment en aéronautique, cette technique reste le domaine de rares experts extrêmement spécialisés. Les chercheurs du programme INCA cherchent à démocratiser cette approche en proposant des outils intégrés et simples d’emploi qui ne s’adressent plus seulement aux experts des méthodes formelles, mais directement aux développeurs.
Le besoin de méthodes formelles tend à s’accroître dans de nombreux secteurs industriels où la part de l’informatique embarquée dans les produits augmente. C’est notamment le cas dans le secteur automobile avec l’électrification des véhicules. L’objectif du programme INCA est désormais de démocratiser cette approche auprès de ces industriels.
La volonté du List s’est matérialisée avec Frama-C, un outil publié sous licence open source et librement téléchargeable par les développeurs. L’objectif de la recherche est de masquer la complexité de l’approche en fournissant des outils fortement automatisés et posant un minimum de contraintes d’utilisation.
Outre l’effort pour proposer des outils d’analyse de code opérationnels et immédiatement utilisables par les entreprises, les chercheurs du programme INCA poursuivent la recherche théorique sur les méthodes formelles.
Ils mettent à jour les modèles d’analyse pour accompagner l’évolution des langages informatiques, intégrer les nouveaux paradigmes de programmation et associer aux vérifications les caractéristiques matérielles via des modèles formels des architectures des systèmes visés. De même, ils créent de nouveaux cadres théoriques pour répondre aux évolutions des modèles de calcul et de communication.
Si les outils développés dans le cadre du programme INCA visent à démocratiser l’usage des méthodes formelles auprès des développeurs, la recherche porte aussi sur leur intégration aux chaînes d’intégration continue et DevOps. L’objectif est d’automatiser et de systématiser les tests portant sur la qualité du code source afin de produire des applications de meilleure qualité et plus sûres.
Ce type d’approche va permettre l’arrivée sur le marché de produits digitaux sûrs par construction (secure by design). Et, par exemple, d’apporter une réponse aux enjeux de plus en plus critiques de cybersécurité vis-à-vis des objets connectés.
Les chercheurs en méthodes formelles du programme INCA participent aux projets ANR SOPRANO, au projet européen STANCE ainsi qu’au projet Chekofv de la DARPA.
