µArchiFI is a formal tool for analyzing the robustness of embedded systems against fault injection attacks by combining the RTL of a processor, the binary of a software, and an attacker model. µArchiFI takes into account the subtle interactions between the microarchitecture and the software running on the processor. µArchiFI can formally prove the security, for a given attacker model, of a system embedding countermeasures to fault injections. If not proven, µArchiFI can return counterexamples illustrating how fault injection can leverage vulnerabilities.
µArchiFI uses the Yosys open-source hardware synthesis environment to produce formal models of both the hardware and the software. These models are enriched with fault injection capabilities that can be controlled spatially, temporally and in terms of bit effects.
This repository contains the source code of µArchiFI now in version 0.2. The initial tool, i.e. release 0.1, was described in the paper "μArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections" (see Publication).
-
Stage 1 — Design Preparation (prep_pass.ys)
Stage 2 — Simulation (simu.ys)
Stage 3 — Fault Injection (apply_faults.ys)
-
Iterator CLI
The repository is structured as follows:
src:passes: Source code of thefault_rtlilpass, which is added within the Yosys infrastructure for evaluating circuit robustness against fault injections.tooling: Source code of theiteratortool, which is responsible for launching and extracting information from CEX traces generated by the model checker and iterating with the found information
examples: Case studies evaluated in the paper.tests: Tests for both thefault_rtlilpass and theiteratormethods.
µArchiFI uses Yosys (0.61). Everything is done with the Dockerfile that will generate an image with all the tools and infrastructure needed to be ready for analysis. To build the container one can use either Podman or Docker.
- Clone the repo:
git clone https://github.com/CEA-LIST/uArchiFI.git
cd uArchiFI
- Build the image:
podman build --tag uarchifi -f Dockerfile .
docker build --tag uarchifi -f Dockerfile .
- Spin up the container and attach the working directory:
podman run -it --name uarchifi -v <work_dir>:/root/work -w /root/work uarchifi
docker run -it --name uarchifi -v <work_dir>:/root/work -w /root/work uarchifi
- (optional) Run tests:
While inside the container:
cd /src
pip install pytest pytest-cov
pytest -v --tb=line --yosys-variant=0.61 ./tests/passes
pytest -v --tb=line ./tests/tooling/
The flow scripts execute the following steps:
- Prepare and normalize a hardware design
- Run cycle-accurate simulation
- Inject saboteurs and export formal verification models
The flow is modular and can be adapted to any RTL design.
| Stage | Script | Purpose |
|---|---|---|
| 1 | prep_pass.ys |
Design preparation and normalization |
| 2 | simu.ys |
RTL simulation and waveform generation |
| 3 | apply_faults.ys |
Fault injection and formal model export |
- Load RTL sources
- Set and normalize the top module
- Clean hierarchy
- Export an intermediate RTLIL representation
# Read SystemVerilog (supports advanced constructs)
read_verilog -sv -defer -formal <input_design>.v
# Set top module
prep -top <top_module>
# Normalize top name
rename -top <top_module>
# Ensure unique module instances for optimization
uniquify
hierarchy -top <top_module>
# Export RTLIL
write_rtlil out/<design>.il
-sv: Enables SystemVerilog features-defer: Delays elaboration (useful for large/multi-file designs)-formal: Keeps formal constructs (assertions, etc.)
-
Performs:
- Hierarchy resolution
- Process lowering
- Basic cleanup
- Ensures each module instance is unique
- Enables better optimization and transformations later
- Intermediate representation used by Yosys
- Input for simulation and saboteurs injection
- Simulate the design
- Generate waveform traces
- Prepare design for further transformations
read_rtlil out/<design>.il
# Convert async logic (REQUIRED)
select t:$check
async2sync
select -clear
# Run simulation
sim -zinit \
-clock clk \
-reset reset \
-rstlen 3 \
-n 12 \
-w \
-fst ./waves.fst
- Initialize all registers/memories to zero
- Defines the clock signal
- Defines reset signal
- Reset stays active for first 3 cycles
- Simulate 12 cycles total
- Write back final simulation state as embedded design init state
- Output waveform file (viewable with tools like GTKWave)
select -module <top_module> i:reset*
delete -input
setundef -undriven -zero
select -clear
- Remove input dependencies
- Replace undefined signals
- Prepare design for formal flows
This section is design-dependent and may require adaptation.
- Inject faults into selected signals
- Prepare design for formal verification
- Export SMT2 / BTOR2 models
read_rtlil ./out/<design>.il
plugin -i fault_rtlil
# Select fault targets
select <selection_expression>
# Mark selected signals
setattr -set fault_signals 1
cd
# Flatten design (needed for global fault control)
flatten
# Exclude internal flatten signals
select a:fault_signals=1 w:*$flatten* %d
# Inject faults
fault_rtlil -cnt 3 -timing 1
# Optimize
cd
opt
# Prepare for formal export
async2sync
dffunmap
# Export models
write_btor -x out/<design>.btor2
write_smt2 -wires out/<design>.smt2
Example:
select <top_module>.* s:1:8 %i n:*clk %d n:*reset %d
s:1:8→ select signals of width 1–8%i→ include inputsn:*clk %d→ exclude clockn:*reset %d→ exclude reset
fault_rtlil [options]
- Occurs at a specific cycle
fault_rtlil -timing 10:20
- Fault active between cycles 10 and 20
fault_rtlil -effect set
- Fault model set -> will force signal to 1
| Option | Description |
|---|---|
set |
Force signal to 1 |
reset |
Force signal to 0 |
flip |
Bitwise inversion |
diff |
Any value different from correct |
xor |
XOR with original |
fixed <value> |
Force specific value |
fault_rtlil -cnt 3
- Maximum 3 faults activated in the design
fault_rtlil -bypass
Note
Required for:
- Global fault counters
- Timing-controlled faults Creates a single-level design
- For
yosys-smtbmcmodel checker
- For
Ponomodel checker
RTL (Verilog/SystemVerilog)
↓
[prep_pass.ys]
↓
RTLIL
↓
[simu.ys]
↓
Simulated RTLIL + Waveforms
↓
[apply_faults.ys]
↓
Fault-injected model
↓
SMT2 / BTOR2 (Formal Verification)
Tip
- Adapt
<top_module>to your design - Tune simulation cycles (
-n) - Adjust fault selection expressions
- Always validate selections with
select -list
Caution
- Forgetting
async2sync→ incorrect simulation/formal behavior - Overly broad
select→ excessive fault injection - Missing
flattenwith-cnt→ invalid model - Not excluding clock/reset → meaningless faults
Tip
- Run
hierarchy -checkduring preparation - Use small simulation cycles first
- Visualize
.fstwaveform outputs - Validate fault coverage incrementally
The iterator command runs an iterative bounded model checking (BMC) workflow using yosys-smtbmc, with automatic counterexample (CEX) extraction and constraint refinement between iterations.
iterator [OPTIONS] BASE_DIR SMTLIB_INPUT ITERATIONS TIME_RANGE BMC_DEPTH| Argument | Type | Description |
|---|---|---|
BASE_DIR |
TEXT |
Output directory where iteration results, logs, and constraints are stored |
SMTLIB_INPUT |
TEXT |
Input SMTLIB v2 file used by yosys-smtbmc |
ITERATIONS |
INT |
Number of iterations to execute |
TIME_RANGE |
TEXT |
Time window for fault injection (e.g. 0:10) |
BMC_DEPTH |
INT |
Depth bound for the model checker |
| Option | Type | Default | Description |
|---|---|---|---|
--run-time |
INT |
60 |
Timeout for a single iteration (in minutes) |
--glob-time |
INT |
4 |
Global timeout across all iterations (in hours) |
--debug, -d |
FLAG |
False |
Enable live streaming output from the model checker |
--cycle-width |
INT |
10 |
Cycle width used when parsing VCD counterexamples |
--solver, -s |
TEXT |
yices |
SMT solver used by yosys-smtbmc |
iterator results/ design.smt2 5 0:10 20 \
--run-time 30 \
--glob-time 2 \
--solver yicesThis will:
- Run up to 5 iterations of the model checker
- Use a BMC depth of 20
- Extract fault signals in the time range
0:10this has to match the range specified infault_rtlilpass options - Limit each iteration to 30 minutes
- Stop the full process after 2 hours if not completed
- Store all outputs under the
results/directory
Each iteration produces a dedicated subdirectory:
BASE_DIR/
├── constr.smtc # Accumulated constraints
├── results.json # Aggregated iteration results
├── iter_0/
│ ├── model_checker.log
│ ├── cex.vcd
│ └── cex_signals.json
├── iter_1/
│ └── ...
For each iteration:
-
The model checker is executed using
yosys-smtbmc -
If a counterexample is found:
- The VCD trace is parsed
- Fault-triggering signals are extracted
- New SMT constraints are generated and appended
-
If no counterexample is found, the iteration completes without refinement
-
The process stops early if:
- A timeout occurs
- The global timeout is reached
Note
- The constraint file (
constr.smtc) is incrementally updated across iterations - Debug mode (
--debug) streams solver output directly to the terminal - Results are serialized to
results.jsonfor post-processing or analysis
Within each example, a Makefile is provided. See the README file associated to each use case for details.
- Use case I: Robust Software: README.md
- Use case II: Robust Hardware: README.md
- Use case III: Crypto Software: README.md
Bounded model checking either proves the robustness (for a given fault model) at a specific verification step before incrementing it to reach the targeted bound:
# With Pono
[2024-09-23 11:54:11.955674] BMC checking at bound: 55
[2024-09-23 11:54:11.955683] BMC reached_k = 54, i = 55
[2024-09-23 11:54:11.955692] BMC adding transition for j-1 = 54
[2024-09-23 11:54:11.979838] BMC adding bad state constraint for j = 55
[2024-09-23 11:54:12.832495] BMC check at bound 55 unsatisfiable
# With Yosys-smtbmc
[2024-09-23 16:09:18.644380] ## 0:02:30 Checking assumptions in step 69..
[2024-09-23 16:09:23.582891] ## 0:02:35 Checking assertions in step 69..
[2024-09-23 16:10:31.020274] ## 0:03:43 Checking assumptions in step 70..
[2024-09-23 16:10:36.504236] ## 0:03:48 Checking assertions in step 70..
or shows a counter-example found at a specific step. Different formats are possible depending on the verification tool being used:
# With Pono
[2024-09-23 11:55:09.533820] BMC checking at bound: 70
[2024-09-23 11:55:09.533829] BMC reached_k = 69, i = 70
[2024-09-23 11:55:09.533838] BMC adding transition for j-1 = 69
[2024-09-23 11:55:09.567581] BMC adding bad state constraint for j = 70
[2024-09-23 11:55:54.579887] BMC check at bound 70 satisfiable
[2024-09-23 11:55:54.579976] BMC saving reached_k_ = 69
[2024-09-23 11:55:54.579988] BMC get cex upper bound: lower bound = 70, upper bound = 70
[2024-09-23 11:55:54.580613] BMC get cex upper bound, checking value of bad state constraint j = 70
[2024-09-23 11:55:54.580650] BMC get cex upper bound, found at j = 70
[2024-09-23 11:55:54.580662] BMC permanently blocking interval [start,end] = [71,70]
[2024-09-23 11:55:54.580672]
[2024-09-23 11:55:54.580682] BMC binary search, cex found in interval [reached_k+1,upper_bound] = [70,70]
[2024-09-23 11:55:54.580692] BMC interval has length 1, skipping search for shortest cex
[2024-09-23 11:56:25.848295] sat
[2024-09-23 11:56:25.848421] b0
[2024-09-23 11:56:25.875069] #0
[2024-09-23 11:56:25.875191] 0 00000000000000000000000000000000 core_i.id_stage_i.alu_operand_a_ex_o@0
[2024-09-23 11:56:25.875206] 1 00000000000000000000000001010101 core_i.id_stage_i.alu_operand_b_ex_o@0
[2024-09-23 11:56:25.878498] 2 1 state223@0
[2024-09-23 11:56:25.882278] 3 0 state229@0
[2024-09-23 11:56:25.885516] 4 1 state250@0
[2024-09-23 11:56:25.888446] 5 0 state254@0
[2024-09-23 11:56:25.892911] 6 00 state257@0
[2024-09-23 11:56:25.892946] 7 00000000000000000000000000000000 core_i.id_stage_i.alu_operand_c_ex_o@0
[2024-09-23 11:56:25.893987] 8 00 state273@0
[2024-09-23 11:56:25.894016] 9 001 state302@0
[2024-09-23 11:56:25.894026] 10 1010 state309@0
[2024-09-23 11:56:25.894034] 11 0 state315@0
[2024-09-23 11:56:25.894042] 12 1010 state321@0
[2024-09-23 11:56:25.894050] 13 101 state328@0
[2024-09-23 11:56:25.894058] 14 1110 state335@0
[2024-09-23 11:56:25.894066] 15 1 state341@0
[2024-09-23 11:56:25.894074] 16 1101 state348@0
[2024-09-23 11:56:25.894082] 17 000 state355@0
[2024-09-23 11:56:25.894090] 18 0 state361@0
[2024-09-23 11:56:25.894097] 19 00 state367@0
[2024-09-23 11:56:25.894105] 20 0 state373@0
[2024-09-23 11:56:25.894113] 21 0 state379@0
[2024-09-23 11:56:25.894121] 22 0 state385@0
[2024-09-23 11:56:25.894129] 23 000000 state392@0
[2024-09-23 11:56:25.894137] 24 0 state398@0
...
# With Yosys-smtbmc (with a counter-example written in the VCD format)
[2024-09-23 16:10:36.504236] ## 0:03:48 Checking assertions in step 70..
[2024-09-23 16:11:36.475702] ## 0:04:48 BMC failed!
[2024-09-23 16:11:36.475775] ## 0:04:48 Assert failed in cv32e40p_wrapper: src/cv32e40p_verifypin_v7.v:9056.4-9074.3|src/cv32e40p_verifypin_v7.v:9142.85-9143.34|src/cv32e40p_verifypin_v7.v:9767.4-9781.3 ($flatten/ram_i./dp_ram_i.$assert$src/cv32e40p_verifypin_v7.v:9142$8010)
[2024-09-23 16:11:36.475788] ## 0:04:48 Writing trace to VCD file: .../uArchiFI/usecases/1.robust_software//out/counter_example.vcd
[2024-09-23 16:11:48.421869] ## 0:05:00 Status: FAILED
See CLA.
Tollec, S., Asavoae, M., Couroussé, D., Heydemann, K., Jan, M. μArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections. Proc. 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023, pp. 101–109.
Unless otherwise noted, everything in this repository is covered by the GNU Lesser General Public License, version 2.1 (see LICENSE for full text).