Keep The Wooden Horse Out Of Your Chip

The OneSpin’s Holiday Puzzle tradition has reached its fourth year: hear, hear! In December 2016, OneSpin challenged engineers to solve the Einstein riddle using assertions and a formal verification tool. In December 2017, the challenge was to model the hardest Sudoku in the world using assertions and find a solution with a formal tool. The OneSpin 2018-19 Holiday Puzzle asked engineers to design a digital circuit for computing Fibonacci numbers given a specification expressed in SystemVerilog Assertions.

This year, we decided to use the puzzle Spot the Wooden Horse to raise awareness on the risk of malicious logic being inserted in semiconductor IPs. To learn more about this topic, read my blog post “Hardware Trojans and the Problem of Trust in Integrated Circuits” or click here to download the OneSpin Trust and Security Solution flyer.

To check out the latest OneSpin Holiday Puzzle click here.

Challenge
We provided two RTL designs, uart-TrojanX and uart-TrojanY, inserted with hardware Trojans, but no specifications or any other information. We challenged engineers with three tasks:

• Achilles the Strong: detect the Trojans and provide waveform traces showing how they would get triggered.
• Paris the Judge: determine which design had stealthier Trojans.
• Helen the Mighty: provide additional comments, about how the Trojans could be detected automatically or made stealthier, for example.

The two designs had multiple suspicious code sections that were easy to identify with a code review. A particular sequence of values at the data input signal would cause a redundant register to toggle at every clock cycle, thus wasting power. A similar data sequence would activate logic corrupting the control function. It would be highly improbable to hit these data sequence scenarios by chance in IP constrained-random simulation verification or system-level tests.

Achilles the Strong
Most participants provided pictures of waveform traces activating a Trojan, generated through simulation tools, formal tools, or both. Some focused on only one Trojan, in most cases the power-wasting register. Given that design specifications were not available, no process could systematically detect all functional Trojans.

However, for specific IPs, this might be possible. OneSpin has a RISC-V Integrity Verification solution that has been successfully applied to several RISC-V cores. The solution includes a model of the RISC-V ISA expressed in SystemVerilog Assertions. Formal verification can prove that the RTL satisfies the assertions. A key strength of this solution is that the set of assertions is proven to be complete and free from gaps using OneSpin’s GapFreeVerification. Coverage metrics, mutation coverage, and code review can detect verification gaps. However, only GapFreeVerification can prove the absence of gaps. This ensures that the RISC-V model is complete and able to detect any RTL deviation, malicious or otherwise, from the RISC-V specification. A paper titled “Complete Formal Verification of RISC-V Processor IPs for Trojan-Free Trusted ICs” was presented at the GOMACTech 2019 conference. To obtain a copy, visit onespin.com/resources/white-papers.

For IPs that do not have an independent trust assurance solution, it is still possible to identify unusual and suspicious code patterns, known Trojan signatures, and weaknesses that could be exploited in implementation stages such as synthesis. A paper on this topic titled “An Automated Pre-Silicon IP Trustworthiness Assessment for Hardware Assurance”, authored by AEROSPACE Corporation and OneSpin engineers, will be presented at the GOMACTech 2020 conference. The paper is expected to be available on the OneSpin website from late March 2020.

Paris the Judge
There are no standard metrics or processes to assess how stealthy a Trojan is. It was interesting, though not surprising, to see that participants expressed many different opinions. Some engineers considered that the Trojan with the harder-to-reach triggering sequence was also harder to detect. This is certainly a valid point when using functional verification techniques, particularly constrained-random simulation, to detect IP deviations from the intended behavior. Things get more complicated if the Trojan has only a power-wasting payload. Others focused on how obfuscated the Trojan logic was, which is likely to be very relevant when code review is the primary trust assurance approach. Some engineers noted that a Trojan implemented using a dedicated FSM was probably easier to spot than one mixed up with a “genuine” FSM. Finally, as some Trojans were causing FSM deadlocks or signals getting stuck, it was also correct to observe that this might be easier to spot as these issues can be detected with automated formal checks. Ultimately, how stealthy a Trojan is will depend on the trust assurance process and technology available: a Trojan that is missed is stealthier than one that gets caught.

Helen the Mighty
Engineers love a good challenge. Participants contributed many interesting and valid ideas on how to make a Trojan stealthier or automate its detection. These are in effect the two sides of the same coin. Some basic ideas were to make the Trojan logic more obfuscated. One of the Trojans in our design included a register called my_power_wasting_reg. Everyone could think of a less obvious name. Making sure that the Trojan logic does not cause any deadlocks, dead code, or stuck-at signals, were other common ideas. Logic distributed across different files, and long latency Trojans, affecting the data output many cycles after being triggered, are ideas that also came up. Design and verification engineers know very well what type of corner-case behaviors are hard to detect, and how even advanced verification testbenches can be fooled if someone has malicious intentions.

Conclusion
Semiconductor IPs could contain hardware Trojans, and this risk can no longer be ignored, particularly for safety- and security-critical chips. Unfortunately, engineering talent could be used for nefarious purposes. As adversaries can go from smart individuals to nation-states, attacks to the IC supply chain could be sophisticated and supported by plenty of resources.

SoC integrators do not know the implementation details of the IPs they use, and they cannot afford to build a rigorous trust assurance environment from scratch. Automated trust assurance solutions that require low effort and no knowledge of the IP implementation details can be used to gain confidence that the IP is free from hidden, undocumented, or malicious logic.

I want to thank all participants for their interesting observations and comments. It was hard to pick winners, as many answers were similar or equally valid, but we made our best effort to make a fair decision. Finally, here are the winners:

• Nithin Kumar Guggilla of Xilinx wins the Achilles the Strong prize for providing waveforms using both formal and simulation tools (and commenting that it was much easier to use formal as the tool automatically creates the Trojan activation stimuli).
• Tero Kuusijärvi of NOKIA wins the Paris the Judge prize for considering that one of the Trojans in design uart-TrojanY was stealthier because it did not add a state (x_DataSend) to a control FSM.
• Wayne Yun of AMD wins the Helen the Mighty prize for providing a lot of valuable comments, many of which have been discussed in this blog post.

This year’s prizes are Bose SoundSport Free wireless headphones!

We are already busy looking for new ideas for the next Holiday Puzzle. Please send your suggestions to [email protected].

A big thank you to all the participants. Stay tuned for the next OneSpin Holiday Puzzle later this year!