Jasper SPV App
Key Benefits
- Proves with mathematical certainty that secure data remains secure
- Provides, when needed, a detailed waveform of exactly how the design can be compromised
- Scales to analyze large designs
Developed with unique path sensitization technology, the Cadence® Jasper™ Security Path Verification (SPV) App is a formal verification product that accepts register-transfer level (RTL) containing a specific secure area (memory or registers), and exhaustively proves that secure data:
- Can’t be read illegally (no leaks)
- Can’t be illegally overwritten (sanctity)
- Remains secure in the face of faults or failure
Most modern SoCs handle some form of sensitive information on-board: credit card numbers, private encryption keys, device identifiers, serial numbers, sensitive healthcare or military information, etc. If this hardware is not secure, then layers of firmware and application software will be unwittingly vulnerable, too.
Unfortunately, verification of hardware designed to store such information securely cannot be done with dynamic methods like simulation/emulation because activation of any security bugs via simulation depends on the “hacking” ability of the verification engineer. Manual review of the RTL is time-consuming and error-prone, and/or does not scale no matter how experienced the reviewer.
Unlike attempting to use regular formal tools for this type of verification, the Jasper SPV App provides unique path sensitization technology to detect security issues that cannot be found by any other method. Using the app, you specify a secure area and illegal sources and destinations for the data, and the app uses the path-sensitization technology to check against three classes of violations:
- No data leaks: Secure data cannot be read illegally
- Data sanctity: Secure data cannot be overwritten illegally
- Fault tolerance: Secure data remains secure in the face of faults, failures, and deliberate tampering
The path-sensitization technology finds all paths propagating data to and from secure areas. The Jasper SPV App captures requirements that are not expressible by regular SystemVerilog Assertions (SVA) and, therefore, not possible to verify with standard formal tools.
Key Features
- Special black-boxing features enable scalability to bigger designs
- Ability to model cases of deliberate tampering by hackers and thus, verify whether the design is robust enough to resist certain attacks
- Customized user interface that expedites security-specific debug and analysis
-
Jasper RTL Apps
- Jasper FPV App
- Jasper Sequential Equivalence Checking App
- Jasper Design Coverage Verification App
- Jasper Coverage Unreachability App
- Jasper X-Propagation Verification App
- Jasper Control and Status Register App
- Jasper Connectivity Verification App
- Jasper Superlint App
- Jasper Behavioral Property Synthesis App
- Jasper Low-Power Verification App
- Jasper Security Path Verification App
- Jasper Clock Domain Crossing App
- Assertion-Based Verification IP
- Jasper FSV App