ANSSI

logo Agence nationale de la sécurité des systèmes d’information

Agence nationale
de la sécurité
des systèmes d’information


You are here : Home > The ANSSI > Publications > Scientific publications > Thesis > Study of the benefits of using deductive formal methods for secure developments

Study of the benefits of using deductive formal methods for secure developments

18 March 2010
Étude de l’apport des méthodes formelles déductives pour les développements de sécurité Imprimer Les fils d’actualité RSS de ssi.gouv.fr Envoyer cette page Réduire la taille du texte Agrandir la taille du texte

Eric Jaeger, ANSSI labs, PhD thesis, 8th march 2010

The use of formal methods in general, and of deductive formal methods in particular, for the development of systems aims at providing mathematical guarantees, for example about their correctness. For this reason, the use of formal methods is recommended or required by safety or security standards, such as the IEC 61508 or the Common Criteria.

Whereas formal approaches indeed induce important benefits, one may wonder about the exact extent of those. For example, some aspects of a system can be left out of the scope of formalisation, but it may not be easy to identify such restrictions or their consequences. If the validity of mechanically checked proofs is generally accepted, their applicability for justifying actual confidence in the physical systems is often questionned.

These question are especially relevant in the field of security, when the considered systems are targetted by intelligent agents; compared with the field of safety, there is a paradigm shift, preventing the application of well known facts or practices.

PDF - 1.3 Mb
Study of the Benefits of Using Deductive Formal Methods for Secure Developments
PDF - 1.3 Mb
PhD thesis, E. Jaeger, 8th march 2010
GZ - 222.1 kb
Study of the Benefits of Using Deductive Formal Methods for Secure Developments
GZ - 222.1 kb
Source code under CECILL-B license
texte - 20.8 kb
CECILL-B licence
texte - 20.8 kb
English language

Source codes developped during this thesis are provided under a free software licence.


FRENCH REPUBLIC | ANSSI © 2014 | Contact Us | Site Map
French governement Legifrance French civil service