针对硬件木马的形式化验证模型构造方法.docx

《针对硬件木马的形式化验证模型构造方法》 硬件安全在当前集成电路领域中扮演着至关重要的角色，尤其是硬件木马的出现，它们可能对电路的保密性、完整性和有效性构成严重威胁。硬件木马一旦植入，可能导致系统安全问题、经济损失甚至人身伤害，如2010年的Stuxnet蠕虫事件就是一例。为了应对这一挑战，形式化验证成为了一种有效的方法，它以算法为基础，提供更全面的验证，尽管耗时较长。 形式化验证主要包括定理证明和模型检测两种技术。定理证明利用数学逻辑验证Verilog代码的安全性，如JIN等人的工作；而模型检测则通过穷举状态空间来验证电路属性，这种方法速度快，且能产生反例帮助理解验证失败的原因。在硬件验证领域，既有针对门级网表的建模方法，也有针对寄存器传输级（RTL）的验证策略。然而，门级建模复杂度高，影响验证效率，相比之下，RTL设计更为简洁。 针对这一问题，文献[8]提出将RTL的Verilog代码转化为C语言代码进行模型检测，但C语言缺乏时序特性，可能导致等价性问题。另一工具Verilog2SMV扩展了Yosys，将Verilog代码转换为SMV模型以供NuXMV验证，但模型的可读性和可重用性有限。因此，提出了一个自动构造形式化验证模型的新方法。 该方法首先生成每个变量的路径条件和表达式对，确定约束关系，然后利用这些对构建Kripke结构的状态转移关系，形成RTL的验证模型。通过定义安全验证属性，使用NuSMV进行符号模型检测，遍历状态空间以查找硬件木马。当验证失败时，反例将揭露硬件木马或其触发器。 实验运用标准测试集Trust-HUB进行验证，利用有限状态机的Kripke结构模型和符号模型检测的优化技术（如有序二元决策图OBDD）提高验证效率。在开始形式化验证前，设计应先通过基本的功能测试，以减少整体验证时间。整个流程如图1所示，首先通过深度优先遍历Verilog设计的控制流图生成路径条件，然后构建形式化验证模型，最终进行模型检测。 总的来说，该方法提供了一种自动化构建形式化验证模型的途径，旨在检测那些仿真测试难以发现的硬件木马，提高验证的准确性和效率，为硬件安全提供了有力保障。