An Automatic Extraction and Verification Method of Security Properties for Integrated Circuit Design

Formal verification methods can prove whether a integrated circuit(IC) design satisfies desired properties with higher verification efficiency than traditional testing methods. However, it requires manual specification of assertion properties for circuit design, where the quality and completeness of properties are difficult to guarantee. In this work, we propose an automatic extraction and verification method for typical security properties of integrated circuit design based on information flow analysis. An information flow model is constructed for the integrated circuit design. Then, the simulation trajectory of the model is further analyzed to identify information flow behaviors related to confidentiality and integrity. These behaviors are described as information flow security properties. The Yosys verification tool is used to formally verify the extracted information flow properties using its Boolean satisfiability problem (SAT) solver. The results of formal verification can demonstrate that the design satisfies the properties, or in case of property verification failures, quickly locate design vulnerabilities from counterexamples provided by the verification tool. This method facilitates subsequent analysis or vulnerability code refactoring for verification personnel.