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,657 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 11 bugs in the xv6 implementation, as well as one bug in the Sail RISC-V semantics, and one bug in Sail's Lean extraction. The verification effort took us 102 days, including the time to develop the MachCSL framework. On top of the verified xv6 kernel, we prove a theorem about console-level behavior: e.g., if the user types echo hello world as input on the UART console, the only output the system can produce is hello world (if there are no crashes or other errors). This theorem covers both the kernel and the init, sh, echo, cat, grep, sync, and seccomp binaries in the initial file system image.

翻译：暂无翻译