When a Patch is Not Enough – HardFails: Software-Exploitable Hardware Bugs
Ghada Dessouky, David Gens, Patrick Haney, Garrett Persyn, Arun Kanuparthi, Hareesh Khattri, Jason M. Fung, Ahmad-Reza Sadeghi, Jeyavijayan Rajendran
(Submitted on 1 Dec 2018)

In this paper, we take a deep dive into microarchitectural security from a hardware designer’s perspective by reviewing the existing approaches to detect hardware vulnerabilities during the design phase. We show that a protection gap currently exists in practice that leaves chip designs vulnerable to software-based attacks. In particular, existing verification approaches fail to detect specific classes of vulnerabilities, which we call HardFails: these bugs evade detection by current verification techniques while being exploitable from software. We demonstrate such vulnerabilities in real-world SoCs using RISC-V to showcase and analyze concrete instantiations of HardFails. Patching these hardware bugs may not always be possible and can potentially result in a product recall. We base our findings on two extensive case studies: the recent Hack@DAC 2018 hardware security competition, where 54 independent teams of researchers competed world-wide over a period of 12 weeks to catch inserted security bugs in SoC RTL designs, and an in-depth systematic evaluation of state-of-the-art verification approaches. Our findings indicate that even combinations of techniques will miss high-impact bugs due to the large number of modules with complex interdependencies and fundamental limitations of current detection approaches. We also craft a real-world software attack that exploits one of the RTL bugs from Hack@DAC that evaded detection and discuss novel approaches to mitigate the growing problem of cross-layer bugs at design time.

https://arxiv.org/abs/1812.00197

SPECTECTOR: Principled Detection of Speculative Information Flows
Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke, Andrés Sánchez
(Submitted on 20 Dec 2018)

Since the advent of SPECTRE, a number of countermeasures have been proposed and deployed. Rigorously reasoning about their effectiveness, however, requires a well-defined notion of security against speculative execution attacks, which has been missing until now. We present a novel, principled approach for reasoning about software defenses against SPECTRE-style attacks. Our approach builds on speculative non-interference, the first semantic notion of security against speculative execution attacks. We develop SPECTECTOR, an algorithm based on symbolic execution for automatically proving speculative non-interference, or detecting violations.
We implement SPECTECTOR in a tool, and we use it to detect subtle leaks — and optimizations opportunities — in the way major compilers place SPECTRE countermeasures.

https://arxiv.org/abs/1812.08639