Microarchitectural Control-flow Integrity (𝜇CFI) is a new security property that enforces the integrity of the microarchitectural control flow which we define as cycle-granular valuations of the Program Counter (PC). Formal verification of 𝜇CFI proves that instructions do not leak data via hardware timing side channels and do not manipulate the architectural control flow via vulnerabilities in the microarchitectural implementation. 𝜇CFI verification combines information flow tracking with formal verification to prove whether operand data can affect the Program Counter (PC) value or update time. We discovered several new vulnerabilities (e.g., CVE-2024-44927, CVE-2023-51973, CVE-2023-51974 and CVE-2024-28365) in open-source CPUs. The 𝜇CFI paper will be presented at CCS’24 and is already open source here.
Motivation
Software security measures often assume that the hardware functions as specified and is secure. However, hardware vulnerabilities may undermine software security principles, such as constant time (CT) or control-flow integrity (CFI).
Data-dependent execution time of instructions can leak secret operand values. An information flow from the operand data (from the register file or forwarding paths) to the PC indicates such a leakage. Furthermore, if such a flow exists and attacker-controlled data is passed to an instruction, an attacker can manipulate the PC.
Certain flows to the PC are expected, e.g., when a branch decision is taken based on a user input (e.g., a password check). However if a branch instruction is able to divert the control flow to an address provided as one of its operands, and it operates on attacker-controlled data, control-flow hijacking attacks become possible.
𝜇CFI – Microarchitectural Control-flow Integrity
We define the microarchitectural control flow (𝜇CF) as the clock-accurate sequence of PC values. Microarchitectural control flow integrity (𝜇CFI) enforces that the microarchitectural control flow is only influenced by instructions for which the ISA explicitly allows a control or data path from their operands to the PC.
Verifying 𝜇CFI
𝜇CFI is a security property that generalizes across CPUs and captures two threat models (information leakage via CT violations and control flow hijacks) in a single formal property. Making use of information flow tracking logic, we specify it as SystemVerilog property and formally prove it with a model checker.
For instructions for which the RISC-V ISA does not specify any flows, we use CellIFT to prove that operand data does not flow to the PC. We use CellDFT, a new Cell-level Data Flow Tracking scheme, to prove that there are no data flows to the PC if the ISA allows control decisions being taken based on operand data (e.g., for branches).
By declassifying information flows via architecturally known paths (through forwarding paths and the register file), we are able to prove 𝜇CFI for instructions within arbitrary, possible infinitely long, programs. An instruction that is proven to satisfy 𝜇CFI is guaranteed to never influence the PC of any in-flight or younger instructions via unspecified paths.
CellDFT
CellDFT is a variant of CellIFT that captures data flows only. It does not track taint propagation via control paths, which we define as paths from a cell’s input to its output, that do not perform data-manipulating operations (see the paper for details). Paths captured by CelllDFT are a subset of the paths captured by CellIFT. CellDFT is open-sourced here.
Declassification
By declassifying information flows via architecturally known paths (through forwarding paths and the register file), we are able to prove 𝜇CFI for instructions within arbitrary, possible infinitely long, programs. An instruction that is proven to satisfy 𝜇CFI is guaranteed to never influence the PC of any in-flight or younger instructions via unspecified paths.
Discovered Vulnerabilities
Many instructions could be formally proven to satisfy 𝜇CFI. We also discovered several severe vulnerabilities. Most notably, a CT violation and register data leakage (CVE-2024-28365) on the Ibex CPU (affecting all configurations), which is used in the OpenTitan root-of-trust. This bug has been fixed after our report with PR2166. We further found a control-flow hijack caused by branches in a customized configuration of Ibex.
In the Kronos CPU we found a control-flow hijack by an ‘addi’ instruction (CVE-2023-51973), a control-flow hijack where jumps and branches read from an older instruction’s register (CVE-2024-44927), and constant time violations (CVE-2023-51974).
The table below shows a summary of our results when applying 𝜇CFI to different RISC-V cores.
Paper and Code
𝜇CFI will be presented at CCS ’24, and is readily open-source here! Use it on your CPU if you want to make sure your RISC-V CPU does not suffer from security bugs and let us know if you found new bugs! Bing created the following logo for 𝜇CFI:
Frequently Asked Questions
Am I affected?
If you use one of the RISC-V CPU versions that we verified in your products, you might be affected. We provide the detailed configuration and integration setting in which we discovered the vulnerabilities in the paper.
If my software code follows the CT principle, is it secure?
Depending on which hardware you run it, your code may be executed in insecure ways (that 𝜇CFI can detect).
My RISC-V CPU states that it supports the Zkt (constant time cryptographic) extension. Is my crypto code guaranteed to execute in constant time?
CPU maintainers can only provide you this guarantee if they formally prove it. Note that fuzzing and other testing methods do not provide formal guarantees. If the CPU is verified with 𝜇CFI, instructions are guaranteed to never influence the timing of the current or any younger instructions.
Is there a CT-secure RISC-V scalar cryptographic extension implementation?
We proved that the Scarv CPU’s implementation of the RISC-V scalar cryptographic extensions satisfies CT.
For which other verification problems can I use CellDFT?
CellDFT can be used to track data flows. For example, you can verify whether forwarded data can be used to calculate an ALU result. Or you could prove that the forwarded data does not reach the ALU in case register addresses do not match. We open-sourced CellDFT in our github.
Do I need a specific formal verification tool to prove 𝜇CFI?
The setup on our github works with any formal verification tool that can prove SystemVerilog Assertions.
Acknowledgements
This work was supported by the Swiss State Secretariat for Education, Research and Innovation under contract number MB22.00057 (ERC-StG PROMISE).