Abstract
Formal verification of hardware often requires the creation of clock cycle accurate properties that need tedious and error-prone adapta tions for each design. Property violations further require attention from verification engineers to identify affected instructions. This oftentimes manual effort hinders the adoption of formal verifica tion at scale. This paper introduces Microarchitectural Control Flow Integrity ( CFI), a new general security property that can capture multiple classes of vulnerabilities under different threat models, most notably the microarchitectural violation of constant time execution and (micro-)architectural vulnerabilities that allow an attacker to hijack the (architectural) control flow. We show a novel approach for the verification of CFI using a single property that checks for information flows from instruction operands to the program counter by injecting taint at appropriate clock cycles. To check arbitrary sequences of instructions and associate property violations to a specific Instruction Under Verification (IUV), we propose techniques for declassifying tainted data when it is being written to registers and forwarded from the IUV through architec turally known paths. We show that our verification approach is low effort (e.g., requires tagging six signals) while capturing all interac tions between unbounded sequences of instructions in the extended threat model of CFI. We verify four RISC-V CPUs against CFI and prove that CFI is satisfied in many cases while detecting five new security vulnerabilities (4 CVEs), three of which are in Ibex, which has already been checked by state-of-the-art verification approaches. CCS Concepts • Security and privacy → Logic and verification. Keywords Hardware security; formal hardware verification; side-channels ACM Reference Format: Katharina Ceesay-Seitz, Flavien Solt, and Kaveh Razavi. 2024. CFI: Formal Verification of Microarchitectural Control-flow Integrity. In Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security (CCS ’24), October 14–18, 2024, Salt Lake City, UT, USA. ACM, New York, NY, USA, 15 pages. https://doi.org/10.1145/3658644.3690344 Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA © 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM. ACM ISBN 979-8-4007-0636-3/24/10 https://doi.org/10.1145/3658644.3690344 1 Introduction With the increasing cost of compromising software due to the plethora of mitigations and security analysis techniques [1, 2, 4, 8, 11, 30, 45, 62, 65, 92, 106, 110], the focus is shifting towards hardware vulnerabilities, highlighting the need for better hardware security analysis [21, 42, 44, 56, 58, 60, 67, 68, 78, 89, 95, 97, 102, 103, 104]. While there are recent advances in the area of hardware fuzzing [16, 17, 19, 26, 48, 54, 55, 59, 87, 94], unlike formal verifica tion, these fuzzers are not complete by design. Formal verification, however, requires significant per-design human effort due to the lack of generic security properties and simple verification meth ods that apply to various hardware designs. This paper introduces Microarchitectural Control-Flow Integrity ( CFI), a generic security property that captures constant-time and control-flow violations at the microarchitectural level and builds a novel approach for for mally verifying this new security property on existing open-source RISC-V CPUs. Hardware verification. To formally verify a hardware design at the Register Transfer Level (RTL), verification engineers often need to specify design-specific (security) properties which can then be evaluated with a model checker. According to a recent study [86], more than half of the human effort in the development of new hardware designs is dedicated to verification, with debugging being the largest effort (47%) during verification. With the increasing pop ularity of open-source RISC-V CPUs, their fast community-driven development cycles, and the increasing number of hardware vul nerabilities, reducing the verification effort is of utmost importance for ensuring reliable and secure CPUs in the future. New security properties that generalize to existing designs have the potential to capture different classes of security vulnerabilities while reducing the verification effort through automation. CFI. We define the microarchitectural control flow as the Pro gram Counter (PC) values at each clock cycle and make a key observation that a single generic security property can capture multiple classes of hardware vulnerabilities, such as constant-time violations or control-flow hijacks. This new property, which we call Microarchitectural Control-Flow Integrity ( CFI), enforces that the microarchitectural control flow is only influenced by instructions for which the Instruction Set Architecture (ISA) explicitly allows a control or data path from their operands to the PC. Data-dependent execution timing of a given instruction causes the PC to have dif ferent values at certain clock cycles, violating CFI. Furthermore, (micro-)architectural vulnerabilities that allow an attacker’s input to directly control the PC also violate CFI. Hence, the verification of CFI captures both classes of security vulnerabilities. CFI verification. Previous approaches that aim to verify the constant-time subset of CFI either require manual extraction of design conditions and specification of candidate invariants [33, 34, 100], or cannot verify the interaction between secure and insecure instructions [33, 34, 35], and neither can provide security classi fications per instruction for unconstrained instruction sequences. Our verification approach aims to address these challenges in the broader threat model of CFI. We make a key observation that CFI can be verified using a single property that checks for all informa tion flows from critical input data, encompassing secret or attacker controlled data, to the PC. By declassifying valid flows through instruction writeback and forwarding paths, CFI can capture in formation flows from instructions to in-flight or future instructions as well. The CFI property can attribute property violations to specific instructions and can check arbitrary and unbounded se quences of instructions, where instructions may operate on any combination of public, secret, or attacker-controlled data. Formal verification of Information Flow Tracking (IFT) proper ties using taint logic has so far been limited to individual modules and properties expressed over interface signals [5, 47, 113]. Leverag ing and extending the state-of-the-art IFT logic, CellIFT [88], com bined with a state-of-the-art model checker [18], we formally verify CFI expressed over CPU internal signals spanning the entire CPU pipeline. We evaluate CFI against four open-source in-order RISC V processors: Kronos [57], PicoRV32 [75], Ibex [49], and Scarv [84]. We automatically (dis-)prove CFI for an unbounded number of clock cycles, and find five new vulnerabilities: two in Kronos that had previously undergone fuzz testing [87] and three in Ibex that had already been extensively verified [34, 35, 50, 100]. Contributions. We make the following contributions: • We introduce CFI, a generic security property, which enforces that cycle-accurate values of the PC are not influenced by mi croarchitectural data dependencies, except via explicitly ISA specified control or data paths. • We formally define CFI as a generic information flow property. • We develop the first generic and automated verification method for formally proving the CFI property using SystemVerilog Assertions and an existing open-source IFT mechanism [88], reusable across in-order RISC-V CPU designs, and capable of verifying arbitrary and unbounded instruction sequences. • We show that formal verification of cell-level taint tracking can scale to in-order RISC-V CPU designs. We prove CFI or find counterexamples by verifying four RISC-V CPUs. In particular, we find five new vulnerabilities: three in Kronos that had pre viously undergone fuzz testing [87] and two in Ibex that had already been extensively verified [34, 35, 50, 100]. Open sourcing. To the extent that commercial licenses permit, we open-source our toolchain. https://comsec.ethz.ch/research/ha rdware-design-security/mucfi/. The extended version of this paper, including appendices, can be found in [25].
Showing the abstract — retrieve the full paper via the Exa API.