𝜇CFI - Formal Verification of Microarchitectural Control-flow Integrity

Welcome to the 𝜇CFI - Microarchitectural Control-flow Integrity - project. 𝜇CFI verifies whether instructions leak information about their operand data via timing side-channels, also known as constant time violation. 𝜇CFI further verfies whether instructions are manipulating the architectural control flow in a data-dependent way. Take a look at the paper here.

This repository contains the Yosys passes and formal properties for verifying 𝜇CFI. We also provide verification setup generation scripts and templates, as well as copies of the RISC-V CPUs that were verified to reproduce the results of our paper:

𝜇CFI - Formal Verification of Microarchitectural Control-flow Integrity.

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

@inproceedings{2024_ceesay-seitz_mucfi,
title="{𝜇}CFI: Formal Verification of Microarchitectural Control-flow Integrity",
author="Ceesay-Seitz, Katharina and Solt, Flavien and Razavi, Kaveh",
booktitle = {Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security},
year = {2024},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
doi = {10.1145/3658644.3690344},
url = {https://doi.org/10.1145/3658644.3690344},
location = {Salt Lake City, UT, USA},
series = {CCS '24},
keywords = {Hardware security; formal hardware verification; side-channels}
}

Abstract

Formal verification of hardware often requires the creation of clock-cycle accurate properties that need tedious and error-prone adaptations for each design. Property violations further require attention from verification engineers to identify affected instructions. This oftentimes manual effort hinders the adoption of formal verification 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 constanttime 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 architecturally known paths. We show that our verification approach is low effort (e.g., requires tagging six signals) while capturing all interactions 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.

Artifact reproduction

Setup

Dependencies

Yosys

First, install the following dependencies:

For example on Ubuntu Linux 22.04.4 LTS the following commands will install all prerequisites for building yosys and running our Python scripts:

$ sudo apt-get install build-essential clang bison flex \
	libreadline-dev gawk tcl-dev libffi-dev git \
	graphviz xdot pkg-config python3.12 libboost-system-dev \
	libboost-python-dev libboost-filesystem-dev zlib1g-dev

Python prerequisites

Python 3.12.3 regex==2024.5.15

Collecting CPU sources

Our verification setup generation flow expects a single Verilog source file where all the sources of the CPU are collected (e.g. cpus/<design_name>/cellift/generated/sv2v_out.v). The easiest way to reproduce our results is to use the sv2v_out.v file from a pregenerated directory. In that case you do not need to install cellift-meta tools.

Instrumenting your own CPU

If you also want to generate this file (e.g., for verifying another CPU), install cellift-meta, following the instructions in https://github.com/comsec-group/cellift-meta.

Alternatively, for only installing the minimum necessary tools, replicate the instructions in our Dockerfile, section 'CellIFT meta and tools'. The docker file expects that mucfi directory is placed next to it and certain sub-directories are zipped.

If you use the original cellift-meta, we need to make some modifications in cellift-meta:

• Make sure that the cellift setup uses our Yosys version mucfi_yosys. Our version has a small modification in the Veriolog backend (write_verilog), that prints some needed information about taint states.
• In cellift-meta/design-processing/common/yosys/instrument.ys.tcl, replace the "yosys write_verilog ..." command with this one: "yosys write_verilog -sv -attr2comment $VERILOG_OUTPUT". This adds comments to the output Verilog file with information about module names and taint states.
• For CellDFT, you need to pass the -data-flow flag to the cellift Yosys command.

Building from source

First, our Yosys version needs to be compiled (type make yosys in directory 'mucfi').

Local configuration

Adapt the paths in verification/common/local_config.mk.

Steps to reproduce the artifacts

There are two main parts to reproduce.

1. The formal setup generation, including taint condition generation.
2. Formal verification, which requires Jasper Gold (or any other formal property verification tool that can proof SystemVerilog Assertions).

Preparation

First, we need to prepare the design sources in a format as the CellIFT Yosys pass supports, ie. we need to translate it to Verilog. Enter a design directory, e.g. cpus/kronos/cellift. Source env.sh in cellift-meta, then source env.sh in cpus/kronos/cellift (if it exists). Then run make generated/sv2v_out.v.

Ibex

For Ibex, you can choose between the version with or without the fix for our CVE-2024-28365 by selecting the LOWRISC_IBEX_LOCATION in cpus/ibex/cellift/Makefile. You can further choose between different configurations by creating (or using) a specific configuration in e.g. cpus/ibex/opentitan/hw/vendor/lowrisc_ibex/rtl/ibex_top_opentitan_rst_slow_no_ls.sv and choosing TOP_MODULE ?= ibex_top_sec1_rst_slow_no_ls_custom in in cpus/ibex/cellift/Makefile.

Experiment 1 and 2

We describe both experiments in the following. They are executed by a single make target. E.g. for the Kronos CPU with CellIFT instrumentation: make kronos_ift or make kronos_dft. Examples are provided in Makefile. Please use Kronos for the reproduction. (The setup generation for the other CPUs should work, but there might be still some scripting errors here or there, we will improve them in the maintained github repo.)

Experiment 1:

In Section 5.2 and 6.4 we describe how to declassify legal information flows. This involves abstracting the select signal of forwarding multiplexer. This experiment is invoked by the make target `

1. automatically finds the forwarding multiplexers (based on the design and the definition of the following signals (in inputs/<design_name>_config.mk): forwarding outputs, register read signals),
2. stores the forwarding multiplexer select signals back into the config file
3. generates the declassification file for signal abstraction in the formal setup

Expected generated files:

• "FWD_MUX_SELECTS" added to inputs/<design_name>_config.mk
• verification/<design_name>/formal/scripts/declass.tcl (containing the mux selects)
• verification/<design_name>/formal/properties/taint_conditions

Note that the taint conditions may differ if the Yosys opt pass is called at different times (or not at all).

REPRODUCTION INSTRUCTIONS: delete the expected generated files and run: make <design>_ift (see Makefile for the examples for all 4 CPUs studied in the paper and for the dft version).

Finding the forwarding multiplexer select signals

A Python script first instruments the design with the existing Yosys pass CellIFT or our newly developed option CellDFT (CellIFT with -data-flow option, sources located in mucfi_yosys/cellift). Then it calls our Yosys pass 'find_fwd_mux_selects'. This pass takes as input the forwarding outputs, declassified signals (register read signals, register write signal) and the PC signal. It searches for potential forwarding multiplexers, and outputs their select signals if the declassification precondition is fulfilled. It also indicates whether there are additional forwarding multiplexers before the

Forwarding multiplexers found between the register file and the register read signals:

If there are forwarding multiplexers found between the register file and the register reading signal, then the FORWARDING_INPUT_BEFORE_REGREAD config must be set and the experiment needs to be rerun (so that these additional forwarding inputs are considered in the taint conditions, as described in the last paragraph of section 6).

Kronos

We add the additional forwarding input "u_if.u_rf.regwr_data".

Scarv

In Scarv additional forwarding multiplexer selects are found: \hzd_rs3_s*. Since our setup does not include instructions that read from rs3 (some non-standard crypto instructions), we do not add rs3_data as additional input. The path outgoing of forwarding outputs and going through \hzd_rs3_s* leads into the register file. That's why the precondition check is satisified. Since register readings signals for rs1/rs2 are not reading from the multiplexers with \hzd_rs3_s*, there are no additional forwarding inputs that need to be considered in the taint condition, so we leave the FORWARDING_INPUT_BEFORE_REGREAD field empty. As a check: If we add i_pipeline.i_gprs.rs3_data as additional input to the REGISTER_READ_SIGNALS, hzd_rs3_s4 is one of the