1.3　形式化验证

除了电路级保护方法，形式化验证也被广泛应用于流片前的功能和安全性验证。在各种形式化验证中，定理证明是一种有代表性的解决方案，可以为底层设计提供高水平的保护。但这种解决方案计算复杂度高，证明过程繁琐，缺乏自动化工具。本节将介绍基于硬件IP核的携带证明硬件（proof carrying hardware，PCH）框架[58]、基于SAT求解器的形式化验证方法，并可用于IP可信性验证。

1.3.1　基于硬件IP核的携带证明硬件框架

基于硬件IP核的携带证明硬件（PCH）框架是确保硬件可靠性的一种方法[24,25,59,60]。PCH方法的灵感来自G.Necula[61]提出的携带证明代码（proof-carrying code，PCC）。不可信的软件开发人员及供应商使用PCC机制为软件客户认证所开发的软件代码。在认证过程中，软件供应商向软件客户给出所提供的安全策略的安全证明和PCC二进制文件，包括对安全性质的形式化证明。通过在证明检查器中快速验证PCC二进制文件，软件客户可确保软件代码的安全性。由于该方法可有效缩短软件客户的验证时间，因此在不同场合得到了广泛使用。尽管拥有这些优点，PCC方法仍需要一个庞大的可信计算基础（TCB）。FPCC（基础性PCC）克服了PCC的局限性，使用基础逻辑表示不同汇编语言指令的操作语义，并在逻辑框架中实现逻辑[62,63,64]。然而，FPCC方法增加了证明的开发工作量。随后，研究者开发了验证汇编程序（certified assembly programming, CAP）语言。该语言使用霍尔逻辑风格的推理构造证明[65,66]。

在文献[24,60]中，论文的作者根据PCC框架的概念，提出了一种用于动态可重构硬件平台的携带证明硬件PCH。其实现方法的核心理念是在硬件运行时利用可重构平台在设计规范和设计实现之间进行组合等价性检查[60]。该方法虽然被命名为PCH，但实际上是一种基于SAT求解器的组合等价性检查。在PCH框架中，应用的安全策略与安全属性并无关联。相反，FPGA比特流（bitstream）提供商和IP用户一致同意的安全策略是确保双方遵循相同的比特流格式、表示组合函数的合取范式以及用于证明构造和验证的命题演算。随后在文献[67]中，研究者对硬件可编程平台上基于SAT求解器的验证携带框架进行了更详细的介绍。在文献[23]中，研究者阐述了硬件信任与威胁模型及实验设置。尽管这些研究者表示，基于其他安全特性，PCH概念具有更多的潜在应用，但所提出的范例仍依赖于运行时组合等价性检查，以检查规范和实现之间的功能等价性。

除了保护综合后FPGA比特流，研究者也希望能用携带证明方法来保护综合前的RTL设计。在文献[25，59]中，研究者在CAP的构建和应用基础上，开发了一种新的PCH框架。与FPCC和CAP框架类似，这种新型PCH框架使用Coq函数语言进行验证构造，并利用Coq平台进行自动验证[68]。Coq平台的使用确保了IP供应商和IP用户实现相同的演绎规则，有助于简化验证过程。然而，Coq平台无法直接识别硬件描述语言。为解决这一问题，研究者提出了一种形式化的时序逻辑模型来表示Coq环境下的硬件电路。研究者还开发了转换规则，以帮助将商用IP核从HDL代码转换为基于Coq的形式逻辑，在此基础上构造安全性定理及其证明[25]。基于这种PCH框架，研究者提出了一种新的可信IP获取和传输协议[58]。从这一框架中，IP用户先向IP供应商提供功能规范和安全属性集，然后IP供应商将根据功能规范准备HDL代码，再将HDL代码转换为形式化表示，以方便生成安全定理并构造证明。HDL代码和形式化定理证明组成可信包。接收到可信包后，IP用户将使用相同的转换规则生成形式化的电路表示。转换后的代码将与形式定理和证明一起加载到证明检查器中。通过一个自动的属性检查过程，IP用户可以快速验证IP核的安全属性以确定其可信度。由于计算工作量从IP用户转移到IP供应商，因此PCH框架成为一种非常具有吸引力的可信IP验证方法。此外，由于自动验证检查过程迅速，IP用户可以在每次使用设计时检查IP核的安全性。这样，即使是内部攻击者，也很难在设计中插入恶意逻辑。

在文献[25]定义的PCH框架中，安全属性集是最重要的组件。一组完整的安全属性将通过检测IP核是否存在恶意逻辑来增强IP核的可信度。然而，PCH方法和文献[25]提出的可信IP交付过程没有为单个设计指定安全属性的详细信息。由于不同的硬件IP核通常共享相似的安全属性，因此为降低PCH框架的设计成本并重用先前开发的定理证明，以集中方式管理不同类型安全属性的属性库将是一种理想的解决方案。任何给定的硬件设计都可以从属性库中选择特定的安全属性集，无需从头开始开发所有属性。所选属性集可以加大许多攻击模式的实现难度，并确保交付IP核的可靠性。安全属性库可根据需要进行扩展，以保护IP核免受不同类型的硬件木马攻击。作为构建安全属性库的第一步，数据安全属性被选为大多数硬件IP核的主要属性[20,26]。数据安全属性的核心思想是跟踪内部信息流，并借助PCH框架，形式化证明没有敏感信息通过主输出或木马侧信道泄露。开发完整的安全属性库仍是一个正在研究的热门课题。

除RTL代码信任验证外，基于携带证明的信息保证方案也被用于支持门级电路网表，在很大程度上扩展了携带证明硬件在IP保护中的应用范围[69]。利用新的门级框架，文献[69]对可测试性设计（design for test, DFT）扫描链的安全性和制造芯片的工业标准测试方法进行了形式化分析，证明插入扫描链的电路会违反数据保密属性。随着各种攻击和防御方法的发展，数十年来，研究者一直研究由DFT扫描链引起的安全问题[70-78]，但文献[69]首次以形式化证明的方式论证由扫描链带来的安全漏洞（注意，RTL验证方法很少能够触及扫描链，因为扫描链是在网表阶段才被插入的）。同样的框架也被应用于内建自测试（built-in-self-test，BIST）结构，证明BIST结构也可以泄露内部敏感信息。

1.3.2　基于SAT求解器的形式化验证方法

除了携带证明方法，SAT求解器还用于RTL代码的安全验证。例如，文献[54]提出在第三方IP中过滤和定位可疑逻辑的四大步骤。第一步，使用由顺序自动测试模式生成（automatic test pattern generation，ATPG）的功能向量删除易检测信号。第二步，使用全扫描N-检测ATPG识别难以激发或传播的信号，缩小可疑信号的范围，识别与硬件木马相关的逻辑电路。第三步，使用SAT求解器对含有极少触发信号的可疑网表与表现出正确行为的电路网表进行等价性检验。最后一步，使用可疑信号列表中的区域隔离方法来确定电路中一系列不可测试的门。文献[79]提出了一种多阶段的可疑信号识别方法，包括基于断言的验证、代码覆盖率分析、冗余电路去除、等价性分析和时序ATPG的使用。这种多阶段方法在较小规模的RS232电路中得到了验证，检测硬件木马信号的效率达67.7%～100%。