A Few Remarks About Formal Development of Secure Systems

Publié le 03 Décembre 2008 Mis à jour le 03 Décembre 2008

Eric Jaeger, T. Hardin, HASE 2008

Les méthodes formelles permettent d'obtenir un très haut niveau d'assurance quant à la correction d'un développement. Leur utilisation est encouragée, et parfois exigée, lorsqu'il y a des exigences fortes en matière de sûreté de fonctionnement ou de sécurité.

Pourtant, il ne faut pas faire aveuglément confiance à un développement formel. Cet article analyse les problèmes potentiels qui peuvent se poser et identifie quelques pièges classiques à éviter lorsque des méthodes formelles déductives (telles que B, Coq, Focal, PVS, etc.) sont utilisées avec un objectif de sécurité. Il vise aussi à permettre une meilleure évaluation du réel niveau d'assurance obtenu.