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

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. This memoir addresses the question of the benefits and the confidence resulting of the application of deductive formal methods for the development or the verification of systems having security requirements. But it also illustrates how it is possible to abuse inadequate specifications or inconsistencies in the theories or the tools, for example allowing a malicious developer to trap a system while providing a formal certificate, or a malicious user to identify possible ways around proofs of compliance. Based on these observations, various strategies are considered to mitigate the risks and improve the overall security of a formally developed system. More specifically, a detailed study of the concept of refinement is presented, providing a generic vision which is applied to several deductive formal methods. It is used to highlight interesting points, and to understand the essence of possible abuses of the so-called Refinement Paradox. We identify for example the influence of parameters of the refinement relation which are generally left implicit in formal developments. This memoir also discusses at length the question of the validation of the theories and tools supporting formal methods, through a deep embedding of the B logic in Coq. Several shortcomings of the B theory are identified and corrected - illustrating the interest of such a validation - and a proven prover is developed. New results for the B logic are also presented, dealing with the replacement of subterms whose free variables are bound by the context. This embedding further leads to technical considerations about the mechanisation of languages, comparing for example various forms of de Bruijn representations. We study approaches with finer context management, enriched de Bruijn indexes, parallel substitutions, before deriving from our work a representation of the simply typed lambda-calculus without typing context.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