Can the NSA Get Into Your Chip?

At DVCon Lawrence Loh and Viktor Markus Purri gave a tutorial on Formally Verifying Security Aspects of SoC Designs. Lawrence is the direector of WW application engineering and Markus is an FAE who specializes in security verification.

I’m not going to attempt to summarize an entire half-day tutorial in under 1000 words, but here is the big picture story.

To motivate the importance of security, they started with some events from the press.

• Automotive: At the upcoming Black Hat Asia 2014 conference, a pair of Spanish security researchers will demonstrate a smartphone-sized circuit board dubbed the ‘CAN Hacking Tool’ (CHT), which they claim will let them remotely take partial control of many vehicles over a wireless Bluetooth connection.”
• Medical: In two weeks of work [a researcher from McAfee] found a way to scan for and compromise insulin pumps that communicate wirelessly. … ‘We can influence any pump within a 300ft [91m] range.’”
• Consumer Electronics: After its Playstation network was shut down by LulzSec, Sony reportedly lost almost $171 million. The hack affected 77 million accounts and is still considered the worst gaming community data breach ever. Attackers stole valuable information: full names, logins, passwords, e-mails, home addresses, purchase history, and credit card numbers.”

A lot of security is going to be implemented in software, but if it is not built on a secure hardware base then it won’t be security. After all, security is like a chain, only as strong as its weakest link. Hardware architectures are emerging to deal with secure information, such as ARM Trustzone. But just by looking at the diagram below with some secure links and some insecure, it is clear that it isn’t clear if it is secure!

The security provisions come down to two simple propositions when you look at a block with inputs and outputs:

• can the secure information appear at the outputs (e.g. steal the keys)
• can the inputs be used to overwrite the secure information (e/g/ change the keys)

There are a number of manual approaches that can be used with regular formal verification to do this, but they are tricky and error prone to set up. For example, all the input might be sensitized with one value and a different value in the secure registers. Then prove that the output can only be the sensitized value and not the secure value.

Jasper’s Security Path Verification App is a completely automated approach to this problem. Since it is formal it can identify unintended paths exhaustively. Anyone can build a security system that they themselves cannot break, it is a common pitfall in security. But this proves that it cannot be broken.

The App takes as inputs the RTL and a list of undesired paths to be verified. The App does everything automatically from there to derive and generate all the properties. The output are counter-examples that show undesired data propagation (if there is any).

The App uses Jasper’s path sensitization technology. Internally the tool inserts a unique tag called the taint. It then checks where the taint can propagate to in the design. If the taint goes from the input and makes it to the output then there is a path through the design.

The tutorial contained lots of case studies, ranging from making sure that device registers could not be used to gain unauthorized access, or scan chains to read a secure memory, or that a secure microprocessor really was secure (it wasn’t).

There are a couple of white papers on the security App on the white paper page here. There is no video of the whole tutorial as far as I know.

More articles by Paul McLellan…

<script type="IN/Share" data