Etude de l'apport des méthodes formelles déductives pour les développements de sécurité

• Main Author: Jaeger, Eric
• Language: ENG
• Published: Université Pierre et Marie Curie - Paris VI 2010
• Subjects: [INFO:INFO_SE] Computer Science/Software Engineering; [INFO:INFO_OH] Computer Science/Other; Méthode formelle; Sécurité; Confiance; Raffinement; Plongement profond; De Bruijn
• Online Access: http://tel.archives-ouvertes.fr/tel-00468914; http://tel.archives-ouvertes.fr/docs/00/46/89/14/PDF/jaeger_thesis.pdf; http://tel.archives-ouvertes.fr/docs/00/46/89/14/PDF/jaeger_resume.pdf; http://tel.archives-ouvertes.fr/docs/00/46/89/14/ANNEX/jaeger_soutenance.pdf

La mise en oeuvre des méthodes formelles déductives lors du développement de systèmes permet d'obtenir des garanties mathématiques quant à leur validité. Pour cette raison, leur utilisation est recommandée ou exigée par certains standards relatifs à la sûreté de fonctionnement ou à la sécurité, tels que l'IEC 61508 ou les Critères Communs. Il reste cependant légitime de s'interroger sur la portée exacte des bénéfices obtenus. Certains aspects d'un système peuvent en effet échapper à la formalisation, et il n'est pas toujours facile d'identifier ces limitations ou leurs conséquences. De même, si la validité d'une preuve vérifiée mécaniquement est difficilement contestable, son utilisation pour justifier d'une confiance réelle dans le système physique n'est pas toujours admise. De telles questions sont particulièrement pertinentes dans le domaine de la sécurité, lorsque les systèmes sont l'objet d'attaques de la part d'agents intelligents ; par rapport à la sûreté il y a un changement radical de point de vue, qui justifie de s'interroger quant à l'application de principes ou de pratiques bien connus. Nous identifions les bénéfice et évaluons la confiance résultant de l'application des méthodes formelles déductives lors de développements de systèmes de sécurité. Cette analyse aborde les éventuelles difficultés, déviations ou problèmes qui peuvent être rencontrés et les illustre par des exemples. Elle comporte également une étude détaillée du concept de raffinement, et présente un plongement profond visant à valider la logique de la méthode B en Coq. Ce plongement conduit par ailleurs à l'étude des représentations à la de Bruijn.