Evaluating the Effectiveness of Hardware Trojan Detection Approaches at RTL

The rapid advancements in semiconductor technol-ogy have fostered unprecedented innovation while simultane-ously increasing the risk of hardware Trojans (HTs)-malicious alterations introduced into integrated circuits (ICs) during de-sign or production. Despite extensive research on HT detection techniques, their practical implementation remains criti-cal for developing robust defenses. This paper quantitatively evaluates the effectiveness of three hardware design analysis techniques-bounded model checking, symbolic execution, and fuzzing - for detecting four types of HTs: combinational, sequential, input-based, and timing-based. We generate a HT benchmark set using a dynamic Trojan insertion framework, DTjRTL, which facilitates a systematic and comprehensive benchmarking process. This paper uses a variety of structural and semantic Trojan complexity metrics to evaluate the strengths and weaknesses of each of the hardware analyses techniques. Our findings show that there is no single technique that is effective for all HTs. Although, bounded model checking based techniques outperform other approaches for most HT types, they may be limited due to RTL features or the supported property specification syntax. We also find that among all the techniques, hardware fuzzing seems to be more sensitive to HT trigger complexity. Symbolic execution based techniques handle deep Timing-based Trojans in a scalable way when guided by fuzzing as an oracle towards suspicious parts of the design. Additionally, signal-dependent metrics have more impact on Trojan detection difficulty compared to the structural metrics.