CEA-LIST/uArchiFI
GitHub: CEA-LIST/uArchiFI
这是一个结合处理器 RTL 和软件二进制文件的形式化验证工具，用于分析嵌入式系统在微架构层面对抗故障注入攻击的安全性。
Stars: 15 | Forks: 0
# µArchiFI
**µArchiFI** 是一个形式化工具，用于分析嵌入式系统对抗故障注入攻击的鲁棒性，它结合了处理器的 RTL、软件的二进制文件以及攻击者模型。µArchiFI 考虑了微架构与在处理器上运行的软件之间微妙的相互作用。对于包含故障注入对策的系统，µArchiFI 可以在给定攻击者模型的情况下形式化证明其安全性。如果无法证明，µArchiFI 可以返回反例，说明故障注入如何利用漏洞。
µArchiFI 使用 [Yosys](https://github.com/YosysHQ/yosys) 开源硬件综合环境来生成硬件和软件的形式化模型。这些模型被增强了故障注入功能，可以在空间、时间以及位效应方面进行控制。
此存储库包含 µArchiFI 现为 0.2 版本的源代码。最初的工具，即 0.1 版本，在论文 "*μArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections*" 中进行了描述（参见 [Publication](#publication)）。
## 章节
1. **[安装](#install-and-build)**
2. **[构建流程脚本](#building-flow-scripts)**
- [完整流程摘要](#scripts-workflow-summary)
- [自定义技巧](#customization-tips)
- [常见陷阱](#common-pitfalls)
- [推荐的流程检查](#recommended-workflow-checks)
3. **[Iterator CLI](#iterator-cli-usage)**
4. **[结果解读](#result-interpretation)**
5. **[出版物](#publication)**
6. **[许可证](#licence)**
## 概述
该存储库的结构如下：
- `src`:
- `passes`: `fault_rtlil` pass 的源代码，它被添加在 Yosys 基础设施中，用于评估电路对故障注入的鲁棒性。
- `tooling`: `iterator` 工具的源代码，负责启动模型检查器生成的 CEX 轨迹并提取信息，并根据发现的信息进行迭代。
- `examples`: 论文中评估的案例研究。
- `tests`: 针对 `fault_rtlil` pass 和 `iterator` 方法的测试。
# 安装与构建
µArchiFI 使用 Yosys (0.61)。所有操作均通过 Dockerfile 完成，该文件将生成一个包含所有工具和基础设施的镜像，准备好进行分析。要构建容器，可以使用 Podman 或 Docker。
1. **克隆仓库：**
```
git clone https://github.com/CEA-LIST/uArchiFI.git
cd uArchiFI
```
2. **构建镜像：**
```
podman build --tag uarchifi -f Dockerfile .
```
```
docker build --tag uarchifi -f Dockerfile .
```
3. **启动容器并挂载工作目录：**
```
podman run -it --name uarchifi -v :/root/work -w /root/work uarchifi
```
```
docker run -it --name uarchifi -v :/root/work -w /root/work uarchifi
```
4. **（可选）运行测试：**
在容器内部时：
```
cd /src
pip install pytest pytest-cov
pytest -v --tb=line --yosys-variant=0.61 ./tests/passes
pytest -v --tb=line ./tests/tooling/
```
# 构建流程脚本
流程脚本执行以下步骤：
1. 准备并规范化硬件设计
2. 运行周期精确仿真
3. 注入破坏者（saboteurs）并导出形式化验证模型
该流程是模块化的，可以适用于任何 RTL 设计。
## 脚本概述
| 阶段 | 脚本 | 目的 |
| ---- | ---------------- | ---------------------------------------- |
| 1 | `prep_pass.ys` | 设计准备与规范化 |
| 2 | `simu.ys` | RTL 仿真与波形生成 |
| 3 | `apply_faults.ys` | 故障注入与形式化模型导出 |
## 阶段 1 — 设计准备 (`prep_pass.ys`)
### 目标
* 加载 RTL 源文件
* 设置并规范化顶层模块
* 清理层次结构
* 导出中间的 RTLIL 表示形式
### 脚本解析
```
# 读取 SystemVerilog (支持 advanced constructs)
read_verilog -sv -defer -formal .v
# 设置 top module
prep -top
# 标准化 top name
rename -top
# 确保唯一的 module instances 用于优化
uniquify
hierarchy -top
# 导出 RTLIL
write_rtlil out/.il
```
### 关键概念
#### `-sv -defer -formal`
* `-sv`: 启用 SystemVerilog 特性
* `-defer`: 延迟细化（elaboration，适用于大型/多文件设计）
* `-formal`: 保留形式化构造（断言等）
#### `prep`
* 执行：
* 层次结构解析
* 进程降级
* 基本清理
#### `uniquify`
* 确保每个模块实例是唯一的
* 启用更好的优化和后续转换
#### 输出：RTLIL
* Yosys 使用的中间表示形式
* 仿真和破坏者注入的输入
## 阶段 2 — 仿真 (`simu.ys`)
### 目标
* 仿真设计
* 生成波形轨迹
* 为后续转换准备设计
### 脚本解析
```
read_rtlil out/.il
# 转换 async logic (REQUIRED)
select t:$check
async2sync
select -clear
# 运行 simulation
sim -zinit \
-clock clk \
-reset reset \
-rstlen 3 \
-n 12 \
-w \
-fst ./waves.fst
```
### 仿真选项说明
#### `-zinit`
* 将所有寄存器/存储器初始化为零
#### `-clock clk`
* 定义时钟信号
#### `-reset reset`
* 定义复位信号
#### `-rstlen 3`
* 复位信号在前 3 个周期内保持有效
#### `-n 12`
* 总共仿真 12 个周期
#### `-w`
* 将最终仿真状态写回为嵌入式设计的初始化状态
#### `-fst`
* 输出波形文件（可使用 GTKWave 等工具查看）
### 仿真后清理
```
select -module i:reset*
delete -input
setundef -undriven -zero
select -clear
```
#### 目的：
* 移除输入依赖关系
* 替换未定义的信号
* 为形式化流程准备设计
此部分**依赖于设计**，可能需要调整。
## 阶段 3 — 故障注入 (`apply_faults.ys`)
### 目标
* 向选定信号注入故障
* 为形式化验证准备设计
* 导出 SMT2 / BTOR2 模型
### 脚本解析
```
read_rtlil ./out/.il
plugin -i fault_rtlil
# 选择 fault targets
select
# 标记选中的 signals
setattr -set fault_signals 1
cd
# 展平设计 (needed for global fault control)
flatten
# 排除内部 flatten signals
select a:fault_signals=1 w:*$flatten* %d
# 注入 faults
fault_rtlil -cnt 3 -timing 1
# 优化
cd
opt
# 准备 formal export
async2sync
dffunmap
# 导出 models
write_btor -x out/.btor2
write_smt2 -wires out/.smt2
```
### 选择故障位置
示例：
```
select .* s:1:8 %i n:*clk %d n:*reset %d
```
#### 含义：
* `s:1:8` → 选择宽度为 1–8 的信号
* `%i` → 包含输入
* `n:*clk %d` → 排除时钟
* `n:*reset %d` → 排除复位
### `fault_rtlil` — 详细用法
#### 基本语法
```
fault_rtlil [options]
```
#### 故障类型
##### 瞬态（默认）
* 发生在特定周期
#### 时序控制
```
fault_rtlil -timing 10:20
```
* 故障在第 10 到 20 个周期之间激活
#### 故障效果
```
fault_rtlil -effect set
```
* 设置故障模型 -> 将信号强制置 1
| 选项 | 描述 |
| ---------------- | ----------------- |
| `set` | 强制信号为 1 |
| `reset` | 强制信号为 0 |
| `flip` | 按位取反 |
| `diff` | 任何不同于正确值的值 |
| `xor` | 与原始值进行异或 |
| `fixed ` | 强制特定值 |
#### 故障计数控制
```
fault_rtlil -cnt 3
```
* 设计中最多激活 3 个故障
#### 调试选项
##### 强制选择约束
```
fault_rtlil -bypass
```
### 为什么 `flatten` 很重要
### 输出格式
#### SMT2
* 用于 `yosys-smtbmc` 模型检查器
#### BTOR2
* 用于 `Pono` 模型检查器
## 脚本工作流摘要
```
RTL (Verilog/SystemVerilog)
↓
[prep_pass.ys]
↓
RTLIL
↓
[simu.ys]
↓
Simulated RTLIL + Waveforms
↓
[apply_faults.ys]
↓
Fault-injected model
↓
SMT2 / BTOR2 (Formal Verification)
```
## 自定义技巧
## 常见陷阱
## 推荐的工作流检查
# Iterator CLI 用法
`iterator` 命令使用 `yosys-smtbmc` 运行迭代有界模型检查（BMC）工作流，并在迭代之间自动提取反例（CEX）和细化约束。
## 命令语法
```
iterator [OPTIONS] BASE_DIR SMTLIB_INPUT ITERATIONS TIME_RANGE BMC_DEPTH
```
### 参数
| 参数 | 类型 | 描述 |
| --------------- | ------ | ------------------------------------------------------- |
| `BASE_DIR` | `TEXT` | 存储迭代结果、日志和约束的输出目录 |
| `SMTLIB_INPUT` | `TEXT` | `yosys-smtbmc` 使用的输入 SMTLIB v2 文件 |
| `ITERATIONS` | `INT` | 要执行的迭代次数 |
| `TIME_RANGE` | `TEXT` | 故障注入的时间窗口（例如 `0:10`） |
| `BMC_DEPTH` | `INT` | 模型检查器的深度边界 |
### 选项
| 选项 | 类型 | 默认值 | 描述 |
| ------------------ | ------ | ------- | ------------------------------------------- |
| `--run-time` | `INT` | `60` | 单次迭代的超时时间（分钟） |
| `--glob-time` | `INT` | `4` | 所有迭代的全局超时时间（小时） |
| `--debug`, `-d` | `FLAG` | `False` | 启用来自模型检查器的实时流式输出 |
| `--cycle-width` | `INT` | `10` | 解析 VCD 反例时使用的周期宽度 |
| `--solver`, `-s` | `TEXT` | `yices` | `yosys-smtbmc` 使用的 SMT 求解器 |
### 示例
```
iterator results/ design.smt2 5 0:10 20 \
--run-time 30 \
--glob-time 2 \
--solver yices
```
这将：
* 运行最多 5 次模型检查器迭代
* 使用 20 的 BMC 深度
* 提取时间范围 `0:10` 内的故障信号，这必须与 `fault_rtlil` pass 选项中指定的范围相匹配
* 将每次迭代限制为 30 分钟
* 如果在 2 小时内未完成，则停止整个过程
* 将所有输出存储在 `results/` 目录下
## 输出结构
每次迭代都会生成一个专门的子目录：
```
BASE_DIR/
├── constr.smtc # Accumulated constraints
├── results.json # Aggregated iteration results
├── iter_0/
│ ├── model_checker.log
│ ├── cex.vcd
│ └── cex_signals.json
├── iter_1/
│ └── ...
```
## 执行流程
对于每次迭代：
1. 使用 `yosys-smtbmc` 执行模型检查器
2. 如果发现反例：
* 解析 VCD 轨迹
* 提取触发故障的信号
* 生成新的 SMT 约束并追加
3. 如果未发现反例，迭代将在不细化的情况下完成
4. 如果满足以下条件，过程将提前停止：
* 发生超时
* 达到全局超时时间
# 示例
每个示例中都提供了一个 Makefile。有关详细信息，请参阅与每个用例关联的 README 文件。
- 用例 I：鲁棒软件：[README.md](./examples/1.robust_software/README.md)
- 用例 II：鲁棒硬件：[README.md](./examples/2.robust_hardware/README.md)
- 用例 III：加密软件：[README.md](./examples/3.crypto_software/README.md)
# 结果解读
有界模型检查会在增加验证步骤以达到目标边界之前，在特定验证步骤证明鲁棒性（针对给定的故障模型）：
```
# 使用 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
# 使用 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..
```
或者显示在特定步骤发现的反例。根据所使用的验证工具，可能有不同的格式：
```
# 使用 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
...
# 使用 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
```
# 贡献
参见 [CLA](./CLA.txt)。
# 出版物
Tollec, S., Asavoae, M., Couroussé, D., Heydemann, K., Jan, M. [μArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections](https://repositum.tuwien.at/handle/20.500.12708/188805). *Proc. 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023*, pp. 101–109.
# 许可证
除非另有说明，否则本存储库中的所有内容均受 GNU Lesser General Public License 版本 2.1 保护（全文参见 [LICENSE](./LICENSE.txt)）。
阶段 1 — 设计准备 (prep_pass.ys)
- [目标](#objective) - [脚本解析](#script-breakdown) - [关键概念](#key-concepts)阶段 2 — 仿真 (simu.ys)
- [目标](#objective-1) - [脚本解析](#script-breakdown-1) - [仿真选项说明](#simulation-options-explained) - [仿真后清理](#post-simulation-cleanup)阶段 3 — 故障注入 (apply_faults.ys)
- [目标](#objective-2) - [脚本解析](#script-breakdown-2) - [选择故障位置](#selecting-fault-locations) - [`fault_rtlil` — 详细用法](#fault_rtlil-detailed-usage) - [为什么 `flatten` 很重要](#why-flatten-is-important) - [输出格式](#output-formats)Iterator CLI
- [Iterator CLI 用法](#iterator-cli-usage) - [参数](#arguments) - [选项](#options) - [示例](#example) - [输出结构](#output-structure) - [执行流程](#execution-flow)标签：CodeQL, RTL仿真, Yosys, 二进制分析, 云安全运维, 侧信道攻击, 反制措施验证, 安全评估工具, 嵌入式系统安全, 形式化建模, 形式化验证, 微架构分析, 故障注入攻击, 硬件安全, 硬件综合, 请求拦截, 软硬件协同验证, 逆向工具, 鲁棒性分析