Unique Program Execution Checking for Exhaustive Hardware Security Analysis

Transient execution attacks still pose a genuine threat to the security of modern computing systems, even 7 years after the discovery of Spectre and Meltdown. Despite recent advances, understanding the intricate implications of microarchitectural design decisions on hardware security remains a great challenge. Past efforts on formal security verification suffer from scalability issues to prove absence of vulnerabilities, and in many cases rely on a priori knowledge about potential attacks, limiting their ability to detect previously unknown ones.  

This talk will present Unique Program Execution Checking (UPEC), which can be used to systematically detect all vulnerabilities to transient execution attacks in RTL designs. UPEC does not exploit any a priori knowledge on known attacks and can therefore detect also vulnerabilities based on new, so far unknown, types of channels. This is demonstrated by two new attack scenarios discovered in our experiments with UPEC. UPEC scales to a wide range of HW designs, including processors with deep out-of-order speculative execution (BOOM), and can even deliver well-defined guarantee for the absence of vulnerabilities for complex secure speculation schemes.  Furthermore, this talk will discuss the application of UPEC in security verification for different objectives and threat models.