Unique Program Execution Checking: A Novel Approach for Formal Security Analysis of Hardware

  • This thesis addresses the need for a new approach to hardware sign-off verification which guarantees the security of processors at the Register Transfer Level (RTL). To this end, we introduce a formal definition of security with respect to microarchitectural vulnerabilities, formulated as a hardware property. We present a formal proof methodology based on 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 the new attack scenarios discovered in our experiments with UPEC. UPEC operates on a verification model consisting of two identical instances of the SoC design under verification. The SoC instances in the model execute the same program. The only difference between the two instances is the content of the protected part of the memory, i.e., the secret.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Mohammad Rahmani Fadiheh
Advisor:Wolfgang Kunz
Document Type:Doctoral Thesis
Language of publication:English
Publication Date:2022/09/06
Year of Publication:2022
Publishing Institute:Technische Universität Kaiserslautern
Granting Institute:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2022/09/05
Date of the Publication (Server):2022/09/06
Tag:Electronic Design Automation; Formal Verification; Hardware Security
Number of page:V, 141
Faculties / Organisational entities:Kaiserslautern - Fachbereich Elektrotechnik und Informationstechnik
CCS-Classification (computer science):B. Hardware
DDC-Cassification:6 Technik, Medizin, angewandte Wissenschaften / 620 Ingenieurwissenschaften und Maschinenbau
Licence (German):Creative Commons 4.0 - Namensnennung (CC BY 4.0)