µArchiFI

µ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).

Sections

1. Installation

2. Building flow scripts

   <details> <summary>Stage 1 — Design Preparation (prep_pass.ys)</summary>
   • Objective
   • Script Breakdown
   • Key Concepts
   </details> <details> <summary>Stage 2 — Simulation (simu.ys)</summary>
   • Objective
   • Script Breakdown
   • Simulation Options Explained
   • Post-Simulation Cleanup
   </details> <details> <summary>Stage 3 — Fault Injection (apply_faults.ys)</summary>
   • Objective
   • Script Breakdown
   • Selecting Fault Locations
   • fault_rtlil — Detailed Usage
   • Why flatten is Important
   • Output Formats
   </details>
   • Full Workflow Summary
   • Customization Tips
   • Common Pitfalls
   • Recommended Workflow Checks

3. Iterator CLI

   <details> <summary>Iterator CLI</summary>
   • Iterator CLI Usage
   • Arguments
   • Options
   • Example
   • Output Structure
   • Execution Flow
   </details>

4. Result interpretation

5. Publication

6. Licence

---

Overview

The repository is structured as follows:

• src:
  • passes: Source code of the fault_rtlil pass, which is added within the Yosys infrastructure for evaluating circuit robustness against fault injections.
  • tooling: Source code of the iterator tool, 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 the fault_rtlil pass and the iterator methods.

Install and Build

µ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.

1. Clone the repo:

git clone https://github.com/CEA-LIST/uArchiFI.git

cd uArchiFI

2. Build the image:

podman build --tag uarchifi -f Dockerfile .

docker build --tag uarchifi -f Dockerfile .

3. 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 

4. (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/

Building flow scripts

The flow scripts execute the following steps:

1. Prepare and normalize a hardware design
2. Run cycle-accurate simulation
3. Inject saboteurs and export formal verification models

The flow is modular and can be adapted to any RTL design.

---

Overview of Scripts

| 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 |

---

Stage 1 — Design Preparation (prep_pass.ys)

Objective

• Load RTL sources
• Set and normalize the top module
• Clean hierarchy
• Export an intermediate RTLIL representation

---

Script Breakdown

# 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

---

Key Concepts

-sv -defer -formal

• -sv: Enables SystemVerilog features
• -defer: Delays elaboration (useful for large/multi-file designs)
• -formal: Keeps formal constructs (assertions, etc.)

prep

• Performs:

  • Hierarchy resolution
  • Process lowering
  • Basic cleanup

uniquify

• Ensures each module instance is unique
• Enables better optimization and transformations later

Output: RTLIL

• Intermediate representation used by Yosys
• Input for simulation and saboteurs injection

---

Stage 2 — Simulation (simu.ys)

Objective

• Simulate the design
• Generate waveform traces
• Prepare design for further transformations

---

Script Breakdown

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

Simulation Options Explained

-zinit

• Initialize all registers/memories to zero

-clock clk

• Defines the clock signal

-reset reset

• Defines reset signal

-rstlen 3

• Reset stays active for first 3 cycles

-n 12

• Simulate 12 cycles total

-w

• Write back final simulation state as embedded design init state

-fst

• Output waveform file (viewable with tools like GTKWave)

Post-Simulation Cleanup

select -module <top_module> i:reset*
delete -input
setundef -undriven -zero
select -clear

Purpose:

• Remove input dependencies
• Replace undefined signals
• Prepare design for formal flows

This section is design-dependent and may require adaptation.

---

Stage 3 — Fault Injection (apply_faults.ys)

Objective

• Inject faults into selected signals
• Prepare design for formal verification
• Export SMT2 / BTOR2 models

Script Breakdown

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

Selecting Fault Locations

Example:

select <top_module>.* s:1:8 %i n:*clk %d n:*reset %d

Meaning:

• s:1:8 → select signals of width 1–8
• %i → include inputs
• n:*clk %d → exclude clock
• n:*reset %d → exclude reset

---

fault_rtlil — Detailed Usage

Basic Syntax

fault_rtlil [options]

---

Fault Types

Transient (default)

• Occurs at a specific cycle

---

Timing Control

fault_rtlil -timing 10:20

• Fault active between cycles 10 and 20

---

Fault Effects

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 Count Control

fault_rtlil -cnt 3

• Maximum 3 faults activated in the design

---

Debug Options

Force selection constraints

fault_rtlil -bypass

---

Why flatten is important

[!NOTE]

Required for:

• Global fault counters
• Timing-controlled faults Creates a single-level design

---

Output Formats

SMT2

• For yosys-smtbmc model checker

BTOR2

• For Pono model checker

---

Scripts Workflow Summary

RTL (Verilog/SystemVerilog)
        ↓
  [prep_pass.ys]
        ↓
      RTLIL
        ↓
    [simu.ys]
        ↓
Simulated RTLIL + Waveforms
        ↓
[apply_faults.ys]
        ↓
Fault-injected model
        ↓
SMT2 / BTOR2 (Formal Verification)

---

Customization Tips

[!TIP]

• Adapt <top_module> to your design
• Tune simulation cycles (-n)
• Adjust fault selection expressions
• Always validate selections with select -list

Common Pitfalls

[!CAUTION]

• Forgetting `a