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.

翻译：可信平台模块（TPM）是一种用于保护现代计算机完整性与安全性的密码协处理器。与TPM的通信通过TPM软件栈（TSS）进行，其中开源库tpm2-tss是一种广泛使用的实现。其代码中的漏洞可能使攻击者能够恢复敏感信息并控制系统。本文描述了一项使用Frama-C验证平台对tpm2-tss进行形式化验证的案例研究。该库代码高度依赖链表与复杂数据结构，对验证工具构成了极大挑战。我们展示了所遇到的若干问题与局限，通过示例加以说明，并提出了允许我们验证代表性函数子集的函数性质和无运行时错误的解决方案。我们还描述了验证结果及为实现目标代码的完全形式化验证所需的工具改进方向。