Formal Analysis of Security Data Paths

One challenge with security in systems is to ensure that there are not backdoors, either accidentally or maliciously inserted. Intel, ARM and others have various forms of trusted execution technology. Under the hood these are implemented by dividing the design into two parts, normal and secure, and implementing them with physical separation on the chip. This is then connected up with a secure operating system so that a minimal secure OS runs on the secure part of the chip and a full-featured operating system runs on the normal part of the chip to deliver the main functionality of the system.

At the Haifa Verification Conference in Israel last month, Ziyad Hanna and Jamil Mazzawi of Jasper presented a paper on formal analysis of these types of design. The hardware is vulnerable if it turns out that secure areas can be accessed without going through the appropriate encryption protected paths. A modern SoC is very complex and contains a lot of IP that might not be very well understood by the designers. This creates unexpected paths to access secure areas. Additionally, test logic creates paths to the outputs (so that the design can be tested) which may themselves represent security vulnerability.

Today, people use ad hoc approaches to look at these issues and inspect them manually. This can only look at a small subset of the possible traces and there is no sense that the analysis is complete.

A better approach is to use formal techniques to specify the secure area(s) and illegal sources and destinations for the data. Waveforms from the formal tool will then show illegal propagations found. This can reduce analysis to weeks from months and exhaustively analyze all paths.

For example, perhaps there is a secure register that contains data that may not be accessed outside the secure area without first being encrypted (DRM keys perhaps). It is necessary to prove that there is no path to the system bus that bypasses the encryption block, and that there is no path in the other direction whereby the secure register can be directly over-written (see diagram).

The heart of the approach is path sensitization technology, which has a source signal and a destination signal. There is no SystemVerilog assertion equivalent for this property. To prove this property the data at the source of the path is tainted and then Jasper formally verifies if it is possible to cover tainted data at the destination, in which case a waveform shows how data can propagate from source to destination. Thus it identifies paths propagating data to and from secure areas through various forms of back-channel or unapproved route.

This approach can be used to verify requirements that are not accessible by regular SVA assertions and so therefore not possible with standard formal verification tools.

The slides from the presentation, which contains more detail and many more examples, are available from the Jasper website here.