AGILE: Automated Assertion Generation to Detect Information Leakage Vulnerabilities

The globalization of the System-on-Chip (SoC) design process has made hardware designs prone to many security vulnerabilities. One of the most critical security vulnerabilities is information leakage (IL), which allows an attacker to gain access to a design's secret information. IL vulnerabilities can result from unintended design flaws or the intentional insertion of malicious functionality into the design. Such vulnerabilities should be identified at the early design stages to secure a hardware design. Property-driven security verification has emerged as a promising method of verifying that such security vulnerabilities do not exist. This verification technique requires developing an appropriate set of assertions to formally represent the properties. However, forming a comprehensive set of assertions that can cover all potential vulnerabilities in design is challenging. Assertion generation cannot be done manually due to the large complexity of designs, lack of security experts as well as the existence of untrusted observable points in the design. In this work, we propose AGILE, a framework to automatically generate security assertions for property-driven verification to identify IL-based vulnerabilities. The experimental results show that the assertions provided by AGILE can detect both intentional and unintentional IL paths in the input design. We demonstrate the effectiveness of AGILE on the NIST standard, Trust-Hub, and OpenCores benchmarks. Moreover, we use code coverage analysis to evaluate the accessibility of the generated assertions to the source code. The analytical result indicates that by utilizing the assertions generated by AGILE, security coverage of the design under verification (DUV) can be improved significantly.