Reharness — 核心想法

从 Linux 驱动中提取硬件交互逻辑 · 2026.07.07

为什么不能直接让 LLM 翻译整个驱动？

现有 C2Rust 翻译范式存在根本性的语义错配（Semantic Mismatch）：

噪声干扰： 将整个驱动代码视作"翻译对象"，LLM 陷入 Linux 内核的胶水代码（spinlock、platform_driver、devm_、PCI 子系统调用）。这些与硬件无关的 OS 耦合逻辑，作为背景噪声严重干扰 LLM 对核心意图的识别。

本质错失： 驱动的唯一终极职责是与硬件交互。翻译的本质不应是"语法等价转换"，而应是"逆向恢复硬件操作协议"。

核心洞察： 摒弃"全量翻译"，转为硬件行为剥离（Hardware Behavior Stripping） —— 将驱动中与硬件寄存器交互的逻辑（RIS）从 OS 泥潭中精准提取出来。

一个比喻

现有 LLM 翻译 Linux 驱动如同"临摹一幅带有复杂背景的画作"，最终作品被背景噪声淹没。
我们反其道而行之，旨在"擦除背景，只提取画中的人物轮廓"。

• 轮廓 = RIS（寄存器交互序列）
• 补充说明 = LLM 为 RIS 写语义
• 完善细节 = 元数据迁移（#define、配置常量）
• 验证轮廓准确 = 动态轨迹偏序对齐

三阶段管线

阶段1：RIS 提取 — 为什么用 AST？

正则有四个硬伤：

AST 解决方案： 预处理记录 → 宏展开；类型信息 → MMIO 消歧；控制流 → 守卫谓词；污点分析 → RMW 检测

阶段2：LLM 语义注入

RIS 只是"寄存器魔数"（读 0x20，写 0x20），需要 LLM 赋予语义：

• "为什么这么配寄存器？"
• "这个函数的角色是什么？"
• "设备的状态机/协议是什么？"

关键约束：

• LLM 仅做注释与归纳，禁止生成新的控制流代码
• 防止 LLM 幻觉引入错误的硬件交互逻辑
• 输出：FunctionSpec（函数级语义）+ DeviceSpec（设备级规约）

阶段3：元数据迁移（语义提升）

驱动中散落的 #define、结构体定义、配置常量，需要从"Linux 风格"转化为"硬件通用风格"：

• 语义提升（Semantic Lifting）： OS 命名空间 → 独立的硬件寄存器位域描述
• 目标： 生成的驱动不出现硬编码，保留完整的寄存器定义和配置信息
• 四层规约中的体现： .facts 文件捕获所有元数据，.bind 文件映射到目标平台

怎么验证提取是对的？

单一静态提取存在路径覆盖盲区 → 动静结合的行为收敛框架

动态金标准： 在 QEMU/真实硬件运行原始驱动，通过 mmiotrace 录制硬件实际接收到的寄存器交互轨迹

覆盖引导测试： 设计涵盖初始化、中断处理、电源管理、数据传输的"最小行为覆盖测试集"

偏序对齐验证：

• 不采用僵硬的序列字符串匹配
• 只检验"配置依赖链"是否在动态轨迹中严格成立
• 例如：Enable 位一定在 Config 位之后 → 容忍乱序与别名

反向优化闭环

静态提取(RIS) ──→ 动态验证(Trace) ──→ 差异分析
     ↑                                      │
     └──── 第二轮精炼(Refinement) ←─────────┘

• 差异（缺失/多余寄存器访问）= 监督信号
• 消除假阳性（OS 噪声残留）
• 补全假阴性（异常路径未执行）
• 形成"提取 → 验证 → 修正"迭代闭环

三大核心贡献

1. 新范式：硬件行为核提取（Hardware Behavior Kernel Extraction）

• 区别于传统"代码翻译"，首次将 OS 逻辑与硬件逻辑量化分离

2. 新技术：动静结合的行为收敛框架

• 静态切片 + 动态轨迹金标准 + 偏序关系比对
• 解决乱序与地址别名难题，遏制 LLM 幻觉

3. 新标准：超越 BLEU 的评估维度

• RIS 可独立适配裸机/RTOS 运行
• 寄存器访问覆盖率 + 动态轨迹重合度 = 量化指标

现有工具对比

reharness 不替代这些工具，而是在它们之上构建"硬件行为剥离"专用管线

当前进展

已完成： libclang AST 提取器、流敏感污点分析、RMW 检测、过程间调用图内联、意图标注、四层规约输出、多后端代码生成、SVF 别名分析原型

进行中： LLM 语义补全管线、驱动元数据提取、就绪度评分

待做： 17 驱动评估、virtio 端到端验证、LLM 合成实验、论文撰写

总结

问题： LLM 翻译整个驱动被 OS 耦合代码淹没 → 语义错配

方案： 三阶段管线 — 提取 RIS → LLM 语义注入 → 元数据迁移

验证： 动态轨迹偏序对齐 + 反向优化闭环

贡献： 新范式（硬件行为核提取）+ 新技术（动静结合收敛）+ 新标准（超越 BLEU）

架构图：pgs.alexbd.cn/reharness-arch.html

讨论要点

1. 叙事框架 — "硬件行为剥离"范式是否清晰？比喻是否恰当？
2. 验证机制 — 偏序对齐验证的可行性？需要多少测试用例？
3. LLM 约束 — "仅注释归纳，禁止生成控制流"是否过于保守？
4. 元数据迁移 — 语义提升的具体实现方案？
5. 评估维度 — 除了寄存器覆盖率和轨迹重合度，还需要什么指标？
6. 论文投稿目标 — 会议/期刊？时间节点？