迈向TPM软件栈的形式化验证：取得的成果与机遇

《Formal Aspects of Computing》：Towards Formal Verification of a TPM Software Stack: Achievements and Opportunities

本文通过Frama-C平台对TPM软件栈实现库tpm2-tss进行形式化验证，重点解决动态内存分配、链表结构及工具局限性问题。采用静态分配器替代动态内存，引入匿名块优化内存模型，并利用Coq证明辅助引理。验证了功能属性和运行时错误排除，识别了工具支持动态内存和更精细内存模型的需求，为后续完整验证奠定基础。

　　在现代计算机系统中，安全性和完整性是至关重要的特性。为了实现这些目标，Trusted Platform Module（TPM）作为一种安全硬件组件被广泛采用。TPM是一种加密处理器，用于保护计算机架构的完整性，并确保存储在其中的加密密钥的安全性。操作系统和应用程序通过一套称为TPM Software Stack（TSS）的API接口与TPM进行交互。在众多TSS的实现中，开源库tpm2-tss因其在安全领域的重要性而受到关注。然而，由于其代码的复杂性，包括大量使用链表和动态内存分配等特性，使得对其的正式验证变得极具挑战性。本文通过一个案例研究，探讨了使用Frama-C验证平台对tpm2-tss库进行正式验证的过程，分析了在验证过程中遇到的困难，并提出了一些解决方案。

Frama-C是一个用于C语言代码的开源验证平台，它包含了多个插件，其中Wp插件专门用于演绎验证。Wp插件能够根据C代码的注释（即acsl语言的注解）生成相应的证明义务（proof obligations），这些义务可以通过Wp自身或借助Why3平台和外部的定理证明器（如Coq）进行验证。Wp还可以自动添加必要的断言，并尝试证明这些断言，以确保程序中没有运行时错误（RTE），如无效指针访问、算术溢出或缓冲区溢出等。这些错误常常是导致安全漏洞的主要原因。因此，通过正式验证确保库的功能正确性与运行时安全性，是本文研究的核心目标。

在正式验证过程中，链表结构的处理是一个关键挑战。链表在tpm2-tss库中被广泛使用，用于管理TPM资源。为了处理链表，我们采用了acsl语言中的逻辑链表（logic list）定义，这是一种将C语言链表转换为逻辑结构的方法。通过这些定义，我们能够验证链表的正确性，包括其结构是否完整、是否无循环以及节点之间是否没有重叠。然而，现有的Frama-C/Wp验证工具对于动态内存分配的支持仍然有限，这使得验证过程中需要进行一些调整，例如使用静态内存分配器替代动态分配器，以实现对内存分配的精确控制。此外，由于Frama-C的内存模型不能直接处理链表的动态分配特性，我们不得不引入一些额外的分离谓词（separation predicates）来模拟内存的“新鲜性”（freshness）。

在处理内存分离问题时，我们还发现了一个重要的问题：当函数调用中使用了局部指针的地址时，该指针会被视为已被分配，从而影响整个函数中其他指针的分离状态。为了解决这一问题，我们采用了一种“匿名块”（anonymous blocks）的方法，将局部指针的使用限制在特定的代码块中，以避免其对其他内存区域的干扰。通过这种方式，我们能够确保链表的结构在函数执行过程中保持不变，并且其节点之间的分离关系仍然有效。此外，为了帮助验证工具更好地理解链表的结构，我们还添加了一些辅助注解，例如循环合同（loop contracts）和断言（assertions），这些注解能够引导验证过程，使得工具能够更准确地推导出链表的正确性。

除了链表的处理，我们还关注了内存管理的问题。例如，在验证过程中，我们发现某些函数调用可能会改变内存模型的状态，从而影响验证的准确性。为此，我们通过引入一些辅助函数和注解，确保内存的分配和释放行为能够被验证工具正确捕捉。此外，我们还对某些内存操作函数（如memcpy）进行了自定义的注解，以确保其行为符合预期，并且不会导致运行时错误。这些自定义注解的引入，使得我们能够绕过某些工具本身的限制，从而更有效地进行验证。

在正式验证的过程中，我们还需要证明一些关键的引理（lemmas）和断言（assertions）。这些引理和断言对于验证链表的结构和分离性至关重要。然而，由于Frama-C的逻辑链表定义与之前的版本有所不同，我们不得不重新证明这些引理，并适配现有的验证脚本。通过使用Coq这样的交互式定理证明器，我们能够证明这些引理，并确保它们能够被验证工具正确应用。这表明，尽管Frama-C在验证过程中提供了强大的功能，但在处理某些复杂结构时，仍然需要借助外部的定理证明器进行交互式证明。

验证的结果显示，我们成功地验证了tpm2-tss库中的一部分功能，包括功能正确性和运行时错误的消除。这些验证结果不仅验证了库中某些关键函数的行为，还确保了其内存操作的安全性。例如，在验证过程中，我们发现通过使用静态内存分配器和匿名块的方法，可以有效地解决动态内存分配带来的验证难题。此外，我们还验证了某些涉及链表操作的函数，确保它们在执行过程中不会破坏链表的结构，也不会导致指针访问错误。

总的来说，本文展示了如何通过Frama-C平台对tpm2-tss库进行正式验证，并探讨了在验证过程中遇到的主要挑战和解决方案。我们发现，尽管Frama-C在验证复杂C代码方面具有一定的优势，但在处理动态内存分配和链表结构时仍存在一些局限性。为了克服这些局限性，我们采用了一些自定义的分配策略和验证方法，包括使用静态内存分配器和引入额外的分离谓词。此外，我们还通过使用Coq这样的交互式定理证明器，证明了一些关键的引理和断言，以确保验证的准确性。

在验证过程中，我们还注意到一些工具本身的改进需求。例如，Frama-C/Wp目前缺乏对动态内存分配的直接支持，这使得验证某些关键功能变得困难。此外，其内存模型在处理链表结构时也存在一定的限制，需要引入额外的注解和验证策略来弥补。为了提高验证的自动化程度，我们期望未来Frama-C能够支持更全面的动态内存分配功能，并改进其内存模型，使其能够更精确地处理链表和内存分离的问题。

通过本文的研究，我们不仅验证了tpm2-tss库中的一部分功能，还为未来的正式验证工作提供了重要的参考。未来的工作可以包括对更多函数进行验证，特别是那些涉及更底层操作的函数。此外，还可以进一步探索如何将演绎验证与形状分析（shape analysis）相结合，以提高验证的自动化程度和准确性。形状分析是一种静态代码分析技术，能够自动推导出关于程序中复杂数据结构的精确不变式（invariants）。通过将形状分析与演绎验证相结合，我们可能能够更有效地验证tpm2-tss库中的复杂链表操作，并减少对交互式证明的依赖。

最后，本文还指出了一些值得进一步研究的方向，例如如何维护验证脚本以适应工具版本的变化，以及如何通过自动化生成验证脚本来提高验证效率。这些研究方向不仅对tpm2-tss库的验证具有重要意义，也可能为其他类似的正式验证项目提供有益的经验。通过不断改进验证工具和方法，我们相信未来的正式验证工作将更加高效和可靠，从而为安全关键系统的开发提供更强有力的支持。