Presentation
FastPath: A Hybrid Approach for Efficient Hardware Security Verification
SessionOf Circuits and Secrets: Emerging Hardware Security Primitives and Cryptographic Accelerators
DescriptionIn response to the surge of security breaches in hardware designs, many verification methods have been proposed to detect microarchitectural information leakage. These sophisticated efforts have gone a long way toward preventing attackers from breaking the confidentiality of the system. However, each approach comes with its own set of weaknesses: it may not be
scalable enough, it may not be exhaustive, it may not be flexible enough to meet changing requirements, or it may not fit well
into existing verification flows.
In this paper, we propose FastPath, a hybrid verification methodology that leverages the strengths of different approaches while compensating their weaknesses. In particular, it combines the efficiency of simulation with the exhaustive nature of formal verification. In addition, FastPath employs a structural analysis framework to automate the method further. Our experimental results compare FastPath to a state-of-the-art formal approach, showing a significant reduction in manual effort while achieving the same level of exhaustive confidence. We also discovered and contributed a fix for a previously unknown leak of internal operands in cv32e40s, a RISC-V processor intended for security applications.
scalable enough, it may not be exhaustive, it may not be flexible enough to meet changing requirements, or it may not fit well
into existing verification flows.
In this paper, we propose FastPath, a hybrid verification methodology that leverages the strengths of different approaches while compensating their weaknesses. In particular, it combines the efficiency of simulation with the exhaustive nature of formal verification. In addition, FastPath employs a structural analysis framework to automate the method further. Our experimental results compare FastPath to a state-of-the-art formal approach, showing a significant reduction in manual effort while achieving the same level of exhaustive confidence. We also discovered and contributed a fix for a previously unknown leak of internal operands in cv32e40s, a RISC-V processor intended for security applications.
Event Type
Research Manuscript
TimeWednesday, June 252:00pm - 2:15pm PDT
Location3008, Level 3
Security
SEC2: Hardware Security: Primitives & Architecture, Design & Test