Unique Program Execution Checking
Unique Program Execution Checking (UPEC) is a verification methodology designed to assess the security of programs in the presence of confidential information, commonly referred to as "secrets." At its core, UPEC aims to determine whether the execution of a program remains invariant despite the presence of such secrets. This is formalized through the concept of unique program execution, which asserts that a program's behavior must not depend on the secret value across all execution cycles. To achieve this, UPEC constructs a tailored miter model where two instances of a CPU execute the same program under identical conditions, except for one protected memory location that contains the secret. By examining variations in execution behavior at the microarchitectural level - known as the "microarchitectural footprint" - UPEC identifies potential vulnerabilities that could arise from secret-dependent variations, which may not be evident at the instruction set architecture (ISA) level. This comprehensive approach allows for the verification of security properties in complex out-of-order processors, ensuring that sensitive information remains secure throughout program execution.
Learn MoreVulnerabilities detected by UPEC
The following table summarizes various findings of vulnerabilities to microarchitectural attacks that have been detected using the UPEC methodology.
| Device | Type of Vulnerability | Description | Detected by | Disclosed | Publication | Fix Available? |
|---|---|---|---|---|---|---|
| Rocket Chip | PMP violation | The PMP implementation allowed the modification of a locked memory configuration in privileged mode without requiring a reboot. | UPEC | Mar. 25, 2019 | M.R. Fadiheh, D. Stoffel, C. Barrett, S. Mitra and W. Kunz: Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking, 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE) | Yes |
| BOOMv2 | Spectre | Multiple variants of Spectre-PHT and Spectre-BTB using the cache as a side channel | UPEC-OoO | Jul. 20, 2020 | M.R. Fadiheh, J. Müller, R. Brinkmann, S. Mitra, D. Stoffel and W. Kunz: A Formal Approach for Detecting Vulnerabilities to Transient Execution Attacks in Out-of-Order Processors 2020 57th ACM/IEEE Design Automation Conference (DAC) | No |
| Spectre-STC | Port contention on write port to register file | UPEC-OoO | Jul. 20, 2020 | M.R. Fadiheh, J. Müller, R. Brinkmann, S. Mitra, D. Stoffel and W. Kunz: A Formal Approach for Detecting Vulnerabilities to Transient Execution Attacks in Out-of-Order Processors 2020 57th ACM/IEEE Design Automation Conference (DAC) | No | |
| Spectre-STC | Port contention on TLB | UPEC-OoO | Jul. 20, 2020 | M.R. Fadiheh, J. Müller, R. Brinkmann, S. Mitra, D. Stoffel and W. Kunz: A Formal Approach for Detecting Vulnerabilities to Transient Execution Attacks in Out-of-Order Processors 2020 57th ACM/IEEE Design Automation Conference (DAC) | No | |
| BOOMv3 (SonicBOOM) | Meltdown | Delayed exception handling in load-store-unit | UPEC-OoO | May 6, 2021 | T. Jauch, A. Wezel, M.R. Fadiheh, P. Schmitz, S. Ray, J. Fung, C.W. Fletcher, D. Stoffel, W. Kunz: Secure-by-Construction Design Methodology for CPUs: Implementing Secure Speculation on the RTL 2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD) | Yes |
| Spectre | UPEC identified a total number of 29 instructions being able to form a covert channel: LB, LBU, LH, LHU, LW, BEQ, BNE, BGE, BGEU, BLT, BLTU, JALR, STA (for all store instructions), DIV, DIVU, DIVW, DIVUW, REM, REMU, REMW, REMUW, FDIV.S, FDIV.D, FSQRT.S, and FSQRT.D |
UPEC-OoO | Oct. 20, 2023 | T. Jauch, A. Wezel, M.R. Fadiheh, P. Schmitz, S. Ray, J. Fung, C.W. Fletcher, D. Stoffel, W. Kunz: Secure-by-Construction Design Methodology for CPUs: Implementing Secure Speculation on the RTL 2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD) | Yes | |
| Data-Dependent Timing | Data-dependent timing behaviour for all division, load/store, jump, branch, and floating-point instructions | UPEC-DIT | Aug. 25, 2023 | L. Deutschmann, J. Müller, M.R. Fadiheh, D. Stoffel, W. Kunz: A Scalable Formal Verification Methodology for Data-Oblivious Hardware in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 43, no. 9, pp. 2551-2564, Sept. 2024 | No | |
| CVA6 | Data-Dependent Timing | Data-dependent timing behaviour for all division, load/store, jump, and branch instructions | UPEC-DIT | Aug. 23, 2022 | L. Deutschmann, J. Müller, M.R. Fadiheh, D. Stoffel, W. Kunz: Towards a formally verified hardware root-of-trust for data-oblivious computing 2022 59th ACM/IEEE Design Automation Conference (DAC) | No |
| OpenTitan | Integrity Violation | Denial-of-Service (DoS) via untrusted IP | UPEC-OI | Aug. 9, 2023 | D. Mehmedagić, M.R. Fadiheh, J. Müller, A.L. Duque Antón, D. Stoffel, W. Kunz: Design of Access Control Mechanisms in Systems-on-Chip with Formal Integrity Guarantees 2023 32nd USENIX Security Symposium (USENIX Security 23) | No |
| CHERIoT-Ibex | Meltdown-style attack | Possibility to probe for specific bits of a data word outside the current compartment. | UPEC-CHERI | Jul. 26, 2024 | A.L. Duque Antón, J. Müller, P. Schmitz, T. Jauch, A. Wezel, L. Deutschmann, M.R. Fadiheh, D. Stoffel, W. Kunz: VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL 2024 IEEE/ACM International Conference on Computer Aided Design (ICCAD) | Yes |
Case Studies
Transient Execution Side Channels
UPEC exposed issues in out-of-order processors that allowed leakage of secret data due to mispredicted speculative execution paths.
Learn MoreTiming Side Channels
UPEC-DIT detected timing-based vulnerabilities in various cores and hardware accelerator where data-dependent execution could reveal confidential data.
Learn MoreFunctional Security Bugs
UPEC found weaknesses in Physical Memory Protection (PMP) that allowed unauthorized access to protected memory regions.
Learn MoreOperation Integrity in SoCs
UPEC-OI was able to detect a Denial-of-Service attack using an untrusted IP in OpenTitan.
Learn More