21/10/2026 · VietTechies · Biên tập
Năm 2009, Gerwin Klein cùng 12 đồng tác giả công bố một kết quả hiếm thấy: họ dùng toán học để chứng minh phần lõi của hệ điều hành seL4 làm đúng như bản mô tả, và từng bước chứng minh đều được máy tính kiểm lại. Phần lõi này, gọi là vi nhân (microkernel), gồm 8.700 dòng code C và 600 dòng assembly, loại ngôn ngữ rất gần với mã máy. Chứng minh chỉ bao phần code C; phần assembly được coi như đúng. Việc nói rõ chỗ dừng ấy cũng là một phần thành quả của nhóm.
Cụ thể, nhóm chứng minh rằng code C của kernel (phần lõi hệ điều hành) làm đúng những gì một bản mô tả chính xác, ở mức khái quát, quy định cho kernel. Bản mô tả này gọi là đặc tả (specification). Giới chuyên môn gọi kết quả đó là tính đúng đắn chức năng: điều kernel thật sự làm khớp chính xác với điều nó được yêu cầu làm, miễn là các giả định đi kèm là đúng.
Việc chứng minh còn bắt được lỗi thật. Theo bài báo gốc, các cách kiểm tra khác đã tìm ra 16 lỗi; sau đó, quá trình kiểm chứng hình thức (formal verification, tức kiểm tra bằng suy luận toán học) tìm thêm 144 lỗi trong code. Chứng minh không phải bước đóng dấu sau cùng, mà là một phần của việc viết và sửa kernel.
Vì sao lại chọn phần lõi?
Kernel chạy với những quyền mà ứng dụng bình thường không có, nên một lỗi ở đây có thể kéo cả hệ thống vào rủi ro. Giữ phần lõi nhiều quyền này thật nhỏ thì việc chứng minh mới trong tầm tay.
seL4 chọn kiểu thiết kế vi nhân: kernel chỉ lo vài việc nền tảng, gồm luồng chạy chương trình (thread), vùng bộ nhớ riêng của từng chương trình (không gian địa chỉ) và cách các chương trình trao đổi với nhau. Phần lớn driver, tức trình điều khiển thiết bị, được đưa ra ngoài và chạy như ứng dụng bình thường; bản kernel trong bài báo chỉ giữ lại driver bộ đếm thời gian. Quyền dùng tài nguyên được kiểm soát bằng capability, có thể hình dung như những chiếc thẻ ghi rõ chương trình nào được dùng đối tượng nào của kernel.
Cách chia này cũng vạch rõ chứng minh nói về cái gì. Kernel đúng không có nghĩa mọi ứng dụng hay driver chạy quanh nó cũng đúng. Phần còn lại của hệ thống vẫn cần được thiết kế và kiểm chứng riêng.
Bản được chứng minh trong bài báo chạy trên chip ARM đời ARMv6. Nhóm tác giả cho biết đã có bản chạy trên x86, nhưng khi ấy bản này chưa được chứng minh. Ngay từ đầu, “chạy được” và “đã được chứng minh” đã là hai chuyện khác nhau.
Đi qua một bản nháp dễ suy luận hơn
Để nối việc viết hệ điều hành với việc chứng minh, nhóm làm trước một bản mẫu bằng ngôn ngữ lập trình Haskell. Lập trình viên chạy thử bản mẫu này cùng trình mô phỏng phần cứng. Vì chỉ dùng một phần giới hạn của Haskell, bản mẫu có thể được chuyển sang dạng mà phần mềm chứng minh xử lý được.
Sau đó, nhóm tự tay viết kernel bằng C. Cách này cho phép tối ưu sát phần cứng và không phải kéo phần chạy nền (runtime) của Haskell vào kernel dùng thật. Bản Haskell vì vậy chỉ là bản nháp chi tiết, không phải thứ được đưa vào sử dụng.
Chứng minh nối ba tầng với nhau: bản mô tả khái quát về hành vi (đặc tả trừu tượng), một bản mô tả chi tiết hơn có thể chạy được, và code C thật. Kỹ thuật này gọi là tinh chỉnh (refinement): chứng minh rằng tầng chi tiết hơn không làm điều gì nằm ngoài những gì tầng khái quát hơn cho phép.
Các nhà nghiên cứu viết và dẫn dắt chứng minh bằng Isabelle/HOL, một phần mềm hỗ trợ chứng minh toán học. Con người nghĩ ra hướng lập luận; phần mềm kiểm lại từng bước. Cách làm này rất khác với kiểm thử thông thường, tức chạy thử chương trình với thật nhiều dữ liệu mẫu.
Sai một chỗ nhỏ cũng có thể gây hậu quả
Phần lớn công sức dồn vào các bất biến (invariant): những điều kiện phải luôn đúng suốt lúc kernel chạy. Ví dụ, với một chuỗi dữ liệu móc nối nhau, mọi liên kết phải trỏ tới chỗ hợp lệ, các phần tử phải nối với nhau đúng cách và phải khớp với thông tin lưu ở nơi khác.
Những điều kiện như vậy không gói gọn trong một hàm. Khi sửa một đối tượng, chương trình phải giữ nguyên những điều mà các phần khác đang dựa vào. Bài báo đếm được hơn 150 bất biến như thế ở các tầng mô tả.
Một lỗi có thật cho thấy điều này cụ thể ra sao. Bộ điều khiển ngắt của chip ARM, bộ phận báo cho bộ xử lý biết có sự kiện cần xử lý, dùng giá trị 0xFF để báo “không có ngắt nào”. Phần lớn code xử lý đúng giá trị này, nhưng ở một chỗ, code lại so với NULL, giá trị mà C dùng cho con trỏ rỗng, tức là so với một giá trị khác hẳn.
Theo các tác giả, nhiều lỗi tìm được khi chứng minh phần code C là lỗi gõ nhầm, hiểu sai bản mô tả, hoặc quên sửa code sau khi bản mô tả thay đổi. Đó là những sơ suất rất bình thường của con người, dù hậu quả có thể là chương trình bị treo hoặc lỗ hổng bảo mật.
Những điều được giả định cũng là một phần kết quả
Chứng minh năm 2009 dừng ở mã nguồn C. Nó coi như trình biên dịch (compiler, phần mềm chuyển code C thành mã máy), phần code assembly và phần cứng đều không có lỗi. Khoảng 1.200 dòng code khởi động và khởi tạo cũng nằm ngoài chứng minh; phần cốt lõi được chứng minh là hành vi của kernel từ lúc chương trình chuyển vào kernel đến lúc kernel trả quyền điều khiển lại.
Một số chi tiết phần cứng ở mức rất thấp vẫn nằm ngoài mô hình. Bài báo bàn về các giả định quanh bộ nhớ đệm (cache) và TLB (translation lookaside buffer), nơi bộ xử lý nhớ tạm cách đổi địa chỉ bộ nhớ. Muốn nối mô hình toán học với chiếc máy thật ở những chỗ này, nhóm phải suy luận và kiểm tra thêm.
Bản mô tả cũng có giới hạn của nó. Các tác giả nói rõ: chứng minh code làm đúng bản mô tả không bảo đảm bản mô tả đúng với điều người dùng mong muốn. Một yêu cầu được làm chính xác vẫn có thể là một yêu cầu sai.
Công sức bỏ ra rất lớn: khoảng 20 người-năm (một người làm trong một năm) cho phần chứng minh, tính cả nghiên cứu, khung làm việc, công cụ và thư viện. Đây là tổng công của nhiều người cộng lại, không phải dự án kéo dài 20 năm.
Nghe “đã kiểm chứng”, cần hỏi thêm gì?
Từ đó đến nay, dự án đã chứng minh thêm nhiều tầng khác. Kho chứng minh hiện nay tách riêng từng loại: chứng minh code C đúng với bản mô tả, kiểm chứng mã nhị phân (bản đã dịch ra mã máy), chứng minh kiểm soát quyền truy cập và chứng minh luồng thông tin. Mỗi loại xác lập một điều khác nhau, không nên gộp hết vào kết quả năm 2009.
Tài liệu chính thức về cấu hình cho thấy sự khác biệt này rất cụ thể: mỗi loại chip và mỗi cấu hình được chứng minh đến đâu. Chẳng hạn, với ARM AArch32 (chip ARM 32-bit), phạm vi kiểm chứng gồm cả mã nhị phân của các hàm C đã được chứng minh ở mức C; với x64 (chip x86 64-bit), tài liệu ghi tính đúng đắn chức năng ở mức code C và không gồm nhánh xử lý nhanh (fast path).
Tài liệu cũng liệt kê những phần chưa được kiểm chứng, trong đó có quá trình khởi động kernel khi bật máy. Trang giải thích ý nghĩa của chứng minh nói rằng việc loại trừ được các nhóm lỗi lập trình chỉ đúng khi các giả định của chứng minh và cấu hình đã kiểm chứng được giữ nguyên; khả năng cô lập các phần của hệ thống cũng chỉ có khi hệ thống được thiết lập đúng.
Vì vậy, khi nghe một phần mềm “đã được chứng minh là đúng”, nên hỏi thêm bốn điều: chứng minh cho phần nào, chứng minh điều gì, trên cấu hình nào và dựa trên giả định nào. Bài báo seL4 là ví dụ rõ: phép kiểm tra 0xFF, code C và bản mô tả khái quát đều nằm trong cùng một lập luận, và giới hạn của lập luận ấy được ghi ra rõ ràng.
Bài liên quan
Đọc bằng ngôn ngữ khác: English
Nguồn
- Klein và các đồng tác giả: seL4: Formal Verification of an OS Kernel, SOSP 2009
- The L4.verified Proofs: tài liệu kho mã
- Tài liệu seL4: Verified Configurations
- seL4: What the Proof Implies
- Ảnh đại diện: Kurt Kaiser; Wikimedia Commons; CC0 (đã chỉnh sửa từ ảnh gốc)
