Déduction Certifiée – DECERT

Les niveaux les plus élevés des standards de développement logiciel, comme le niveau EAL7des Critères Communs pour la certification de systèmes et des composants critiques, exigent l'utilisation de techniques formelles fondées sur des sémantiques mathématiques strictes. Ces techniques sont mécanisées par le biais d'outils déductifs qui permettent de démontrer des propriétés portant sur les logiciels. Notre vision à long terme est de contribuer à rendre l'utilisation de tels outils économiquement viable et, autant que possible, de rendre l'utilisation de méthodes formelles invisible aux développeurs et aux utilisateurs de systèmes. Afin que cette vision puisse se réaliser sur une échelle plus étendue, des composants automatisés et performants doivent interagir et forger un environnement de confiance pour le développement et/ou le déploiement de systèmes. L'objectif du projet DECERT est de concevoir une architecture pour des procédures de décision coopérant entre elles, avec une attention particulière portée à des fragments de l'arithmétique (arithmétiques bornée et non-bornée, sur les entiers et les réels, ...) et à leur combinaison avec d'autres théories concernant les structures de données (listes, tableaux, ensembles, ...). Pour garantir une confiance globale dans cette combinaison d'outils, les procédures de décision seront soit prouvées correctes à l'intérieur d'un assistant de preuve, soit produiront des certificats de résultat qui permettront à des outils extérieurs de vérifier la validité de leurs réponses. Nous définirons un format normlisé pour des témoins de preuves adapté aux procédures de décisions et leurs combinaisons. Ces témoins de preuve devront être produits sans trop de surcoût par les procédures de décisions et certifiés de manière efficace par les noyaux des assistants de preuve. Nous proposons d'utiliser ces procédures dans plusieurs scénarii d'application provenant à la fois du milieu académique et industriel et qui demandent des garanties élevées de confiance. En développement prouvé de systèmes, des modèles de haut niveau sont généralement écrits dans des langages expressifs de modélisation tels la logique d'ordre supérieure, B ou TLA+ et dont les problèmes de vérification ne peuvent être entièrement automatisés. Dans ce contexte, des procédures de décision automatiques doivent interagir avec des assistants de preuve comme Coq ou Isabelle, sans que les assurances fortes de correction associées à l'utilisation de ceux-ci soient compromises. Le deuxième scénario d'application que nous étudierons concerne l'utilisation de code téléchargé sur des plates-formes non dignes de confiance à travers le paradigme du code porteur de preuve (PCC : Proof Carrying Code). Afin de s'assurer que le code soit conforme à une politique de sûreté précise, il est assorti d'une preuve qui peut être généré par un outil de déduction automatique et qui est certifiée correcte sur le site hôte par un vérificateur de confiance. Dans les deux scénarii, la confiance repose sur un environnement de confiance fondé sur des certificats sous la forme de traces de preuve. En résumé, le projet se concentre sur les trois problèmes suivants : 1. Développer et implémenter des nouvelles et efficaces procédures de décision coopératives, en particulier pour des fragments de l'arithmétique. 2. Développer et standardiser une interface de sortie basée sur des certificats et des objets de preuve. 3. Intégrer les points 1 et 2 dans des assistants de preuve sceptiques, dans une architecture pour le code porteur de preuve et dans des outils de vérification tels que l'outil Rodin pour B et l'outil Frama-C du CEA pour la vérification de programmes C.