Biblio

The design of modern computer hardware heavily relies on third-party intellectual property (IP) cores, which may contain malicious hardware Trojans that could be exploited by an adversary to leak secret information or take control of the system. Existing hardware Trojan detection methods either require a golden reference design for comparison or extensive functional testing to identify suspicious signals. In this paper, we propose a new formal verification method to verify the security of hardware designs. The proposed solution formalizes fine grained gate level information flow model for proving security properties of hardware designs in the Coq theorem prover environment. Compare with existing register transfer level (RTL) information flow security models, our model only needs to translate a small number of logic primitives to their formal representations without the need of supporting the rich RTL HDL semantics or dealing with complex conditional branch or loop structures. As a result, a gate level information flow model can be created at much lower complexity while achieving significantly higher precision in modeling the security behavior of hardware designs. We use the AES-T1700 benchmark from Trust-HUB to demonstrate the effectiveness of our solution. Experimental results show that our method can detect and pinpoint the Trojan.

Secure hardware design is a challenging task that goes far beyond ensuring functional correctness. Important design properties such as non-interference cannot be verified on functional circuit models due to the lack of essential information (e.g., sensitivity level) for reasoning about security. Hardware information flow tracking (IFT) techniques associate data objects in the hardware design with sensitivity labels for modeling security-related behaviors. They allow the designer to test and verify security properties related to confidentiality, integrity, and logical side channels. However, precisely accounting for each bit of information flow at the hardware level can be expensive. In this work, we focus on the precision of the IFT logic. The key idea is to selectively introduce only one sided errors (false positives); these provide a conservative and safe information flow response while reducing the complexity of the security logic. We investigate the effect of logic synthesis on the quality and complexity of hardware IFT and reveal how different logic synthesis optimizations affect the amount of false positives and design overheads of IFT logic. We propose novel techniques to further simplify the IFT logic while adding no, or only a minimum number of, false positives. Additionally, we provide a solution to quantitatively introduce false positives in order to accelerate information flow security verification. Experimental results using IWLS benchmarks show that our method can reduce complexity of GLIFT by 14.47% while adding 0.20% of false positives on average. By quantitatively introducing false positives, we can achieve up to a 55.72% speedup in verification time.