Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents

arXiv 초록 페이지를 기준으로 옮겼어요. 논문 본문(PDF)은 읽지 않았어요.

논문

• 제목: Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents
• 저자: M. Frans Kaashoek, Nickolai Zeldovich
• arXiv:2609.04043 (cs.LO, cs.OS). 2026년 9월 3일 제출, 10월 12일 v3

초록

MachCSL은 OS 커널 같은 시스템 소프트웨어를 RISC-V 컴퓨터의 저수준 의미론(Sail RISC-V 의미론) 위에서 검증하는 프레임워크예요. 핵심은 Iris 기반 동시 분리 논리(concurrent separation logic)를 명령어보다 더 잘게 쪼갠 하드웨어 실행 수준의 추론에 맞게 바꾼 거예요. 대상에는 페이지 테이블 변환, TLB, 권한 수준, 설정 레지스터, 명령어 인출·해독·실행, 트랩과 인터럽트, DMA, 공유 메모리, 전원 장애 등이 들어가요. 이 정도로 세밀하게 추론하면 시스템 소프트웨어가 하드웨어의 모든 세부를 올바르게 다루는지 보장할 수 있어요.

이렇게 낮은 추상 수준에서 검증하는 건 지루하지만, LLM 기반 에이전트는 이런 저수준 세부를 추론할 수 있다고 저자들은 말해요.

사례 연구: xv6

xv6 커널(C와 어셈블리 6,657줄)을 검증했어요. 프로세스, 파일 시스템, 파일 디스크립터, 선점형 스케줄링 같은 전통적 Unix 시스템 콜 인터페이스를 제공하고, 세밀한 락을 쓰는 멀티코어, 공유 메모리, 인터럽트, DMA 등 내부 동시성이 상당해요.

• 검증 과정에서 xv6 구현 버그 11개, Sail RISC-V 의미론 버그 1개, Sail의 Lean 추출 버그 1개를 찾았어요.
• MachCSL 프레임워크 개발을 포함해 102일이 걸렸어요.
• 검증된 커널 위에서 콘솔 수준 동작에 관한 정리도 증명했어요. 예를 들어 UART 콘솔에 echo hello world를 입력하면, 크래시 같은 오류가 없는 한 시스템이 낼 수 있는 출력은 hello world뿐이에요. 이 정리는 커널과 초기 파일 시스템 이미지의 init, sh, echo, cat, grep, sync, seccomp 바이너리까지 다뤄요.