Search for a command to run...
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.