Inter-IP Malicious Modification Detection through Static Information Flow Tracking
Zhaoxiang Liu1, Orlando Arias2, Weimin Fu1, Yier Jin2 and Xiaolong Guo1
1Kansas State University
2University of Florida
ABSTRACT
To help expand the usage of formal methods in the hardware security domain. We propose a static registertransfer level (RTL) security analysis framework and an electronic design automation (EDA) tool named If-Tracker to support the proposed framework. Through this framework, a data-flow model will be automatically extracted from the RTL description of the SoC. Information flow security properties will then be generated. The tool checks all possible inter-IP paths to verify whether any property violations exist. The effectiveness of the proposed framework is demonstrated on customized SoC designs using AMBA bus where malicious modifications are inserted across multiple IPs. Existing IP level security analysis tools cannot detect such Trojans. Compared to commercial formal tools such as Cadence JasperGold and Synopsys VC-Formal, our framework provides a much simpler user interface and can identify more types of malicious modifications.
Keywords: SoC Protection, AMBA Bus System, Hardware Trojan Detection, Formal Method.
