From 1aadf623be6d65e219b59b0a1512cb64f12e8944 Mon Sep 17 00:00:00 2001 From: DslsDZC Date: Mon, 10 Aug 2026 19:21:50 +0800 Subject: [PATCH] =?UTF-8?q?docs:=20=E6=8C=87=E9=92=88=E5=AE=89=E5=85=A8?= =?UTF-8?q?=E8=AE=BE=E8=AE=A1=E5=AE=9A=E8=AE=BA=E2=80=94=E2=80=94=E7=B1=BB?= =?UTF-8?q?=E5=9E=8B=E5=8F=8C=E5=85=B3=E8=87=AA=E5=8A=A8=E9=AA=8C=E8=AF=81?= =?UTF-8?q?=20+=20crasm=20=E7=A1=AC=E4=BB=B6=E6=8F=8F=E8=BF=B0=E8=A1=A8=20?= =?UTF-8?q?+=20TODO=20bug=207?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - docs/crasm.md: 特权级安全模型改版——硬件描述表（标准表/厂商表/表外）自动验证，unsafe 只管表外入口 - docs/pointer-model.md: unsafe 表删类型双关行（图只认字节可推导）；新增类型双关节；2026-08-10 设计定论（不扩展 0x 直接指内部地址，YAGNI） - TODO.md: 预存 bug 7 类型双关验证缺口（DEREF 宽度检查 + asp 无主机制） --- TODO.md | 13 +++++++++++++ docs/crasm.md | 29 ++++++++++++++++++++++++----- docs/pointer-model.md | 19 ++++++++++++++++++- 3 files changed, 55 insertions(+), 6 deletions(-) diff --git a/TODO.md b/TODO.md index 43f0e05..9f26d61 100644 --- a/TODO.md +++ b/TODO.md @@ -132,6 +132,19 @@ RVSDG 式嵌套 region 已落地（规格 docs/superpowers/specs/2026-08-08-regi - `lexer.cr` 浮点/`..` 范围修复（main 已有）→ 核对 lexer.md 是否已反映 - 完成后需重跑 `python3 tools/pseudocode_check.py` 并更新相应文档的源行数标注 +### 7. 类型双关验证缺口（2026-08-10 记） +- 背景：设计讨论定论——指针模型扩展收敛：**"程序内部地址直接指"（0x 字面量指内部对象）不做**（YAGNI：内部对象用 `&` 取址更优——无漂移/类型全/验证无条件；外部契约地址 unsafe 已够用；0x 字面量仅保留 unsafe 外部入口角色）；**类型双关保留**——图只认字节（pts/offset/alloc_size 全字节级，无类型检查），双关在图层天然合法，验证 = 边界 + 宽度 +- 现状核实（源码）： + - checker EXPR_AS **无类型兼容检查**（checker.cr:2188 仅推断内层 + 返回目标类型）→ `*(float*)&i` 已放行 + - cast 透传（ir_gen.cr:1595 EXPR_AS 返回内层表达式）→ provenance 边不断 + - DEREF 边界检查只查 `off >= alloc_size`（provenance_verify.cr:58-64）→ 越界双关照拦 + - DEREF 节点不携带类型（ir_gen.cr:735 `emit(IR_DEREF, dv, inner_var, 0, 0, 0)`，type_kind=0）→ 访问宽度无从查 + - **asp 无主机制**：checker.cr:404/1451 写入 TYP_PTR 的 asp 标志（unsafe 块内 = 外部地址空间），全仓库无任何消费点——`0x... as *int` 在 safe 代码同样放行，安全语义未落地 +- 待修： + 1. DEREF 宽度检查：`off + width <= alloc_size`（width 从 s1 指针变量的 TYP_PTR 指向类型经 type_size（ir_gen.cr:295）取；DEREF 的 type_kind 是占位 0，需从变量类型推导或改 emit 传真实类型） + 2. asp 机制收尾：完成（asp=1 指针的 DEREF 要求 unsafe 包裹）或删除（当前写入无人消费，是隐患） +- 参考：docs/pointer-model.md（unsafe 边界表已删"类型双关"行 + 新增类型双关节 + 2026-08-10 设计定论） + ## 待实现特性 ### 控制流自动惰性（2026-08-09 记） diff --git a/docs/crasm.md b/docs/crasm.md index c099efe..f44f5ea 100644 --- a/docs/crasm.md +++ b/docs/crasm.md @@ -77,13 +77,15 @@ extern fn port_read(addr: u64) fn port_read(addr: u64) -> u8 { ### 特权指令固定集 特权指令是**标准手册定义的有限固定集**（几十条）——固定 = 约束有限 = 可形式化 = 可验证。 +标准硬件布局同理：标准手册定义的寄存器/MMIO 区域也是固定集 → 可建表验证（见下文硬件描述表）。 ## 示例 ```crasm unsafe fn port_write(addr: u64, val: u8) { // 用法验证：addr 必须 64 位、val 必须 8 位（与 MMIO 寄存器宽度匹配） - // 副作用隔离：写入后的硬件行为由人工保证 + // 硬件表验证：addr 落在标准/厂商表声明区域 → 自动（归属/宽度/对齐） + // 表外隔离：仅表外硬件行为与动态时序由人工保证 mmio_write(addr, val); } ``` @@ -95,7 +97,7 @@ unsafe fn port_write(addr: u64, val: u8) { | 级 | 指令 | 验证策略 | |---|---|---| | 普通级 | 数据传输/算术/分支/内存操作/地址计算 | **自动验证**：寄存器生命周期 + 地址 provenance/边界（复用现有指针模型 pass）——"绝大多数可验证" | -| 特权级 | mmio/barrier/irq/swap_context/halt | **用法验证**（自动）：参数类型/宽度、放置规则、指令间约束（固定集 → 可形式化）；**副作用隔离**（unsafe 边界）：硬件行为/时序超出编译期验证范围，人工保证 | +| 特权级 | mmio/barrier/irq/swap_context/halt | **用法验证**（自动）：参数类型/宽度、放置规则、指令间约束（固定集 → 可形式化）；**硬件表验证**（自动）：地址落在标准/厂商表声明区域、寄存器宽度匹配；**表外隔离**（unsafe 边界）：表外硬件行为与动态时序人工保证 | ### 寄存器生命周期规则（新 pass，.crasm 专用） @@ -107,12 +109,29 @@ unsafe fn port_write(addr: u64, val: u8) { | 宽度一致 | 运算操作数宽度匹配（8/16/32/64） | `%0(8bit) := %1(64bit) + 1` | | 分支一致性 | goto 目标存在；if 条件是条件寄存器 | `if %0 == 0 goto missing` | +### 硬件描述表：标准部分自动验证 + +"硬件有的地方是标准的，也是可以验证的"——特权访问的验证对象分三层： + +| 层 | 覆盖 | 验证依据 | +|---|---|---| +| 标准表 | 公开标准硬件：UART 16550、x86 APIC/IOAPIC、PCIe ECAM、CMOS RTC | 标准手册 → 形式化表（地址范围、寄存器宽度、读写语义） | +| 厂商表 | SoC 外设：GPIO、SPI 控制器等 | 厂商手册 → 与标准表同构的形式化描述 | +| 表外 | 自定义 FPGA 逻辑、非标准设备 | unsafe 入口标注一次，人工保证 | + +mmio_read/write 的地址落在表内 → 编译器自动验证区域归属、寄存器宽度匹配、对齐合法。 +这与指针模型同构：unsafe 标注的是"图边界入口"（外部地址、FFI 返回），进入图内编译器 +重新获得追踪权——硬件表让标准部分拿回自动验证，unsafe 只承担表外入口。 + +无论硬件多标准，**动态行为**（时序、中断延迟、握手时序）都超出编译期验证范围， +始终位于表外，人工保证。 + ### 与现有验证的关系 - 寄存器规则：新 pass（`.crasm` 专用——虚拟寄存器是抽象层概念） - 地址/内存验证：复用 PointerAnalysis / RegionCheck / ProvenanceVerify （`.crasm` 的 `load [addr]` 转成与 IR 相同的 provenance 检查） -- 特权用法验证：固定指令集约束表（参数宽度/放置规则），pass 检查 +- 特权用法验证：固定指令集约束表（参数宽度/放置规则）+ 硬件描述表（区域/宽度/对齐），pass 检查 - 错误报告：走新错误码体系（验证类，挂错误码规格类别表，实现时定归属） ## 交互接口 @@ -172,8 +191,8 @@ x86 mov / arm ldr）——映射正确性由固定表保证。 - 模拟器/调试器支持 - .crasm 的 C 生态兼容（新生态无义务） -- 指令级时序验证（超出编译期验证范围） -- 特权指令副作用验证（隔离，人工保证） +- 指令级时序验证（动态行为无论硬件多标准都超出编译期验证范围） +- 表外硬件行为验证（unsafe 隔离，人工保证——表内标准部分仍自动验证） ## 当前状态 diff --git a/docs/pointer-model.md b/docs/pointer-model.md index c5c8f7d..e15818a 100644 --- a/docs/pointer-model.md +++ b/docs/pointer-model.md @@ -185,7 +185,18 @@ fail → panic | 外部硬件地址 | `0x7fff0000 as *int` 没有 ALLOC 节点 | | FFI 返回值 | 外部函数返回的指针没有 Core 的 provenance | | inline assembly | 汇编的输出指针没有来源 | -| `unsafe` 类型双关 | 违反类型系统假设，编译器无法推导 | + +### 类型双关 + +`*(float*)&i` **不需要 unsafe**。图的内存模型是"字节序列 + 宽度 + 边界"——provenance +（alloc 归属）、offset（字节偏移）、alloc_size（字节大小）全部与类型无关，类型只是 +DEREF 处的"视图"。cast 在图里无节点（ir_gen 透传），provenance 边不断： + +- 双关合法判据 = 边界 + 宽度：`offset ∈ [0, alloc_size)` 且访问宽度不超出分配 +- 越界双关由现有 DEREF 边界检查拦截 +- 宽度检查（`off + width <= alloc_size`）待补，见 TODO 预存 bug 7 +- 编译器内部 `asp`（外部地址空间）标志在 checker 写入 TYP_PTR 但全仓库无消费点—— + `0x... as *int` 在 safe 代码同样放行，归属待定，见 TODO 预存 bug 7 `unsafe` 块内部的指针操作仍然被三点 pass 追踪。`unsafe` 不是"关掉验证"——是"标注图边界入口"。一旦进入 safe 代码，编译器重新获得追踪权。 @@ -218,6 +229,12 @@ Core 编译器已有数据流图（`src/compiler/dataflow.cr`）和线性扫描 边界检查序列（s3 编码 alloc_size），运行时 prov_table 维护堆边界并 patch DEREF 检查点， 配合 2026-07-28 的 Arena 内存模型（`src/stdlib/arena.cr`）。细节见 `TODO.md`。 +**更新（2026-08-10）**：设计定论—— +1. 类型双关由图自动验证（见上"类型双关"节），不需要 unsafe；宽度检查待补（TODO 预存 bug 7） +2. **不扩展"程序内部地址直接指"（0x 字面量指内部对象）**——YAGNI：内部对象用 `&` 取址 + 更优（无漂移、类型全、验证无条件）；外部契约地址 unsafe 已够用。0x 字面量仅保留 + unsafe 外部入口角色（上表前三行），详见 TODO 预存 bug 7 + ## 参考 - **SVF** (SVF-tools): LLVM 上的值流图框架，自动检测 use-after-free、double-free、buffer overflow。Core 的数据流图是更统一的形式——同一张图同时做 regalloc、调度、验证。