San Diego-based startup Tortuga Logic has developed a toolkit for checking the security aspects of SoC hardware designs.
“What we really want to do is ensure that next-generation systems such as IoT devices are being built with security in mind, analyzing the RTL from the earliest stage and looking at the potential security problems,” said Tortuga cofounder and CEO Jason Oberg.
The checks look for potential sources of information leaks, with some similar in objective to those in Cadence Design Systems’ Security Path Verification App, part of the former Jasper Design Automation portfolio.
“One example is access-control issues that happen in a modern SoC. You may have a crypto core, A, storing keys. You want to make sure that another core, B, can’t access the data in that core,” Oberg said.
As well as access checks, the Tortuga Prospect tool builds in a number of higher-level analyses. “We have some key patents that cover specific certain types of attacks. One looks for [the possibility of] timing-based side-channel attacks,” Oberg added. “If you perform encryption using a key and it takes five cycles to process with one key but ten cycles for a different key, that has been shown to be exploitable.”
Timing-based attacks have been used against internet servers because, unlike other side-channel attacks based on heat or electromagnetic emissions, they can be performed without physical access. But in recent years, increasing processor performance has made it harder to distinguish timing variances when network jitter and the effects of multitasking are overlaid.
“When your system is very complex, you have a lot of variability which increases the difficulty of timing attacks. But as things are shrinking for the IoT, these are hardware heavy systems rather than software-intensive server farms. In that environment these types of attacks will manifest themselves again,” Oberg claimed.
“Also you want to make sure that a device responds always within a time window. Or that a secure core can’t affect the timing response of another core,” he added.
Formal and dynamic options
The Prospect tool is designed to use either formal or simulation-based techniques. “Our solution is not necessarily tied to formal, although we found a good partner in OneSpin to go down the formal route,” Oberg said.
“From what we have seen the use of formal depends on the properties. A lot of checks can span across the SoC and which formal might not handle because of capacity. Then there are properties where formal will work well because you don’t want to miss the corner cases.”
To check aspects of a design the team needs to define properties that the tool will apply to the RTL.
“A lot of the big semiconductor companies, they have security teams in place,” said Oberg. “They already have security requirements that they need to enforce. They specify a lot of these in a spreadsheet. They are already writing the properties. The [design and verification] engineers then use our tool to check the design.
“We have a specification language that we developed. It’s not SystemVerilog assertions; it’s our own language. It’s very high level so makes the requirements easy to write. At this stage, the language does look a lot like assertions but I think there are higher level descriptions possible. It’s done in terms of information flows.”
The team derived the Prospect tool from research into the security of information flows performed at the University of California at the San Diego and Santa Barbara sites. One result was the research language Caisson, although this is not used directly in Prospect.
“We were all doing research in this space for a long time,” said Oberg. “Of the four founders, Ryan [Kastner] and Tim [Sherwood] were the pioneers in this space. I did my PhD under Ryan. Jon [Jonathan Valamehr] under Tim at Santa Barbara.
“The ideas didn’t seem to have practicality at first. But, around 2010, industry started getting more interested in what we were doing. In 2013, we incorporated as we saw a good opportunity to bring the solution we were doing to an actual product.”