What is it about?
Microarchitectural Control-flow Integrity 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 muCFI 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. Our verification methodology combines information flow tracking with formal verification to prove whether operand data can affect the Program Counter (PC) value or update time. Microarchitectural control-flow integrity is the first formal information flow tracking based work that got CVEs (e.g., CVE-2024-44927, CVE-2023-51973, CVE-2023-51974 and CVE-2024-28365) for its newly discovered vulnerabilities in open-source CPUs.
Featured Image
Photo by Brian Kostiuk on Unsplash
Why is it important?
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 to the program counter indicates such a leakage. Furthermore, if such a flow exists and attacker-controlled data is passed to an instruction, an attacker can hijack the software control flow. Many instructions could be formally proven to satisfy microarchitectural control-flow integrity. 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.
Perspectives
Formal verification can seem like a daunting task. muCFI shows that with a general definition of a security property it is possible to largely automate the verification and re-use the code and method across multiple CPUs. Furthermore, it is possible to discover serious vulnerabilities quickly.
Katharina Ceesay-Seitz
ETH Zurich
Read the Original
This page is a summary of: μCFI: Formal Verification of Microarchitectural Control-flow Integrity, December 2024, ACM (Association for Computing Machinery),
DOI: 10.1145/3658644.3690344.
You can read the full text:
Resources
Open source code
The main repository containing all the code for generating taint conditions and verifying Microarchitectural Control-flow Integrity. The code can reproduce the experiments or can be applied to other CPUs.
Presentation in the Yosys User Group
The presentation in the Yosys User Group extends the conference presentation with more details on the developed and use Yosys passes.
Main project website
The main project website on our COMSEC (Computer Security) group website of ETH Zurich.
Contributors
The following have contributed to this page
