ASAX: Automatic security assertion extraction for detecting Hardware Trojans
Chenguang Wang, Yici Cai, Qiang Zhou, Haoyi Wang · 2018 23rd Asia and South Pacific Design Automation Conference (ASP-DAC) · 2018
Hardware Trojans (HT) has been one of the major concerns of IC designers, and formal methods have been applied to the HT detection. In general, the assertions for detecting HT are manually defined, which is time-consuming and error-prone even for an expert engineer. However, there is a lack of studies on the automatic definition for security assertions. To fill in this gap, we propose an automatic security assertion extraction (ASAX) tool. ASAX labels the candidate signals and infers the proposed register transfer level (RTL) invariants from simulation traces. Next, the security assertions are mined from the inferred RTL invariants. By adopting a two-step invariants inferring technique, ASAX can extract high-coverage assertions with a low runtime. We validate the effectiveness and efficiency of ASAX through experiments on the benchmarks from Trust-hub, DeTrust and OpenCores. The results show that the HT can be 100% detected by model checking with the extracted security assertions.