Modélisation et vérification formelles de systèmes embarqués dans les cartes à microprocesseur (plate-forme Java Card et système d'exploitation)

Les travaux présentés dans ce mémoire ont pour objectif de renforcer le niveau de sûreté et de sécurité des systèmes embarqués dans les cartes à puce grâce à l'utilisation des Méthodes Formelles. D'une part nous présentons la vérification formelle de l'isolation des données de différentes applications chargées sur une même carte à puce, et plus précisément la preuve formelle, dans le système de preuve Coq, que le contrôle dynamique d'accès aux données implémenté par Java Card assure les propriétés de confidentialité et d'intégrité. D'autre part, nous nous sommes intéressés à la correction et à l'innocuité du code source bas niveau d'un système d'exploitation embarqué. Cette étude est illustrée par un module de gestion de mémoire Flash par journalisation, assurant la cohérence des données de la mémoire en cas d'arrachage de la carte du terminal. La vérification de propriétés fonctionnelles et locales a été développée à l'aide de l'outil Caduceus. Cet outil n'acceptant pas certaines constructions de bas niveau du langage C, telles que les unions et les casts, nous proposons des solutions pour la formalisation de ces constructions. Nous proposons également une extension de Caduceus permettant de spécifier et de vérifier le comportement d'une fonction en cas d'interruption soudaine de son exécution. Puis nous introduisons une méthodologie de vérification de propriétés globales de haut niveau sur un modèle formellement lié au code source. Plus précisément, nous décrivons l'extraction automatique d'un système de transitions formel, à partir d'annotations vérifiées par le code source. Ce système de transitions peut alors être plongé dans une logique d'ordre supérieur.The work presented in this thesis aims at strengthening the security and safety level of smart card embedded systems, with the use of Formal Methods. On one hand, we present the formal verification of the isolation of the data belonging to different applets loaded on the same card. More precisely, we describe the formal proof, in the Coq proof system, that the run-time access control, performed by the Java Card platform, ensures data confidentiality and integrity. On the other hand, we study the correctness and the safety of low level source code of an embedded operating system. Such source code is illustrated by a case study of a Flash memory management module, using a journalling mechanism and ensuring the memory consistency in the case of a card tear. The verification of functional and local properties has been developed using the Caduceus program verification tool. Since this tool does not support some low level constructions of the C language, such as the unions and the casts, we propose an analysis and some solutions for the formalisation of such constructions. We also propose an extension of Caduceus that allows to specify and verify the behaviour of a function in the case of sudden interruption of its execution. Then, we introduce a methodology for the verification of high level and global properties, which is meant for the expression and proof of this kind of properties on a model formally linked to the source code. More precisely, we describe an automatic extraction of a transition system from the annotations that are verified by the source code. This transition system can then be translated in a high order logic.ORSAY-PARIS 11-BU Sciences (914712101) / SudocVILLEURBANNE-DOC'INSA LYON (692662301) / SudocSudocFranceF