| L'avènement du réseau Internet a contribué au développement et à la prolifération des codes malicieux, dont le plus connu reste le virus informatique. Cette nouvelle donne dans le monde informatique constitue un véritable défi en termes de sécurité, de fiabilité, d'intégration, d'interopérabilité, de maintenance, etc. Plus que jamais, la qualité des logiciels prend de plus en plus d'importance et ne se restreint plus aux secteurs économiques jugés sensibles. Plus précisément, au cours de cette décennie, voire des prochaines décennies, la sécurité et la fiabilité des systèmes informatiques aura un essor grandissant. Une certification logicielle rigoureuse pourra être exigée. Le principal objectif de notre recherche est l'élaboration de méthodes et d'outils pratiques, fondés sur des aspects théoriques robustes, pour la certification de composantes logicielles. À cette fin, nous avons intégré deux techniques, la compilation certifiée et la vérification par évaluation de modèles ( modal-cheching), pour l'obtention d'un modèle global de certification de code tant au niveau des propriétés de sûreté qu'au niveau des propriétés de sécurité. Les principaux résultats ayant contribué à l'atteinte de cet objectif sont: (1) La formalisation d'un système de types pour un langage assembleur typé permettant de décider si un code objet satisfait des propriétés de sûreté. (2) La définition d'une sémantique tri-valuée pour le μ-calcul modal. Cette sémantique offre la possibilité de décider si une propriété est satisfaite par un modèle malgré le manque d'information relatif à des actions abstraites δ. (3) La définition d'une sémantique basée sur les tableaux. Ce système permet la construction d'évaluateurs de modèles efficaces. Nous proposons également les preuves de correction, de complétude et de terminaison de cette sémantique. (4) L'implantation d'un environnement de certification de code. |
