Hierarchy-Preserving Formal Verification Methods for Pre-silicon Security Assurance

The wide usage of hardware intellectual property (IP) cores from untrusted vendors has raised security concerns in the integrated circuit (IC) industry. Existing testing methods are designed to validate the functionality of the hardware IP cores. These methods often fall short in detecting unspecified (often malicious) logic. Formal methods, on the other hand, can help eliminate hardware Trojans and/or design backdoors by formally proving security properties on soft IP cores despite the high proof development cost. To alleviate the computation burden, we propose a new hierarchy-preserving formal verification (HiFV) framework for circuit trust evaluation at the pre-silicon stage. This framework is derived from the Proof-Carrying Hardware (PCH) and is dedicated for security property verification of System-on-Chip (SoC) platforms, where third-party soft IPs are integrated as sub-modules. The key novelty lies in the improvement of the proof construction process of the previously developed security property verification framework, so that the framework can support building theorem proofs in a hierarchical way. We assume a trusted third-party verification house exists, which can use the proposed framework for security theorem construction and proof writing. The applicability of the proposed framework is demonstrated by formally verifying the memory integrity property on an 8051 microprocessor whose sub-modules were treated as untrusted third-party IPs.