Information-Flow Integrity (IFI) is a novel CPU security property that formalizes the legal information flows between architectural hardware elements, exactly as derivable from the Instruction Set Architecture (ISA). Formal verification of IFI enables the systematic detection of both microarchitectural vulnerabilities and functional bugs that compromise confidentiality or integrity.
To concretely verify IFI on a CPU implementation, we introduce VerIFI, a verification method that proves four key properties for the existence or absence of certain information flows. We applied VerIFI to two verified open-source RISC-V CPUs, Kronos and Ibex, confirming known vulnerabilities and discovering two new ones (including CVE-2024-42999).
The IFI paper will be presented at EuroS&P 2026. VerIFI is already open-sourced here.
Motivation
Modern Central Processing Units (CPUs) are plagued by information leakage and integrity vulnerabilities. Errata of commercial CPUs and open-source bug reports frequently reveal Information Flow (IF) violations. Such vulnerabilities compromise fundamental confidentiality or integrity properties in the CPU, violating how information should propagate as implicitly defined by the ISA.
Vulnerabilities that violate confidentiality enable attackers to leverage timing side channels or architectural bugs to exfiltrate information. Vulnerabilities that compromise integrity typically lead to a full system compromise, e.g., by hijacking the architectural control flow, or leaking information by manipulating the speculative control flow.
While existing verification methods like functional verification or Constant Time (CT) verification capture parts of IFI, we previously lacked a generic method that fully specifies and verifies correct information flows in a CPU for a given ISA. VerIFI does not require a complete functional reference model, which might not be available for custom ISA extensions and it scales beyond functional verification.
IFI – Information-Flow Integrity
We define Information-Flow Integrity (IFI) to augment existing ISAs with information flow policies by mapping bit-precise taint propagation rules from hardware Information Flow Tracking (IFT) methods to RISC-V instructions, and extending them in some cases. A program executed on a CPU that is proven to comply with IFI is guaranteed not to expose more information than is allowed by the ISA. Similarly, such a program is guaranteed not to violate the integrity of data beyond the manipulations allowed by the ISA. To account for known information leakage, like, e.g., through the cache, our Specification-derived Information Flow (SIF) semantics allows the customization of the taint propagation rules per instruction. These customizations can be specified as declassification conditions in VerIFI.
Verifying IFI
VerIFI verifies that a concrete CPU implementation propagates information exactly as defined by Specification-derivable Information Flow (SIF) rules. Making use of the hardware IFT logic CellIFT, we specify four key properties that together verify the equivalence of the SIFs and effective hardware information flows:
- Confinement: Enforces that information only propagates from architectural states when an instruction is specified to cause that information flow.
- Containment: Enforces that whenever information is specified to propagate from architectural states as a consequence of instruction execution, it reaches only the specified instruction destinations.
- Freshness: Ensures that information indeed reaches instruction destinations whenever that information flow should not be masked, ensuring that stale data in instruction destinations is appropriately overwritten and does not leak.
- Masking: Verifies that information does not propagate to an instruction’s destination when it is supposed to be masked by non-tainted data.
We specify these properties as SystemVerilog assertions and formally prove them with a model checker.
Precise Spatio-Temporal Path Gating
To avoid excessive blocking of information flows or verification scenarios, we introduce path gating, a new spatio-temporal precise taint injection and declassification method. This method gates the taint propagation at specified locations, under specified conditions, while restoring the original taint path otherwise. This allows controlled introduction and declassification of taint, accommodating microarchitectural optimizations and known vulnerabilities.
Discovered Vulnerabilities
Despite both Kronos and Ibex having undergone prior formal verification and fuzz testing, VerIFI successfully proved properties for many instructions while uncovering two new vulnerabilities:
- Kronos (CVE-2024-42999): A memory data leakage vulnerability where an attacker capable of injecting spurious memory acknowledgements can force an invalid instruction to decode as a load, writing arbitrary memory values into General Purpose Registers (GPRs).
- Kronos (GPR Leakage – same rootcause as CVE-2023-51973): A spurious CSR write-enable activation caused by unexpected bus acknowledgements allows source registers of arithmetic instructions to be mistreated as CSR write data, leaking to other GPRs.
- Ibex (Memory data leakage – NEW): Ibex responds to activity on the memory bus even though no load or store instruction was executed. A containment violation happens, where Ibex unexpectedly triggers an exception due to a mismatch of Error Correcting Code (ECC) bits when memory data changes on a shared bus. This allows malicious IP cores to deduce bus data or attack CPU availability.
We also successfully rediscovered existing vulnerabilities (like the Ibex multiplication register leak CVE-2024-28365 and the Kronos control-flow hijack CVE-2024-44927), which validate our methodology.
Paper and Code
VerIFI is provided open-source at our GitHub repository as far as licenses allow! Use it for verifying your CPUs against information flow integrity violations. Let us know if you find new bugs!
Frequently Asked Questions
Can I use VerIFI to verify custom ISA extensions? Yes, this is a perfect use case if you have no complete functional model of your extension available. You can specify the information flows expected to be caused by your custom extensions. Then you can specify them as taint injection and declassification conditions in VerIFI.
Does VerIFI cover both constant-time and functional bugs? Yes! IFI unifies the aspects of functional verification and constant-time verification that are relevant for Information Flow Tracking, capturing both timing side channels and architectural data leaks/integrity violations in a single specification framework.
Which information flow tracking method can I use? We implemented VerIFI using CellIFT, but you might re-implement it using another taint tracking logic or self-composition (miters).
Do I need a specific formal verification tool to prove IFI? The setup works with any industrial hardware formal verification tool that can prove concurrent SystemVerilog Assertions. In our evaluation, we used Cadence Jasper.
Acknowledgements
This work has been supported by a Qualcomm Innovation Fellowship and the Swiss State Secretariat for Education, Research and Innovation under contract number MB22.00057 (ERC-StG PROMISE).