- Ironclad là nhân họ Unix hỗ trợ thời gian thực dựa trên kiểm chứng hình thức dành cho môi trường phổ thông và nhúng
- Kiểm chứng hình thức (Formal verification): chuỗi quy trình và phép kiểm tra mà mã kernel phải trải qua để bảo đảm không có lỗi thời gian chạy (AoRTE, Absence of Runtime Errors) và tính chính xác của các thành phần
- Được viết bằng SPARK và Ada, đồng thời cấu thành từ 100% phần mềm tự do
- Hỗ trợ giao diện tương thích POSIX, đa nhiệm có ưu tiên thu hồi, kiểm soát truy cập bắt buộc (MAC) và lập lịch thời gian thực cứng
- Được phân phối theo giấy phép GPLv3, duy trì kiến trúc mã nguồn mở hoàn chỉnh không có firmware blob
- Có thể được port sang nhiều nền tảng, và hệ sinh thái đang mở rộng thông qua các bản phân phối như Gloire
Tổng quan về kernel hệ điều hành Ironclad
- Ironclad là nhân họ UNIX hỗ trợ thời gian thực có áp dụng một phần kiểm chứng hình thức (formal verification)
- Được thiết kế cho cả hệ thống mục đích chung lẫn hệ thống nhúng
- Kiểm chứng hình thức (Formal verification): chuỗi quy trình và phép kiểm tra mà mã kernel phải trải qua để bảo đảm không có lỗi thời gian chạy (AoRTE, Absence of Runtime Errors) và tính chính xác của các thành phần
- Để làm điều này, dự án sử dụng SPARK, một tập con của Ada
- Toàn bộ mã nguồn được cấu thành từ phần mềm tự do
- Kernel cung cấp giao diện tương thích POSIX, đồng thời hỗ trợ đa nhiệm có ưu tiên thu hồi, kiểm soát truy cập bắt buộc (MAC) và lập lịch thời gian thực cứng
- Mang lại trải nghiệm phát triển tương tự môi trường UNIX hiện có
- Có cấu trúc phù hợp với các hệ thống cần điều khiển thời gian thực
Đặc tính như một phần mềm tự do
- Ironclad được phát hành hoàn toàn dưới dạng mã nguồn mở theo giấy phép GPLv3
- Kernel không bao gồm firmware blob
- Mọi thành phần trong stack đều được cung cấp dưới dạng mã nguồn mở
Kiểm chứng hình thức (Formal Verification)
- Tận dụng các tính năng kiểm chứng hình thức của ngôn ngữ SPARK để bảo đảm sự vắng mặt lỗi và tính chính xác của các thành phần chính
- SPARK xác minh về mặt toán học tính nhất quán logic của mã bằng cách đặc tả điều kiện tiên quyết (Pre), điều kiện hậu nghiệm (Post), phụ thuộc (Depends) trong mã Ada
- Các đối tượng được kiểm chứng bao gồm mô-đun mật mã, hệ thống MAC, các chức năng liên quan đến giao diện người dùng
Tính di động và môi trường phát triển
- Ironclad đã được port sang nhiều nền tảng và bo mạch, đồng thời được thiết kế để dễ dàng mở rộng sang các nền tảng khác
- Chỉ phụ thuộc vào toolchain GNU, cho phép cross-compilation dễ dàng
- Nhờ tính tương thích POSIX, việc port phần mềm và phát triển trở nên thuận tiện
Bản phân phối và hệ sinh thái
- Dự án Ironclad cung cấp các bản phân phối (distribution) cho nhiều kiến trúc và bo mạch khác nhau
- Bản phân phối tự do và mã nguồn mở tiêu biểu là Gloire
- Cung cấp image phân phối có thể tải về ở dạng tarball
Hỗ trợ dự án và tính bền vững
- Ironclad được duy trì như một dự án cho phép tự do sử dụng, nghiên cứu và chỉnh sửa
- Việc vận hành dự án phụ thuộc vào quyên góp và trợ cấp
- Mọi đóng góp đều có tác động trực tiếp đến việc mở rộng và phát triển của dự án
1 bình luận
Ý kiến trên Hacker News
Đây là một dự án thú vị. Tôi tò mò về giới hạn của việc xác minh hình thức đối với thời gian thực thi tệ nhất (WCET)
Cũng đã có những kernel được kiểm chứng khác như seL4, atmosphere, và cũng có thể xây thêm lớp tương thích POSIX như genode
Ngoài ra còn có những kernel hoàn thiện và tương thích đầy đủ như QNX hay VxWorks, nên việc xác minh hoàn toàn có thể không mang lại nhiều giá trị bổ sung
Tuy vậy, tôi hiếm khi thấy trường hợp nào đồng thời có đủ WCET + xác minh hình thức + tương thích POSIX
Ở giai đoạn hiện tại, khó có thể nói độ trưởng thành của nó đã đủ cao để dùng ngay cho các mục đích thời gian thực như tài liệu đề cập
seL4 nhanh hơn Linux rất nhiều, nhưng cái này có vẻ sẽ chậm hơn. POSIX vốn có khuyết tật mang tính bản chất, còn MAC thì quá phức tạp nên khó dùng trong thực tế
Ada thuộc nhóm ngôn ngữ họ Wirth (họ Pascal). Tới giờ, tôi chỉ biết TUNIS là kernel kiểu Unix được viết bằng ngôn ngữ họ Wirth
TUNIS được triển khai bằng Concurrent Euclid
Ngoài ra, Sol của INRIA vào thập niên 80 được triển khai bằng một phương ngữ Pascal và cung cấp môi trường tương thích Unix, sau đó tiếp nối thành Chorus
Cũng có một công ty liên quan đến NDA mang tên Ironclad. Cần cẩn thận với vấn đề nhãn hiệu
Dù vậy, tôi thực sự hoan nghênh những thử nghiệm như thế này. Nhưng trong thực tế, mắt xích yếu nhất của bảo mật lại là tầng firmware
Ước mơ của tôi là phần cứng như máy tính của Framework sẽ có firmware EFI đã được kiểm chứng cùng firmware của từng thành phần đã được kiểm toán
Việc tạo ra một OS mới thực sự là một tham vọng lớn. Gần đây Radiant Computer cũng được nhắc tới, nên tôi tò mò không biết còn dự án thú vị tương tự nào nữa không
Tôi hy vọng một ngày nào đó kernel được xác minh hình thức hoàn toàn sẽ trở nên phổ biến
Có lẽ không thể xác minh toàn bộ Linux, nhưng seL4 dường như có thể nắm bắt cơ hội ở các thị trường như smartphone
Nhìn vào lộ trình xác minh của họ thì gọi đó là “xác minh hình thức” có phần hơi quá
Không có chứng minh cho các thuộc tính cốt lõi của kernel, và chưa đạt tới mức của những kernel như seL4 hay Tock
CuBit là một OS khác được viết bằng SPARK/Ada
Có thể xem mã nguồn trên GitHub
Với người dùng phổ thông, chỉ riêng kernel thì không có nhiều ích lợi
Một ví dụ về OS sử dụng kernel Ironclad là Gloire
Tài liệu liên quan đến MAC được trình bày khá tốt (Mandatory Access Control)
Nhìn vào dòng “liên hệ để biết giá” của SPARK, có vẻ đây là kiểu ‘free’ theo nghĩa khác chứ không hẳn là ‘phần mềm tự do’