检测由"Don't Care Transitions"触发的硬件木马的符号化方法
摘要：硬件设计中使用的有限状态机中可能存在不关心的过渡，黑客可以利用这种过渡来植入硬件木马。本文提出了一种符号化的方法来检测不关心的过渡和隐藏的硬件木马。我们的检测方法在RTL和门级电路两个层次都可以工作，并且不需要一个黄金设计。具体而言，我们的方法包括三个阶段：第一阶段是探索可达状态，第二阶段是进行近似分析来找出不关心的过渡，第三阶段是从具有输入不关心过渡的可达状态进行状态空间探索，以找出与第一阶段观察到的行为差异。我们还提出了一种基于状态可达性的剪枝技术。我们展示了一种既利用RTL又利用门级电路的方法，以提高验证的准确性和效率。具体而言，我们发现不关心的过渡必须在门级电路中进行检测，即在综合之后进行。然而，在特定条件下，可以在RTL级别更高效地进行木马检测。我们在OpenCores和TrustHub提供的一组基准测试中，使用Yosys和Synopsis Design Compiler（SDC）生成的门级表示进行评估，结果表明我们的方法在检测不关心的过渡和利用不关心的过渡的木马方面，既高效（相对于不进行剪枝可以提高10倍的速度）又准确（0%的假阳性）。此外，当综合保留了FSM结构并且木马检测在RTL级别进行时，总体分析时间可以实现3.40倍（使用Yosys）和2.52倍（SDC）的加速。
作者：Ruochen Dai and Tuba Yavuz
论文ID：2111.03989
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2021-11-09