Formal verification of trusted layers of software : application to the TPM Software Stack
Le Trusted Platform Module (TPM) est un cryptoprocesseur conçu pour protéger l'intégrité et la sécurité des ordinateurs modernes. Les communications avec le TPM passent par la TPM Software Stack (TSS), qui joue le rôle de couche de confiance pour le TPM. La bibliothèque open-source tpm2-tss (éc...
Enregistré dans:
| 主要作者: | |
|---|---|
| 其他作者: | , , , , , |
| 格式: | Thèse numérique |
| 語言: | Anglais |
| 出版: |
2025.
|
| 主題: | |
| 在線閱讀: | Accès au texte intégral https://theses.univ-orleans.fr/public/2025ORLE1055_va.pdf http://www.theses.fr/2025ORLE1055/abes https://theses.hal.science/tel-05540117 |
| 提示: |
Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : École doctorale Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes (Centre-Val de Loire ; 2012-....) Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire) Autre(s) contribution(s) : Claude Marché (Président du jury) ; Wolfgang Ahrendt (Membre(s) du jury) ; Catherine Dubois, Alain Giorgetti (Rapporteur(s)) |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | Vérification formelle de couches de confiance dans les logiciels :, application à la TPM Software Stack |
| 總結: | Le Trusted Platform Module (TPM) est un cryptoprocesseur conçu pour protéger l'intégrité et la sécurité des ordinateurs modernes. Les communications avec le TPM passent par la TPM Software Stack (TSS), qui joue le rôle de couche de confiance pour le TPM. La bibliothèque open-source tpm2-tss (écrite en C) est une implémentation largement utilisée de la TSS. Actuellement, la spécification et la vérification d'applications critiques pour la sécurité telles que la librairie tpm2-tss restent un défi important, en particulier lorsque le code n'est pas écrit dans l'optique d'être vérifié. L'objectif de cette thèse est d'explorer dans quelle mesure il est actuellement possible de spécifier et de vérifier des propriétés de sécurité, des propriétés fonctionnelles et des propriétés de sûreté sur un code critique qui n'a pas été pensé pour la vérification. La plateforme de vérification Frama-C et certains de ses principaux analyseurs (Wp, E-ACSL et MetAcsl) sont utilisés pour étudier l'efficacité de diverses techniques de vérification dans ce contexte. En ce qui concerne la vérification déductive à l'aide de Wp, la spécification et la vérification de propriétés fonctionnelles et de l'absence d'erreurs à l'exécution sur un sous-ensemble représentatif de fonctions mettent en évidence plusieurs limitations et des solutions de contournement nécessaires, notamment lorsqu'il s'agit d'allocations dynamiques et de structures de données récursives. Par ailleurs, lorsque la vérification déductive s'avère difficile à appliquer à ce type de code, l'outil de vérification à l'exécution E-ACSL est utilisé pour vérifier les propriétés de sécurité de haut niveau écrites avec MetAcsl. Cette approche offre un moyen plus accessible d'évaluer des propriétés de haut niveau sur des programmes de grande taille, mais donne moins de confiance dans les résultats de la vérification. Enfin, nous explorons des approches combinées pour évaluer les propriétés de tels programmes : d'abord en combinant la vérification déductive avec l'analyse de forme fournie par l'outil MemCAD pour se concentrer sur les propriétés de bas niveau; ensuite en combinant Wp et E-ACSL pour la vérification d'exigences de haut niveau écrites avec MetAcsl. The Trusted Platform Module (TPM) is a cryptoprocessor designed to protect integrity and security of modern computers. Communications with the TPM go through the TPM Software Stack (TSS), which assumes the role of a trusted layer for the TPM. The open-source library tpm2-tss (written in the C programming language) is a widely used implementation of the TSS. Currently, the specification and verification of security-critical applications such as tpm2-tss remains an important challenge, especially when the code is not written with an intention of verification in mind. The goal of this thesis is to explore to what extent it is currently possible to specify and verify safety, functional and security properties on critical code not designed for verification. The Frama-C verification platform and some of its main analyzers (Wp, E-ACSL and MetAcsl) are used to investigate the efficiency and effectiveness of various verification techniques in this context. Regarding deductive verification using Wp, the specification and verification of functional properties and the absence of runtime errors on a representative subset of functions highlights several limitations and necessary workarounds, notably when dealing with dynamic allocations and recursive data structures. Alternatively, when deductive verification has proved to be a challenge for such code, the runtime verification tool E-ACSL is used to verify high-level security properties written with MetAcsl. This approach offers a more accessible way to assess high-level properties over large programs, but provides less confidence in verification results. Finally, we explore combined approaches to evaluate properties on such programs: first by combining deductive verification with the shape analysis provided by the MemCAD tool to focus on low-level properties; then by combining Wp and E-ACSL for the verification of high-level requirements written with MetAcsl. |
|---|---|
| Item Description: | Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : École doctorale Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes (Centre-Val de Loire ; 2012-....) Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire) Autre(s) contribution(s) : Claude Marché (Président du jury) ; Wolfgang Ahrendt (Membre(s) du jury) ; Catherine Dubois, Alain Giorgetti (Rapporteur(s)) |
| 格式: | Configuration requise : un logiciel capable de lire un fichier au format : PDF |