UPEC: Formal Security Verification

Figure: Speculative program execution can enable side channel

Unique Program Execution Checking (UPEC) is a method for formally verifying the security of hardware at the RTL. UPEC checks whether confidential data in the system can be stolen by an attacker (user program) for any programs that can be executed on the hardware. UPEC detects all confidentiality violations that are made possible by so-called transient execution side channels of the microarchitecture. Spectre and Meltdown are well-known examples of this class of vulnerabilities. In addition, UPEC also uncovers all confidentiality vulnerabilities that can arise due to design errors (“HW bugs”), which easily occur when implementing protection mechanisms.

In Phase 1 of the Scale4Edge project, the security analysis focuses primarily on cores ranging from smaller in-order cores to larger out-of-order processors. The focus is on transient execution side channels. In Phase 2, UPEC will be extended to entire SoCs. SoCs pose different security challenges than processor cores, including secure system integration, functional design flaws, and system integrity violations.