一种用于检测由无关转移触发的硬件木马的符号方法
符号计算
2021-11-09 v1
摘要
由于集成电路（IC）供应链的全球化，硬件木马及其触发攻击已成为重要的安全问题。一类硬件木马利用硬件设计有限状态机（FSM）中的无关转移（don't care transitions）。本文提出一种用于检测无关转移及隐藏木马的符号方法。我们的检测方法在 RTL 和门级均有效，不需要黄金设计，并分三个阶段进行。第一阶段探索可达状态。第二阶段执行近似分析以找出无关转移。第三阶段从具有传入无关转移的可达状态进行状态空间探索，以发现相对于第一阶段所观测结果的行为差异。我们还提出一种基于 FSM 状态可达性的剪枝技术。我们提出一种结合 RTL 与门级以保证正确性与效率的方法。具体而言，我们证明无关转移必须在门级（即综合完成后）进行检测以保证正确性；但在特定条件下，木马检测在 RTL 上可更高效。在使用来自 OpenCores 和 TrustHub 的基准集以及由两种综合工具 Yosys 和 Synopsis Design Compiler（SDC）生成的门级表示进行评估时，我们的方法在检测无关转移及利用它们的木马方面既高效（相较无剪枝最高 10 倍加速）又精确（0% 假阳性）。此外，当综合保留 FSM 结构且在 RTL 执行木马检测时，总分析时间可实现最高 3.40 倍（使用 Yosys）和 2.52 倍（SDC）的加速。
引用
@article{arxiv.2111.03989,
title = {A Symbolic Approach to Detecting Hardware Trojans Triggered by Don't Care Transitions},
author = {Ruochen Dai and Tuba Yavuz},
journal= {arXiv preprint arXiv:2111.03989},
year = {2021}
}