Mở rộng logic phân tách đồng thời xuống phần cứng để chứng minh kernel hệ điều hành xv6 trên RISC-V bằng AI agent

MachCSL là một framework để chứng minh phần mềm hệ thống, như một kernel hệ điều hành, dựa trên ngữ nghĩa cấp thấp của một máy tính RISC-V, dựa trên ngữ nghĩa Sail RISC-V. Ý tưởng chính đằng sau MachCSL là thích ứng logic phân tách đồng thời, dựa trên Iris, để lý luận về quá trình thực thi phần cứng cấp thấp tại mức độ dưới một instruction: dịch trang bảng, TLB, các cấp độ đặc quyền, thanh ghi cấu hình, instruction fetch/giải mã/thực thi, traps và ngắt, DMA, bộ nhớ chia sẻ, lỗi nguồn điện, v.v. Việc lý luận ở mức độ chi tiết này đảm bảo rằng phần mềm hệ thống quản lý đúng tất cả các chi tiết phần cứng.

Việc chứng minh phần mềm ở mức độ trừu tượng thấp này rất tẻ nhạt, nhưng các AI agent dựa trên LLM có khả năng lý luận về những chi tiết cấp thấp như vậy. Là một nghiên cứu điển hình, chúng tôi chứng minh kernel hệ điều hành xv6 (6.657 dòng mã C và assembly), cung cấp giao diện gọi hệ thống Unix truyền thống (quy trình, hệ thống tệp, bộ mô tả tệp và lập lịch ưu tiên ngắt) và có độ đồng thời nội bộ đáng kể (hỗ trợ đa lõi với khóa độc lập mỏng, bộ nhớ chia sẻ, ngắt, DMA, v.v.). Trong quá trình chứng minh, chúng tôi phát hiện 11 lỗi trong cài đặt xv6, cũng như một lỗi trong ngữ nghĩa Sail RISC-V, và một lỗi trong trích xuất Lean của Sail. Cố gắng chứng minh mất 102 ngày, bao gồm cả thời gian phát triển framework MachCSL.

Trên kernel xv6 đã được chứng minh, chúng tôi chứng minh một định lý về hành vi ở cấp độ console: ví dụ, nếu người dùng nhập echo hello world làm đầu vào trên console UART, thì đầu ra duy nhất mà hệ thống có thể sản xuất là hello world (nếu không có sự cố hoặc lỗi khác). Định lý này bao phủ cả kernel và các tệp nhị phân init, sh, echo, cat, grep, sync và seccomp trong hình ảnh tệp tin hệ thống ban đầu.