Microarchitectural Control-flow Integrity (μCFI): Thwarting Timing & Hijacking Attacks
In a study, researchers from COMSEC, the computer security group at ETH Zurich’s Department of Information Technology and Electrical Engineering (D-ITET), have developed and formally verified Microarchitectural Control-flow Integrity (μCFI), a security framework designed to protect CPU control flows from timing-based and control-flow hijacking attacks.
Traditional software security has often relied on the assumption that underlying hardware behaves as expected. However, hardware-level vulnerabilities can undermine even the most robust software security techniques, such as Control-flow Integrity (CFI) and constant-time execution principles. Hardware-based timing channels can leak sensitive information, while control-flow hijacking remains a persistent threat in modern computing.
μCFI directly addresses these issues by enforcing control-flow integrity at the microarchitectural level—a more granular control over the Program Counter (PC), ensuring that hardware behavior aligns with what’s architecturally specified. This novel approach combines information flow tracking with formal verification, offering rigorous proof that certain CPU instructions do not leak data or manipulate the control flow in unexpected ways.
At its core, μCFI uses formal verification techniques to track how operand data influences the Program Counter (PC), which governs instruction execution. Through precise information flow tracking, researchers can detect leaks and vulnerabilities that occur when instructions modify the PC in ways they shouldn’t.
By defining the microarchitectural control flow (μCF) as the clock-accurate sequence of PC values, μCFI enforces a strict policy that prevents unauthorized changes to this flow, such as those from attacker-controlled data. μCFI’s verification ensures that only expected instructions can affect the control flow, providing a robust defense against both timing side-channel attacks and control-flow hijacking.
The formal verification approach employed in μCFI has already revealed several critical vulnerabilities in popular open-source CPUs. For example:
- CVE-2024-28365: A constant-time violation and register data leakage affecting the Ibex CPU, commonly used in the OpenTitan root-of-trust framework. The issue was reported and swiftly patched, securing this critical CPU architecture.
- CVE-2023-51973 and CVE-2024-44927: Control-flow hijacks identified in the Kronos CPU caused by improper handling of certain branch and jump instructions.
- CVE-2023-51974: A constant-time violation in the Kronos CPU, which could expose secret data through timing side channels.
The μCFI verification process was crucial in identifying these vulnerabilities, leading to improvements in CPU design that enhance overall security.
One of the most exciting aspects of the μCFI project is its open-source nature. The research team has made μCFI’s code publicly available, encouraging CPU designers and security professionals to integrate it into their own hardware designs. As CPUs evolve, this tool offers a promising way to formally verify that hardware behaves securely, even in complex, real-world environments.
The research will be presented at the ACM Conference on Computer and Communications Security (CCS 2024), where attendees will have the opportunity to dive deeper into the findings and explore the future applications of μCFI. For now, interested users can access the code and further details on the COMSEC GitHub repository.
