别名分析 & 污点追踪 — reharness 核心分析引擎 一、别名分析 (alias.py) 回答：两个指针是否可能指向同一块 MMIO 区域？ C 驱动源码 struct my_dev *dev void __iomem *base clang -emit-llvm C → LLVM IR (.ll) 保留 debug info (行号) SVF 别名分析引擎 VFG (Value Flow Graph) 遍历 指向分析 → May-Alias 集合 svf-mmio-alias (C++ 工具) 别名 JSON {global: [{func, ln:N}]} 哪些行引用了全局 MMIO libclang AST 行号映射 别名解析 行号 → AST 节点 → C 变量名 dev->base 在第 42 行加载全局 MMIO → dev->base 是 BasePtr 别名 输出: MMIO Base 别名集合 {"dev->base", "regs", "mmio_base"} — 这些变量都指向同一块 MMIO 区域 为什么重要？如果没有别名分析，readl(dev->base + 0x10) 和 readl(regs + 0x10) 会被当成访问不同设备 二、污点追踪 (taint.py + dataflow.py) 追踪：MMIO 读出的值去了哪里？参与了什么运算？最终如何影响硬件操作？ 6 种抽象污点值 BasePtr MMIO 基址 ioremap() 返回值 ReadTaint MMIO 读出的值 readl() 返回值 Const 编译期常量 0x1234, #define REG Computed 已知运算结果 Const ⊕ Const → Const Top (⊤) 完全未知 外部输入/函数参数 Unknown 未追踪 非 MMIO 相关变量 污点源 (Sources) ioremap(addr, size) → BasePtr (MMIO 基址) 所有基于此地址的读写都是 MMIO Symbolic: base.reg + offset readl(base + offset) → ReadTaint (MMIO 读出值) 携带: 地址 = BasePtr + Const 污点传播 (Propagation) 赋值传播 val = readl(...); → val: ReadTaint 算术传播 x = val + 1; → x: Computed 位域提取 Bits{hi,lo}(ReadTaint) → Computed 污点汇 (Sinks) writel(val, base + off) 地址: BasePtr + Const | 值: ReadTaint/Const 条件分支 if(val & FLAG) ReadTaint 影响控制流 → 附加到 op.condition RMW 检测 read→modify→write 同一地址 read 后 write → ReadModifyWrite 流敏感 (Flow-Sensitive) 追踪 污点状态随基本块逐语句更新 — 同一变量在不同程序点可能有不同污点 BB1: val = readl(...) → val: ReadTaint | BB2: val = 0; → val: Const | BB3: φ(BB1, BB2) → val: ReadTaint ⊔ Const = Top ⊔ (join) 操作: ReadTaint ⊔ Const = Top, BasePtr ⊔ BasePtr = BasePtr (同源), 不同源 = Top 三、实例：一个 MMIO 读-修改-写的完整追踪 C 代码 ① dev->base = ioremap(0xFE200000, 0x100); ② val = readl(dev->base + GPIO_VAL); // 读状态 ③ if (val & BIT(3)) { ④ val |= BIT(5); ⑤ writel(val, dev->base + GPIO_VAL); ⑥ } 污点追踪结果 ① dev->base : BasePtr Symbolic(reg: dev->base) ② val : ReadTaint addr = Symbolic(dev->base) + 0x04 ③ condition = val & BIT(3) 附到 op.condition ④ val : ReadTaint | BIT(5) → 仍是 ReadTaint (污染传播) ⑤ → ReadModifyWrite read ② + write ⑤ 同一地址 最终 op: RMW, addr=Symbolic(dev->base,0x04), guard=(val & BIT(3)), transform=(val | BIT(5)) 数据流/污点源 传播 污点汇/条件 未知