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进行形式化验证的案例研究。该库代码高度依赖链表和复杂数据结构，给验证工具带来了巨大挑战。我们阐述了实践中遇到的若干问题与局限，通过实例说明并提出解决方案，最终实现了对代表性函数子集的功能属性验证及运行时错误验证。文中总结了验证结果，并提出了为实现目标代码完全形式化验证所需的工具改进方向。