Osmosis 2020: Customer Story - Hardware Security Verification Using Unique Program Execution Checking | Technische Universität Kaiserslautern

Wolfgang Kunz, Professor, Department of Electrical & Computer Engineering

The discovery of the Spectre and Meltdown security attacks in advanced processors has resulted in high public alertness about the security of hardware. The root cause of these attacks is information leakage across a new class of side channels, called transient execution side (TES) channels. Many sources believe that TES channels are intrinsic to highly advanced processor architectures based on speculation and out-of-order execution, suggesting that such security risks can be avoided by staying away from high-end processors. This talk, however, presents verification results involving OneSpin 360 DV, which show that the problem is of wider scope: similar leakages are possible also in average-complexity processors and must be addressed during RTL design time. Our new method is called Unique Program Execution Checking (UPEC). It does not require a priori knowledge on possible attacks and detects HW vulnerabilities systematically without demanding the clever thinking of a human attacker. UPEC provides a unified approach to HW security analysis. In addition to TES channels, it also detects those functional bugs in a design that cause security issues, for example, related to the communication between the core and its peripherals. We present results from several case studies on RISC-V systems, Rocket Chip, BOOM, Ariane, and Pulpissimo, in which UPEC detected a number of previously unknown security vulnerabilities.