ANSSI

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.

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