Visible to the public Case Study: Discovering Hardware Trojans Based on Model Checking

TitleCase Study: Discovering Hardware Trojans Based on Model Checking
Publication TypeConference Paper
Year of Publication2018
AuthorsZhao, Jianfeng
Conference NameProceedings of the 8th International Conference on Communication and Network Security
Conference LocationNew York, NY, USA
ISBN Number978-1-4503-6567-3
Keywordscomposability, model checking, processor, pubcrawl, RTL level Hardware Trojan

Hardware Trojan may cause changes in system functions, system information leakage, and system damage or system paralysis. According to the hardware Trojan classification method, this paper discusses the hardware Trojan that belongs to the design stage, the behavior level description, the internal trigger, and it changes the function of processor, it is a hardware Trojan of combinational logic. The domestic and foreign research institutions put forward a variety of methods for the detection of hardware Trojans. In this paper, based on the open source processor OR1200 RTL source code, Aiming at a kind of hardware Trojan, which is composed of combinational logic trigger, one of the formal methods, the model checking technique, is used to detect the hardware Trojan. The experiment uses the open source EBMC model detection tool, uses the RTL source code as the model input, and uses SVA to describe the property input. The experimental results show that the model checking technique can be used as an effective hardware Trojan detection method.

Citation Keyzhao_case_2018