Spécifier et vérifier des exigences de haut niveau sur des programmes importants : application à la sécurité des programmes C

La spécification et la vérification d’exigences haut niveau (comme des propriétés de sécurité, telles que l’intégrité des données ou la confidentialité) reste un défi pour l’industrie, alors que les cahiers des charges en sont remplis. Cette thèse présente un cadre formel pour les exprimer appelé les meta-propriétés, décrites pour un langage de programmation abstrait, et centrées sur les propriétés liées aux manipulations de la mémoire et les invariants globaux. Ce cadre formel est appliqué au langage C avec HILARE, une extension d’ACSL, qui permet la spécification d’exigences haut niveau sur des programmes C de grande taille avec facilité. Des techniques de vérification pour HILARE, basées sur la génération d’assertions locales et la réutilisation des analyseurs de Frama-C existants, sont présentées et implantées dans le greffon MetAcsl pour Frama-C. Une méthodologie pour l’évaluation des propriétés de grands programmes est détaillée, articulant les méta-propriétés, les techniques de vérification et les particularités du C. Cette méthodologie est illustrée par un cas d’étude complexe : le bootloader de Wookey, un périphérique de stockage chiffré. Enfin, nous explorons une autre manière de vérifier une exigence de haut niveau en la déduisant à partir d’autres, via un système formel prouvé en Why3 et intégré dans MetAcsl.Specification and verification of highlevel requirements (such as security properties like data integrity or confidentiality) remains an important challenge for the industrial practice, despite being a major part of functional specifications. This thesis presents a formal framework for their expression called meta-properties, supported by a description on an abstract programming language, focusing on properties related to memory and global invariants. This framework is then applied to the C programming language, introducing the HILARE extension to ACSL, to allow easy specification of these requirements on large C programs. Verification techniques for HILARE, based on local assertion generation and reuse of the existing Frama-C analyzers, are presented and implemented into the MetAcsl plugin for Frama-C. A complete methodology for assessing large programs is laid out, articulating meta-properties, verification techniques and quirks specific to the C programming language. This methodology is illustrated to a complex case study involving the bootloader of WooKey, a secure USB storage device. Finally, we explore another way to verify a high-level requirement deducing it from others, through a formal system proven in Why3 and integrated in MetAcsl