| Title | ArtiFact: Architecture and CAD Flow for Efficient Formal Verification of SoC Security Policies |
| Publication Type | Conference Paper |
| Year of Publication | 2018 |
| Authors | Deb Nath, Atul Prasad, Bhunia, Swarup, Ray, Sandip |
| Conference Name | 2018 IEEE Computer Society Annual Symposium on VLSI (ISVLSI) |
| Keywords | alternative architecture, ArtiFact, CAD, CAD flow, centralized infrastructure IP, complex steps, Complexity theory, critical steps, cryptography, efficient formal verification, Engines, expensive steps, flexible infrastructure IP, formal verification, functional design flow, illustrative policies, industrial SoC, integrated circuit design, IP networks, modern SoC design validation, Monitoring, off-the-shelf formal tools, policy-based governance, pubcrawl, security architecture, Security Engine, security of data, Security Policies Analysis, security policy, security policy implementation, simulation-based security verification, SoC Security, SoC security policies, SoC Verification, streamlined verification, system-level security policies, system-on-chip, Tools, verification time, verification tools |
| Abstract | Verification of security policies represents one of the most critical, complex, and expensive steps of modern SoC design validation. SoC security policies are typically implemented as part of functional design flow, with a diverse set of protection mechanisms sprinkled across various IP blocks. An obvious upshot is that their verification requires comprehension and analysis of the entire system, representing a scalability bottleneck for verification tools. The scale and complexity of industrial SoC is far beyond the analysis capacity of state-of-the-art formal tools; even simulation-based security verification is severely limited in effectiveness because of the need to exercise subtle corner-cases across the entire system. We address this challenge by developing a novel security architecture that accounts for verification needs from the ground up. Our framework, ArtiFact, provides an alternative architecture for security policy implementation that exploits a flexible, centralized, infrastructure IP and enables scalable, streamlined verification of these policies. With our architecture, verification of system-level security policies reduces to analysis of this single IP and its interfaces, enabling off-the-shelf formal tools to successfully verify these policies. We introduce a CAD flow that supports both formal and dynamic (simulation-based) verification, and is built on top of such off-the-shelf tools. Our approach reduces verification time by over 62X and bug detection time by 34X for illustrative policies. |
| DOI | 10.1109/ISVLSI.2018.00081 |
| Citation Key | deb_nath_artifact:_2018 |
ArtiFact: Architecture and CAD Flow for Efficient Formal Verification of SoC Security Policies