Security breaches in modern computing systems have been emerging at an alarming rate in recent years. Reports about cyber-attacks make the headlines all too often and cause growing concerns in a society that depends increasingly on digital infrastructures. While vulnerabilities of the software are an important and frequent cause of security violations, more recently, also the hardware has received increased attention. Designers of Systems-on-Chip (SoCs) tend to integrate more and more security-specific HW features, such as HW-based stack protection, memory encryption, cryptographic engines and trusted execution environments.

Yet, as reported by numerous sources, also these sophisticated HW security barriers can be overcome by clever attackers. This was impressively demonstrated by the famous Spectre and Meltdown attacks which caused world-wide headlines in 2018. But also other types of microarchitectural side channels, such as cache-based side channels, in spite of being known for many years, continue to grow into more power­ful attacks and pose a threat in security-critical applications. Poorly understood HW weak­nesses can compromise any attempt to develop so called “data-oblivious” SW and may undermine the sec­urity architecture of the entire SW stack. In addition, due to the increasing complexity of HW with its integrated defense mechanisms, also conventional (functional) HW design bugs are of growing concern and can lead to security breaches which are extremely hard to detect in conventional verification flows. In fact, HW “bug escapes” can jeopardize the confidentiality and integrity of the entire system stack.

Check out:

• our papers at DATE-19 (link), DAC-20 (link), DAC-21 (link), IEEE Trans. on Computers (link) and DAC-2022 (coming up)
• this article in EETimes relating to our research
• online articles like in Verdict
• an Interview with Prof. Kunz in Deutschlandfunk (in German)

In our research, we focus on the HW security requirements at the microarchitectural level. The proposed methods directly apply to an SoC’s Register Transfer Level (RTL) description which serves as the golden model in most design flows and is the point of reference for sign-off verification. We develop techniques for formal security analysis which are exhaustive with respect to well-defined classes of security threats, such as transient execution side channels (Spectre and Meltdown). Spectre and Meltdown are not the only security issues at the microarchitectural level. Our methods also cover security-critical design bugs, integrity violations by third-party IPs, violations of data obliviousness in HW and other threats.

Using our methods based on "Unique Program Execution Checking (UPEC)",  already dozens of previously unknown security breaches were found in several hardware designs (Rocketchip, BOOM, Pulpissimo, Ariane, Ibex, OpenTitan), including previously unknown variants of the Spectre attack. This is the first time that such vulnerabilities are identified by a tool rather than by the clever thinking of a human attacker.

Current (unpublished) research pursues the goal of a secure-by-construction RTL design methodology driven by UPEC.  The methodology systematically interleaves design steps and steps of specialized security verification. In this way, we can directly exploit synergies between the solvers of formal verification and the design process for fine-grain, customized HW defenses at the RTL. This allows for pinpoint and largely automated fixes with exhaustive protection against the modeled threats, while avoiding the overheads induced by the conservatism of current techniques.