Static Gate-Level Information Flow for Hardware Information Security with Bounded Model Checking

Information flow security is an essential component of hardware security. Ensuring the confidentiality, integrity, and availability of data within hardware systems is critical to protect against unauthorized access, data breaches, tampering, and other security threats. Gate-level information flow technology can trace the flow of signals to detect malicious information flow and security vulnerabilities in the design. In this paper, we introduce a novel framework that combines GLIFT and bounded model checking to enable the static verification of information flow within hardware systems. This combination facilitates designers conducting exhaustive analysis, tracking of information flows and detecting potential security threats in their designs. When the design violates security policies, our framework provides a counterexample that assists designers in identifying malicious information flows in the hardware circuits. To demonstrate the efficiency of our framework, we conducted verification on hardware Trojan benchmarks from the Trust-hub. The results indicate that our verification framework is capable of detecting malicious information flows that exist in the designs.