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.
Author: | Mohammad Rahmani Fadiheh |
---|---|
URN: | urn:nbn:de:hbz:386-kluedo-69305 |
DOI: | https://doi.org/10.26204/KLUEDO/6930 |
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 |
MSC-Classification (mathematics): | 94-XX INFORMATION AND COMMUNICATION, CIRCUITS |
Licence (German): |