LAUSR

A hardware Trojan (HT) is a malicious modification of the design done by a rogue employee or a malicious foundry to leak secret information, create a backdoor for attackers, alter functionality, degrade performance and even halt the system. In Black-hat high-level synthesis (HLS) (Pilato et al., 2019), the authors have introduced a possibility of HTs insertion in the register transfer level (RTL) design by the HLS tool itself. Specifically, degradation attack (DA), battery exhaustion (BE) attack, and downgrade attack (DG) have been proposed in that work. In this study, we show how all three HTs inserted by Pilato et al. (2019) can be detected using a C-to-RTL equivalence checking framework. We have assumed that both the input C code and the Trojan-infected RTL code are available for our analysis. Specifically, our framework extracts an RTL-level finite-state machine with datapaths (RTL-FSMDs) from the HLS-generated RTL. During finite-state machine with datapath (FSMD) construction, a BE attack can be identified. Our proposed method then compares the FSMD of the input C code with the RTL-FSMD to identify the DA and the DG. The experimental results confirm the detection of HTs of the black-hat HLS tool.