Weekly Report 2026-03-29

工作任务

1.尝试跑论文KNighter: Transforming Static Analysis with LLM-Synthesized Checkers的工具KNighter

2.调研从riscv isa文档到具体代码实现的中间层pattern的形式

工作进展

====周一到周四的工作======

对于RISC-V CVE类型分类的重构

按照我的分类，11/19的CVE是隐式API/ABI/时间规定违反+特性/机制冲突，8/19的CVE是功能实现不完整+特殊/边缘情况遗漏+分支路径遗漏，也就是说一半多的漏洞本质都是语义冲突带来的矛盾（即对ISA和linux的结合之处不熟悉），另一半是功能实现不完整（即对ISA/linux本身的不熟悉，这一般来说用fuzzer就能找出来的（很多确实就是用fuzz跑出来的））

新的几个patch

https://lore.kernel.org/all/20260323115957.38348-1-vulab@iscas.ac.cn/

https://lore.kernel.org/all/20260323172826.69428-1-vulab@iscas.ac.cn/

https://lore.kernel.org/all/20260325083139.15638-1-vulab@iscas.ac.cn/

都是直接将相应的代码片段给gemini，加人工审核出来的，说明linux的浅层漏洞是很多的，这种简单的办法都是很容易找出漏洞的。

===周四下午开完会之后的工作====

尝试复现论文KNighter: Transforming Static Analysis with LLM-Synthesized Checkers的工具Knighter

简要概括这个论文就是，先前的漏洞挖掘流程是

• 人类通过以前的CVE学习，获得经验，然后写出静态checker工具的pattern，然后进行scan。这个的局限性是耗时

• 或者是像我一样，直接将代码传给LLM，让LLM分析是否存在漏洞。但是这个局限性是LLM上下文长度，只能找出一些简单的浅层漏洞

这个论文提出了一个新的workflow：

机器通过对于以前的CVE/commit进行学习，获得经验，写出静态checker，然后进行扫描（其实就是对于第一个方法的升级），然后这个方法可以不同程度的弥补上面两个方法的局限性

然后他引出了一个工具，就叫做Knight，他的工作流程就是gen（LLM生成checker）-> refine（LLM打磨checker）->scan（用checker全量扫描）-> triage（让LLM检测误报，生成漏洞报告）-> gen….. 不断循环提升checker的质量

（这一段是AI写的）本周主要推进了基于大模型的静态分析工具 KNighter 在 RISC-V Linux 内核上的适配与验证（目前以单 commit 为目标进行了初步跑通测试）。

期间集中解决了大量底层环境与工具链的兼容性问题：

1. 修复了 Nix 环境下 HOSTCC 编译缺失 stdio.h 和 OpenSSL 等依赖的问题。

2. 重新编译自定义 LLVM，补充了缺失的 RISC-V 交叉编译后端。

3. 排查并修复了 KNighter 源码中的多个硬编码 Bug（包括分支名 main 错误、并发参数 -jNone 导致 make 崩溃、以及 Checker 命名带减号导致 Clang 无法加载插件等）。

扫清上述障碍后，成功跑通了从规则生成、精炼到全内核编译扫描（gen -> refine -> scan）的端到端闭环。利用 AI 针对 SR_SUM 漏洞补丁生成的 LLVM 规则对内核进行全量扫描，最终成功捕获到 1 个漏洞报告。虽然经查看确认为误报（假洞），但已实质性验证了该自动化静态分析流水线在 RISC-V 内核上的有效性。

之后开始使用25-26年的21个commit给knight，增加样本范围，由于需要llvm编译，llm对话，以及kernel的编译，整个过程耗时非常长

最终他说跑出了291个bugs，但是最后一步用LLM去重始终出错，于是作罢。

调研从riscv isa文档到具体代码实现的中间层pattern的形式

RISC-V ISA文档到具体的代码实现有一层巨大鸿沟，现在有不少工作都在减少这巨大鸿沟，具体来说是依靠建立一层一层的抽象层

首先，研究的主体是RISC-V ISA/SBI文档，他是用自然语言编写的，并且他的作用是要涵盖所有需要RISC-V需求的用户，比如操作系统，编译器，cpu设计，所以他是混乱的起始

文档规范层：

第一个抽象层（RISC-V的formal表示）：是the RISC-V Foundation官方的formal representation of spec，一个用Sail语言表示的模型https://github.com/riscv/sail-riscv，该语言在ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS 论文中被提出，他有些类似于llvm，构建起了由自然语言编写的各种isa spec到{模拟器，test suite，SMT，Lem，coq，甚至ref system verilog}的双向转换

但是现在大多数对于sail的利用都集中在cpu验证，针对操作系统的不是很多，sail规范的是操作系统管理的资源，而如何利用sail来做操作系统的验证呢，Automatic ISA analysis for Secure Context Switching 提出了一个方法，他创建了一个叫做sailor的工具，能利用sail来对于操作系统的context switch部分做检测，他的原理是

1. 首先通过提三个基本问题+sail输入给scanner创建对于ISA的insight，比如一条指令的footprint（比如他会改动哪些csr，哪些可以在s mode访问？）

2. 通过Isla工具创建的footprint和上述的ISA-insight交叉验证

3. 将ISA-insight传给analyzer，让他通过一个算法找出哪些是ISA-state是security-sense state

从而找出这些secure-sense state是否会在真实os中的context switch中出现来判断是否可能存在bug。

他依赖的工具Isla是Isla: Integrating full-scale isa semantics and axiomatic concurrency models.这篇论文提出的，按我的理解，Isla能将一条指令在Sail（即ISA）的层面上进行符号执行，即能找出这条指令所有可能的路径已经footprint

第二个抽象层（Formal表示的语义提取）：但是这会存在一个问题，就是即使有riscv的formal表示，the user of the formal representation可能不同，比如cpu领域需要依赖他，编译器领域的需要依赖他，以及我们的操作系统领域，各个领域对于spec的需求侧重点其实是不一样的，如果仅仅是用同一个sail表示，他只是类似一刀切，语义层面大家的需求还是不一样，针对这个问题，A Multipurpose Formal RISC-V Specification开创一个方法，他把isa spec描述为a program with holes，这类似于c++里面的类，他只是定义了一个spec的框架，但是就像一个hole，留下了很多洞是未实现的，比如他有一个LOAD的abstract方法，每个领域的实现都不一样，比如对于编译器，地址合法就返回值，但是对于cpu就需要考虑流水线，多级cache，对于操作系统可能更侧重mmu（用户态的地址校检）。这个抽象层主要是将语义从isa规范中剥离出来了，他是sail的扩展。

系统实现层：

第三个抽象层（编译器）：编译器后端永远是将软件逻辑映射到物理硬件最重要的抽象层，让软件逻辑被抽象出来，并且可以减少关注具体硬件实现而专注软件逻辑（我对编译器原理有点不熟悉，就暂时跳过了这部分的深究）

Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA

第四个抽象层（执行环境（SBI/ Security Monitor/TEE））：

DORAMI: Privilege Separating Security Monitor on RISC-V TEEs – USENIX

第五个抽象层（内核本身）：内核本身的很多很复杂的机制或者util本身就是一层抽象层，我认为这个抽象层是riscv CVE最多发的区域

一些想法：

1. 通过sail生成一个正确的操作系统模型goden model（不现实），或者一个绝对正确的操作系统组件（可以简化一点细节）

2. 通过sail生成一个sail checker，来检查现有的操作系统（Checker的本质是内核不能做什么，而sail的本质是os管理的资源是什么，他们之间有一层鸿沟，我认为可以从sail中提取一些安全属性，从而提取出所有的“内核不能做什么”。Ai给我的一句话感觉很形象：“让硬件的数学模型自动充当**“漏洞预言机（Bug Oracle）”**”）（Automatic ISA analysis for Secure Context Switching）

3. 通过现有的patch和commit生成checker，类似knight（KNighter: Transforming Static Analysis with LLM-Synthesized Checkers）

4. 还有一个想法就是让sail带来的语义部分和内核在没有riscv的其他api/abi的语义是否存在冲突，比如说内核有一个叫做vmemmap的变量，他的语义是page结构体的虚拟地址起始，隐含着一个对齐语义，但是riscv的起始地址的对齐要求可能和他不一样，但是为了引入riscv方便，他会利用vmemmap的抽象，这里存在语义冲突，这就是CVE-2024-57945，CVE-2024-56673，CVE-2024-26795的根因，riscv的引入会利用很多内核本身的某些抽象，比如说一些函数，一些struct，他们的很多规范是隐含的，并且包含着其他架构的取舍，可能与riscv的sail模型冲突，很多API/ABI misuse就会产生。（这个想法我暂时没有找到具体论文，可能暂时没人做吧）

参考文献

KNighter: Transforming Static Analysis with LLM-Synthesized Checkers

ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS

Isla: Integrating full-scale isa semantics and axiomatic concurrency models.

Automatic ISA analysis for Secure Context Switching

A Multipurpose Formal RISC-V Specification