Security Path Verification

Formal approaches and security are a perfect match since you really want to prove that there are no holes in your security, rather than just being fairly confident. At the recent Jasper User Group meeting, Victor Purri presented some case studies in security verification.

The Jasper Security Path Verification (SPV) App is used to prove properties about the paths to secured data. For example,

• Data in secure area must not be visible by CPU if it is not in secure mode
• Secure register must not be written by non-secure agent

Usually data propagation requirements can usually be translated into one of these questions:

• Can data on secure location A propagate to non-secure location B?
• Can data on non-secure location X propagate to secure location Y?

In both cases we want the answer to be no, but it can be very hard to perform good verification without proper tools. Structural analysis can be very ad-hoc. Simulation depends on how good the verification engineer is at breaking the security. And standard formal verification is not a good fit since it is hard to describe the requirements as SVA/PSL assertions.

The SPV App is used specifically to address this need. The user specifies paths where data propatation should not occur and then the SPV App will act as a hacker and try and illegally overwrite secure data, or illegally leak secure data. This approach is exhaustive, efficient and correct.

The tool uses Jasper’s path sensitization technology. The tool inserts a unique tag, the taint, at the source and checks if it can appear in the destination’s signal. If so, then there is a path and a security violation.

One example Victor presented was that of a secure microcontroller which contains an encryption key. We want to make sure that it is not possible for the key to be leaked from the microcontroller. SPV proves that only the “key match” signal can be influenced by the key (and so it cannot be leaked that way). But that is not good enough, since we also need to check that the key match signal is correctly implemented. JasperGold inserts malicious instructions and finds a problem. A big one.

Note that the problem is not that our RTL is wrongly implemented, it is a hole in our overall security architecture. We need to extend the microprocessor architecture with an additional bit to tag instructions to indicate whether instructions are secure or non-secure.

SPV App is still an evolving methodology. The new tool ha a graph viewer and reachability analysis. In the future there will be support for bigger designs, different access interfaces and different security features.

There is more in the presentation. If you are a Jasper user (not necessarily one who attended JUG) then you can download the presentations, including this one, here.

More articles by Paul McLellan…