| Source | https://cyber.gouv.fr/publications/few-remarks-about-formal-development-secure-systems |
| Date de publication | 2008-12-03T00:00:00 |
| Date de mise à jour | 2008-12-03T00:00:00 |
| Description | 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. |
| Documents | |