HT-PGFV: Security-Aware Hardware Trojan Security Property Generation and Formal Security Verification Scheme

Property-driven hardware verification provides a promising way to uncover design vulnerabilities. However, developing security properties that check for highly concealed security vulnerabilities remains a significant challenge. In this paper, we propose a scheme, called HT-PGFV, to implement hardware Trojan security property assertion automatic generation and formal security verification for Trojan-infected designs. In our scheme, we develop a hardware Trojan security property assertion generation method for automated hardware which can extract hardware Trojan security properties from Trojan-infected designs by performing the three main steps of Trojan-infected signal identification based on feature matching, influence-cone-analysis-based Trojan path identification, and information flow trace mining, and formulate them as SystemVerilog assertions. In addition, we develop a formal security verification method based on information flow analysis which can formally verify hardware Trojan security properties and detect hardware Trojans violating information flow security policies by checking the security of information flows via our developed RT-level hardware information flow security models. The proposed method is demonstrated on several Trojan benchmarks from Trust-Hub. Experimental results show that our scheme can generate hardware Trojan security property assertions for Trojan-infected designs and detect information leakage and functionality change hardware Trojans activated by external inputs or internal conditions.