VerIFI: Formal Verification of Microarchitectural Information-Flow Integrity

Welcome to the VerIFI project. Information Flow Integrity (VerIFI) verifies whether instructions leak information about their operand data via any architecturally observable leakage channels, inclduing timing side-channels, also known as constant time violation, and leakage through registers or memory. VerIFI proves that instructions indeed write to their intended destinations, at the specified times, and that they do not violate the integrity of any registers. VerIFI further proves that information remains contained in architectural states when no instruction is specified to move that data.

Take a look at the paper here.

Feel free to you re-use any part of our toolchain. Please cite as:

@inproceedings{2026_ceesay-seitz_verifi,
title="VerIFI: Formal Verification of Microarchitectural Information-Flow Integrity",
author="Ceesay-Seitz, Katharina and Solt, Flavien and Yin, Mengyuan and Razavi, Kaveh",
booktitle={2026 IEEE 11th European Symposium on Security and Privacy (EuroS\&P)},
year = {2026},
organization={IEEE}
}

Abstract

Fundamental security properties such as confidentiality and integrity are violated in CPUs due to unintended or missing information flows. We introduce Information-Flow Integrity (IFI), a CPU property that formalizes the legal information flows between architectural hardware elements, as derivable from the ISA. Ensuring 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 captures IFI by proving four key properties for the existence or absence of certain information flows. Specifically, VerIFI ensures that data is appropriately fresh, masked by non-tainted data, and that information flows are contained within the originating architectural elements, and confined to the correct architecturally-visible state elements across space and time. VerIFI introduces a precise spatio-temporal path gating technique that supports controlled introduction and declassification of information flows, accommodating microarchitectural optimizations and known exceptions. Applying VerIFI to two verified RISC-V CPUs, Kronos and Ibex, we confirm known vulnerabilities and discover two new ones. %, where for one of them we obtained a CVE.

Properties

All assertions that need to be proven per instruction are prefixed with ifi_.

Confinement, Freshness, Masking

Run with TAINT_TYPE LEGAL:

make run CONFIG=data_leakage INSTR_TYPE=ALU TAINT_TYPE=LEGAL DESIGN_TYPE=NORMAL/FIX

Confinement only

Proofs are sometimes slower when logic is included in the setup that is not even used. If you want to prove confinement only, define NO_MASKING_NO_FRESHNESS at the top of formal/properties/data_leakage.sv. This can significantly speed up the verification. We obtained the multiplication confinement results like this.

Containment

Run with TAINT_TYPE ILLEGAL:

make run CONFIG=data_leakage TAINT_TYPE=ILLEGAL DESIGN_TYPE=NORMAL/FIX

How to run

Run experiments with make run from the CPU-specific verification directory depending on which design you want to verify.

• Ibex: execute make commands inside verification/ibex. Example:

Confinement, masking, freshness:

• make run CONFIG=data_leakage TAINT_TYPE=LEGAL INSTR_TYPE=ALU DESIGN_TYPE=FIX

Change the instruction type as desired.

Containment:

• make run CONFIG=data_leakage DESIGN_TYPE=FIX TAINT_TYPE=ILLEGAL

• Kronos: execute make commands inside verification/kronos. Example:

Confinement, masking, freshness:

• make run CONFIG=data_leakage INSTR_TYPE=ALU TAINT_TYPE=LEGAL DESIGN_TYPE=NORMAL
• make run CONFIG=data_leakage INSTR_TYPE=LSU TAINT_TYPE=LEGAL DESIGN_TYPE=NORMAL

Containment:

• make run CONFIG=data_leakage DESIGN_TYPE=FIX TAINT_TYPE=ILLEGAL

Type make help to see all options.

When the GUI opens, select the task and prove all properties starting with ifi_.

Scenarios

The main data-leakage property is configured in formal/properties/data_leakage.sv. It contains two groups of scenario switches: These switches are defined in the property file and control which proof scenario is instantiated.

Branch scenarios (BR)

Enable exactly one branch setup to model different taint flows:

• BR_OP_SCENARIO_NO_DECLSSIFICATION — no declassification and no DIT; taken branches can stall the CPU and expose data-dependent timing.
• BR_OP_SCENARIO_DECLASS_BR_DECISION — declassifies the branch decision so pipeline control signals such as stall are not tainted.
• BR_OP_SCENARIO_DIT — enables DIT so branches should complete in data-independent time.

The file currently defaults to the declassification branch setup, and BR_OP_SCENARIO_DIT is treated as an additional toggle that enables the shared DIT define.

Multiplication / division scenarios (MULT)

Choose one multiplication setup:

• MULT_SCENARIO_DIT — injects taint in DIT mode; multiplications and divisions are expected to be secure.
• MULT_SCENARIO_NO_DIT — injects taint without DIT; operand 2 leakage is expected to produce a counterexample because timing depends on the data.

The file currently enables MULT_SCENARIO_DIT by default.

Ibex data_leakage.sv ifdef options

The Ibex property file verification/ibex/formal/properties/data_leakage.sv contains compile-time switches for specific experiment scenarios.

• BR: Enables branch-specific scenario selection logic.

  • BR_OP_SCENARIO_NO_DECLSSIFICATION: Branch decision is not declassified. Without DIT, taken branches can taint timing-related control (e.g., stall behavior).
  • BR_OP_SCENARIO_DECLASS_BR_DECISION: Declassifies the branch decision so branch control behavior is treated as non-sensitive.
  • BR_OP_SCENARIO_DIT: Enables DIT-gated branch behavior checks. When enabled, the file also defines DIT.

• MULT: Enables multiply/divide-specific scenario selection logic.

  • MULT_SCENARIO_DIT: Runs MUL/DIV checks with DIT enabled at taint injection. This is expected to prove data-independent timing behavior.
  • MULT_SCENARIO_NO_DIT: Runs MUL/DIV checks without DIT. This is expected to expose timing-dependent counterexamples for relevant operand flows.

• NO_MASKING_NO_FRESHNESS (set to 1): Excludes freshness/masking logic by loading dummy conditions. This is intended as a proof-speed optimization for confinement-only runs.

Notes:

• DIT is not typically set directly in this file; it is derived from the selected scenario (BR_OP_SCENARIO_DIT or MULT_SCENARIO_DIT).
• Keep branch and multiply scenarios scoped to their respective guards (BR and MULT) to avoid mixing unrelated experiment settings.

Available instruction type groups (see details and full lists in verification/common/instr_type.json):

• ALU: LUI, AUIPC, ADDI, SLTI, SLTIU, XORI, ORI, ANDI, SLLI, SRLI, SRAI, ADD, SUB, SLL, SLT, SLTU, XOR, SRL, SRA, OR, AND
• BR: JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU
• JUMP: JAL, JALR
• CSR: CSRRW, CSRRS, CSRRC, CSRRWI, CSRRSI, CSRRCI
• MULT: MUL, MULH, MULHSU, MULHU, DIV, DIVU, REM, REMU
• LSU: LW, LH, LHU, LB, LBU, SW, SH, SB

There's currently no way to keep it running in the GUI if you close the connection to the server, you can use the command line version, execute the run, come back later, close it with typing ctrl+c only once! and then, when it finished gracefully after some seconds, restore the session with make restore_run EXPERIMENT_DIR_TO_RESTORE=experiments/<dirname> & (also described in the 'make help')

Development

File locations, based on the example of an AND instruction:

in ibex/formal/signal_defs/declassification_sigs_assignments.sv: // AND logic[X_LEN-1:0] declass_source_gpr_regwr_AND_t0; assign declass_source_gpr_regwr_AND_t0 = u_ibex_core__rf_wdata_wb_ecc_o_t0;

in common/formal/signal_defs/declass_cond_reg.sv the CPU specific signal is assigned to the common gpr declassification signal struct for the AND: declass_AND_gpr_regwr, and subsequently to declasses_AND.

in common/formal/properties/checker_inst_data_leakage_legal.sv declasses_AND is passed to the checker: legal_data_leakage_taint_checker chk_legal_AND_op1(taint_start_cond_AND_op1, taint_stop_cond_AND_op1, op1_AND_t0, pc_tainted_instr, declasses_AND, abstract_op1, abstract_op1_stop_cond, op1_AND_fwd_sel_id, abstract_op1_prev);

The checker is declared in common/formal/assumptions/asm_taint_declass.sv. It constrains the generic signal declass_source_gpr_regwr_AND_t0 that reads from u_ibex_core__rf_wdata_wb_ecc_o_t0 whenever taint declassification should happen. Thus, it implicitely constrains u_ibex_core__rf_wdata_wb_ecc_o_t0 to be 0 ONLY if this signal is abstracted.

Declassification Contracts

The declassification contracts perform the taint path gating

Adding a new contract clause = adding a new declassification rule

To add a declassification contract clause that excludes an acceptable information flow from the check, proceed as follows:

• Identify the signal that shall be declassified, and add it as signal to be abstracted into the task creation command for the property for which it shall be declassified: verification/ibex/formal/scripts/tasks/(full_)task_creation_data_leakage_taint_checker_illegal.tcl
• Identify the condition when the declassification shall take place
• Optionally: add a copy signal into the design that reads the original driving logic of the signal to be declassified.
• Create a file in designname/formal/properties/declass_conditions and include it in designname/formal/properties/data_leakage.sv.
• In this file, define: declass_start_cond_, declass_stop_cond_, declass_source_t0, declass_source_prev, declass_pc_ (optional).
• In designname/formal/properties/data_leakage.sv add a declass_contract checker instantiation to the DECLASSIFICATION_CHECKER_INSTANTIATIONS macro

Method, based on csr declassification example

in ibex/formal/signal_defs/declassification_sigs_assignments.sv: assign declass_source_csr_CSRRS_t0 = u_ibex_core__cs_registers_i__dummy_instr_seed_o_t0; // used because csr_wdata_int is optimized out.

A copy of the signal that shall be declassified is created in the design: in ifi/ibex/designs/cellift_ibex_simple.sv assign dummy_instr_seed_o_t0 = 1036 | 1912; assign dummy_instr_seed_o_copy_t0 = 1036 | 1912;

in ifi/ibex/formal/properties/data_leakage_csr_inject.sv The copy is assigned to the signal that stores the prev (i.e., original) value of the signal that shall be sometimes declassified assign declass_source_prev_csr_t0 = u_ibex_core__cs_registers_i__dummy_instr_seed_o_copy_t0;

in ifi/common/formal/signal_defs/declass_cond_reg.sv The prev signal is assigned to the paramter struct: assign declass_CSRRW_csr = '{declass_start_cond_csr, declass_stop_cond_csr, declass_source_csr_CSRRW_t0, declass_source_prev_csr_t0, declass_pc_csr};

in /data/kceesay/workspace/ifi/common/formal/assumptions/asm_taint_declass.sv

we assume with an assumption: if (!declass_active) declass_source == declass_prev_source; that the values of declass source taint and declass_prev_source taint match. Since we abstract declass_source taint, it becomes disconnected from its original driving logic and we can control it completely via an assumption. If declassification is not active, we let the declass_source match the value of declass_prev_source, which is actually the original logic that was connected to declass_source.

we assume with an assumption: if (declass_active) declass_source == 0; that the declass_source taint is 0. Since we abstract declass_source taint, we can control it completely without affecting the original driving logic of this signal.

Instruction tracker

See the tracker files for explanations on how we implemented the instruction tracker per CPU. For a new CPU, implement a corresponding tracker.

• Ibex (with WB stage): verification/ibex/formal/properties/iuv_tracker_w_wb_stage.sv
• Ibex (without WB stage): verification/ibex/formal/properties/iuv_tracker_wo_wb_stage.sv
• Kronos: verification/kronos/formal/properties/iuv_tracker.sv

Setting up a new CPU

First, create the setup by adding a make target for the CPU into the main Makefile. Copy the target 'simpleooo', call it and run 'make '.

Next, we write the properties in formal/properties/data_leakage.sv: Copy that file from another CPU and replace the signal names for clk, reset, gprs, pc

For legal source checks, we need:

• a taint injection point (e.g. the GPRs)
• abstraction/taint injection condition for the taint injection point (we re-used the auto-generated conditions and setup from 𝜇CFI).
• declassification points (legal sources, e.g. the target GPR)
• declassification conditions = The condition when the instruction legally writes to the state element that stores the GPR data.
• declassification pc, which is used to compare with the IUV's PC

For illegal source checks, we need:

• A list of all architectural states
• All taint injection conditions for legal sources for all instructions

Additional experiments

Cache timing side channel (IBEX)

This experiment needs to be enabled by defining MODEL_MINIMAL_CACHE in ibex/designs/cellift_ibex_fix.sv.

Use the following command to demonstrate a timing side channel through a (modelled) cache. This command uses the verification/ibex/configurations/data_leakage_cache_example.mk configuration.

make run CONFIG=data_leakage_cache_example INSTR_TYPE=LSU TAINT_TYPE=LEGAL DESIGN_TYPE=FIX

Now prove confinement for a load instruction, e.g.,

prove -property {t_legal_data_leakage_taint_checker_LW_op1::cellift_ibex.cellift_ibex_fpv_bind.chk_legal_LW_op1.as_ifi_confinement}.

The property will fail and taint flow through the cache will be visible.

Define or comment DEBUG_IGNORE_CACHE_TAINT in ibex/designs/cellift_ibex_fix.sv to either ignore any taint flowing through the cache or not. This serves as a quick test to confirm that the timing side channel that we see indeed is caused by information flow through the cache module.