发表机构
MIT CSAIL（麻省理工学院计算机科学与人工智能实验室）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出基于Iris的MachCSL框架，将并发分离逻辑扩展至硬件层级，借助LLM智能体验证RISC-V上的xv6内核，发现10个漏洞，耗时77天完成验证。
AI 中文摘要
MachCSL是一个用于验证系统软件（如操作系统内核）的框架，它基于Sail RISC-V语义构建，依托RISC-V计算机的底层语义实现。MachCSL的核心思路是对基于Iris的并发分离逻辑进行适配，以实现对子指令级别的底层硬件执行的推理，涵盖页表转换、TLB、特权级别、配置寄存器、指令取指/译码/执行、陷阱与中断、DMA、共享内存、电源故障等环节。在这一细节层级进行推理可确保系统软件能正确管理所有硬件细节。在如此低的抽象层级验证软件十分繁琐，但基于大语言模型（LLM）的智能体具备推理这类底层细节的能力。作为案例研究，我们对xv6操作系统内核（包含6593行C语言和汇编代码）进行了验证，该内核提供传统Unix系统调用接口（进程、文件系统、文件描述符及抢占式调度），且具备大量内部并发特性（支持多核细粒度锁定、共享内存、中断、DMA等）。在验证过程中，我们发现了xv6实现中的9个漏洞，以及Sail RISC-V语义中的1个漏洞。整个验证工作耗时77天，其中包含开发MachCSL框架的时间。
英文摘要
MachCSL is a framework for verifying system software, such as an OS kernel, on top of low-level semantics of a RISC-V computer, based on the Sail RISC-V semantics. The key idea behind MachCSL is to adapt concurrent separation logic, based on Iris, to reasoning about low-level hardware execution at the sub-instruction level: page-table translation, TLB, privilege levels, configuration registers, instruction fetch/decode/execute, traps and interrupts, DMA, shared memory, power failures, etc. Reasoning at this level of detail ensures that the system software correctly manages all of the hardware details. Verifying software at this low level of abstraction is tedious, but LLM-based agents are capable of reasoning about such low-level details. As a case study, we verify the xv6 OS kernel (6,593 lines of C and assembly code), which provides a traditional Unix system call interface (processes, file system, file descriptors, and preemptive scheduling) and has substantial internal concurrency (multi-core support with fine-grained locking, shared memory, interrupts, DMA, etc.). In the verification process, we uncovered ten bugs in the xv6 implementation, as well as one bug in the Sail RISC-V semantics. The verification effort took us 93 days, including the time to develop the MachCSL framework. On top of the verified xv6 kernel, we prove an application-level theorem: if the user types echo hello world as input on the UART console, the only output the system can produce is hello world. This theorem covers both the kernel and the init, sh, and echo binaries in the initial file system image.
