How Secure Is Your Design?

Once upon a time, secure hardware was only needed for mil-aero and banking systems. Today, numerous industrial and consumer applications require special hardware to protect data required for digital rights management, electronic wallets, private encryption keys, or medical information.

Current methodologies to verify that such hardware is impervious to attack and/or the data within remains secure are essentially ad hoc approaches tacked-on to the overall verification that’s part of IP design, SoC integration, system validation, and software development. The main methodology is to fire a battery of constrained-random simulations that attempt to hit all possible security leakage scenarios. Granted this technique scales with simulation capacity, but it is not exhaustive. Inevitably many corner cases are left unchecked, leaving open pathways for attackers. Put another way, verifying these systems cannot be exhaustively done with dynamic methods such as simulation/emulation, because activation of any security bugs via simulation depends on the “hacking” ability of the verification engineer. Bottom-line: Although protecting your device from unauthorized access is critical, verifying whether secure information can be leaked is impossible to achieve with conventional RTL validation methods.

With RTL validation methods ruled out, the exhaustive nature of formal analysis remains an obvious candidate. However, security requirements are not easily expressible by regular SVA assertions. In a nutshell, an assertion would have to be written for each potential path – a situation that essentially mirrors the challenge of writing enough constrained-random tests. Thus, it is not practical to achieve security validation closure with standard formal verification tools.

Recognizing this apparent catch-22, Jasper has developed a Security Path Verification App (SPV) with special formal technologies, engines, and an optimized user workflow to tackle the security verification challenge. Specifically, with SPV it is convenient to specify the security paths and perform an exhaustive verification based on our special path sensitization technology, automatic connectivity abstraction, path divide-and-conquer search, and by leveraging the comprehensive core formal engines and usability features of the JasperGold platform. In short, SPV provides a comprehensive solution to the security path verification problem.

One note on methodology: the major focus of security verification that we see relies on verifying the correctness of encryption algorithms and their implementation in software and hardware. In contrast, Jasper’s SPV addresses a specific, often overlooked aspect of security verification by formally proving that attackers cannot breach the hardware authentication logic and registers, and/or read or alter the secure data through illegal logic paths.

The SPV app is in active use by various customers in the SoC domain. To learn more about the type of verification these customers are doing, download the Jasper white paper on Security Path Verification. Additionally, earlier this year Ziyad Hanna of Jasper R&D published the following case study on formally verifying secure on-chip datapaths in John Cooley’s “DeepChip” website, in bulletin ESNUG 524, item 3.