# SeSBI

**Repository Path**: dongshan-community/SeSBI

## Basic Information

- **Project Name**: SeSBI
- **Description**: The formal verification of a RISC-V SBI firmware. 
- **Primary Language**: Unknown
- **License**: MulanPSL-1.0
- **Default Branch**: main
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 25
- **Forks**: 23
- **Created**: 2025-09-26
- **Last Updated**: 2025-11-11

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# SeSBI —— 面向 RISC-V 的经形式化验证的 SBI 固件

> **SecuritySBI (SeSBI)**：一个以**形式化验证**驱动开发的 RISC-V SBI 固件实现，聚焦**安全启动、功能正确性与高可信性**。  
> 项目采用 **Isabelle/HOL（抽象规范层）** 与 **Dafny（可执行规范层）** 的**分层验证框架**，并引入**硬件语义/状态模拟**以提升验证效率与可移植性。

- 代码仓库（Gitee）：<https://gitee.com/yangyeqian/SeSBI>
- 适配架构：RISC-V（U/S/M 三特权级）
- 面向场景：可信启动、PMP（物理内存保护）配置校验、内核/固件研究教学与工程落地

---

## 为什么是 SeSBI？> 

- **更高可信**：以定理证明为核心的方法论，证明**不存在**违反规范的行为（而非仅“未测出”）。  
- **更简洁的实现**：以**最小可用功能集**为目标，减小攻击面；在等价功能下以更少的代码实现部分 SBI 接口。  
- **从启动第一阶段就可验证**：覆盖**启动流程正确性、模式切换、PMP 配置、时钟初始化**等关键属性。

---

## 核心亮点（Features）

- **分层形式化验证框架**
  - Isabelle/HOL：抽象规范层，统一固件系统语义与多特权级模型（U/S/M），证明关键安全/正确性性质。  
  - Dafny：可执行规范层，引入**RISC-V 硬件状态模拟**，对时钟、PMP、模式切换等进行可执行级性质验证。
- **关键属性已验证**
  - **启动与模式切换正确性**（含 `mstatus` 字段更新、`mret` 返回路径等）  
  - **PMP（物理内存保护）配置正确性**（对齐、2 的幂、NAPOT/NA4、边界与溢出检查）  
  - **时钟初始化正确性**（`SBI_SET_TIMER` 调用契约）
- **工程化价值**
  - 以 RISC-V SBI v3.0 为参照进行实现与验证；  
  - 通过**硬件语义抽象/模拟**降低验证开销，兼顾工程效率与学术严谨。

---

## 架构总览

> 以“抽象规范层 ↔ 可执行规范层”的**双层验证**为主线，辅以硬件语义与状态模拟。

```mermaid
flowchart LR
  A[需求/标准: RISC-V SBI v3.0] --> B[抽象规范层<br/>Isabelle/HOL]
  A --> C[可执行规范层<br/>Dafny]

  subgraph B1[抽象层验证]
    B2[统一系统语义/理论接口] --> B3[特权级模型U/S/M]
    B3 --> B4[性质证明: 启动/模式切换正确性]
    B3 --> B5[性质证明: PMP 配置约束]
  end

  subgraph C1[可执行层验证]
    C2[硬件状态模拟: CSR/PMP/Timer] --> C3[契约式方法验证]
    C3 --> C4[性质证明: 定时器/模式切换/PMP]
  end

  B --> D[SeSBI 固件实现]
  C --> D
  D --> E[QEMU/仿真环境运行与对比]
```

---

## 启动流程与系统调用（示意）

```mermaid
sequenceDiagram
  participant U as U-Mode App
  participant S as S-Mode OS
  participant M as SeSBI (M-Mode)
  participant HW as RISC-V HW

  U->>S: 系统调用请求
  S->>M: SBI ecall (e.g., set_timer / console)
  M->>HW: 访问CSR/定时器/UART/PMP 等
  M-->>S: 返回结果
  S-->>U: 完成调用

  Note over M: 启动阶段：<br/>1) 关中断<br/>2) 初始化栈<br/>3) 设置 mscratch/mstatus<br/>4) 跳转 sbi_main
```

> 启动过程与模式切换关键步骤给出形式化语义与定理证明（如 `init_sequence`、`insert_field/read_csr` 等），并对 `mstatus`、`pmp` 条目等进行了定义与验证。

---

## 与 OpenSBI 的定位对比（精要）

| 维度           | SeSBI                            | OpenSBI              |
| -------------- | -------------------------------- | -------------------- |
| 目标           | 高可信/可验证的最小实现          | 功能完备、平台广泛   |
| 代码体量       | 精简（降低攻击面）               | 较大（灵活但更复杂） |
| 正确性与安全性 | 形式化证明（抽象+可执行）        | 以传统测试为主       |
| 适配性         | 面向验证与教学/研究/工程安全基座 | 面向广泛工程部署     |

> 结论：**SeSBI 强在“可信与可证”**，OpenSBI 强在“功能广度与生态适配”。两者定位互补。

---

## 代码结构（示例性导览）

> 以论文描述的模块为线索，仓库中典型会包含以下（命名以实际仓库为准）：

```
SeSBI/
├─ 1.dfy  #dafny-sbi pmp正确配置验证
├─ 2.dfy  #dafny-可执行规范层：硬件状态模拟等正确性验证       
├─ 3.dfy  #dafny-sbi 串口初始化正确性验证                  
├─ 4.dfy   #dafny-sbi timer初始化正确性验证
├─ README.md  
├─ SeSBI_welcome.png   #成功启动打印图
├─ base.S             # 启动汇编：关中断/设栈/跳转等
├─ sbi_main.c          #M模式C代码(如 sbi_main.c)：UART/Timer/PMP/陷阱等
├─ sbi_main.thy      #isabelle-抽象规范层：硬件状态模拟
├─ security.thy      #isabelle-sbi串口初始化与timer初始化等正确性验证
└─ set_pmp.thy       #isabelle-sbi pmp正确配置验证
```

---

## 快速上手（Getting Started）

> 以下为典型流程指引，具体以仓库脚本为准。

### 1) 依赖环境

- RISC-V 交叉工具链（如 `riscv64-unknown-elf-gcc`）
- QEMU（支持 RISC-V）
- Dafny 4.x，Isabelle 2023（用于重放/扩展证明）
- GNU Make / CMake（视仓库脚本而定）

### 2) 构建固件

```bash
git clone https://gitee.com/yangyeqian/SeSBI.git
cd SeSBI
make        # 或 ./scripts/build.sh
```

### 3) 在 QEMU 中运行/调试

```bash
# 纯运行（示例）
qemu-system-riscv64 -machine virt -nographic   -kernel build/sesbi.elf

# 带 GDB
qemu-system-riscv64 -machine virt -nographic -s -S   -kernel build/sesbi.elf
# 另开终端：
riscv64-unknown-elf-gdb build/sesbi.elf -ex "target remote :1234"
```

### 4) 复现/扩展形式化证明

```bash
# Isabelle（抽象规范层）
isabelle jedit proofs/isabelle/SeSBI_Abstraction.thy

# Dafny（可执行规范层）
dafny /compile:0 proofs/dafny/*.dfy
```

---

## 已验证的关键性质（节选）

- **启动序列正确性**：如 `mscratch ≠ 0`、`mstatus` 字段设置满足切换前置条件等；
- **模式切换正确性**：`mstatus.MPP ← PRV_S`、`MPIE` 语义、`mret` 返回路径等；
- **PMP 配置正确性**：对齐、2 的幂、NAPOT/NA4、边界/越界检查与错误码约束；
- **时钟初始化正确性**：`SBI_SET_TIMER` 的后置条件成立（定时器值与返回状态）。  
  以上性质在抽象层（Isabelle/HOL）与可执行层（Dafny）分别给出模型、语义与定理证明。

---

## 实验与环境

- **虚拟化环境**：VMware + Ubuntu 20.04 LTS  
- **仿真器**：QEMU 4.2.0（配 GDB）  
- **证明工具**：Isabelle 2023（HOL），Dafny 4.0.0  
- **验证结果**：抽象层与可执行层对**启动/模式切换/PMP/时钟**等性质均通过证明器校验。

---

## 路线图（Roadmap）

- ✅ 启动/模式切换、PMP、时钟等关键性质的分层验证
- 🔜 扩展更多 SBI 接口与性质覆盖
- 🔜 层间**精化（refinement）关系**的系统性证明
- 🔜 更广平台/SoC 适配与工程集成

---

## 适用人群

- **高校/研究机构**：形式化方法教学与实验课；可信固件/内核研究  
- **工程团队**：需要可证明安全性的底层软件基座、供应链安全与合规  
- **社区开发者**：关注 RISC-V 生态、SBI 实现与形式化验证实践

---

## 许可协议与联系

- 许可协议：以仓库内 LICENSE 为准（若未注明，建议采用开源友好协议并在官网同步）。  
- 联系方式：请在 Gitee Issues 提交问题或建议：<https://gitee.com/yangyeqian/SeSBI/issues>