A Golden-Free Formal Method for Trojan Detection in Non-Interfering Accelerators
CoRR(2023)
摘要
The threat of hardware Trojans (HTs) in security-critical IPs like
cryptographic accelerators poses severe security risks. The HT detection
methods available today mostly rely on golden models and detailed circuit
specifications. Often they are specific to certain HT payload types, making
pre-silicon verification difficult and leading to security gaps. We propose a
novel formal verification method for HT detection in non-interfering
accelerators at the Register Transfer Level (RTL), employing standard formal
property checking. Our method guarantees the exhaustive detection of any
sequential HT independently of its payload behavior, including physical side
channels. It does not require a golden model or a functional specification of
the design. The experimental results demonstrate efficient and effective
detection of all sequential HTs in accelerators available on Trust-Hub,
including those with complex triggers and payloads.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要