  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), a popular implementation of which is the
open-source library tpm2-tss. Vulnerabilities in its code could allow attackers
to recover sensitive information and take control of the system. This paper
describes a case study on formal verification of tpm2-tss using the Frama-C
verification platform. Heavily based on linked lists and complex data
structures, the library code appears to be highly challenging for the
verification tool. We present several issues and limitations we faced,
illustrate them with examples and present solutions that allowed us to verify
functional properties and the absence of runtime errors for a representative
subset of functions. We describe verification results and desired tool
improvements necessary to achieve a full formal verification of the target
code.
