Mã nguồn KSOS (Unix bảo mật) được công bố lại sau gần 4 thập kỷ
"The article reports the public release of KSOS source code, a late-1970s/1980s US Department of Defense-backed secure Unix-compatible operating system originally developed at Ford Aerospace and later extended at Logicon. KSOS was written in the type-safe language Modula, designed for formal verification and high-assurance use, and the recovered code was added to the TUHS archive after an old tarball was found; no vulnerability or CVE is discussed."
KSOS là ví dụ lịch sử về hướng tiếp cận formal verification và type-safe trong thiết kế hệ điều hành, có thể cung cấp tham chiếu cho các nỗ lực bảo mật hiện nay. Điểm then chốt: khả năng chứng minh bảo mật, giảm rủi ro do lỗi kiểu dữ liệu, và tài liệu/nguồn mở để kiểm chứng lại.
Việc mã nguồn KSOS được đưa vào kho TUHS chủ yếu mang giá trị học thuật và tham chiếu thiết kế, hỗ trợ đào tạo và nghiên cứu. Điểm then chốt: tăng nguồn tài liệu lịch sử, giảm chi phí nghiên cứu nền tảng, nhưng không tạo tác động vận hành trực tiếp vì đây không phải bản phát hành sản phẩm thương mại hay bản vá hệ thống đang dùng.
The Unix Heritage Society (TUHS) vừa công bố mã nguồn KSOS—một hệ điều hành tương thích Unix do Bộ Quốc phòng Mỹ tài trợ vào cuối thập niên 1970 và 1980. Theo thông báo của người sáng lập TUHS Warren Toomey, KSOS trước đây còn được gọi là Secure UNIX và được thiết kế để cung cấp một hệ điều hành có thể chứng minh bảo mật cho các máy tính mini quy mô lớn.
KSOS được hiện thực bằng ngôn ngữ Modula (hướng tới kiểm chứng hình thức), thay vì C. Bài viết nhấn mạnh điểm tương đồng về tư duy “type safety” và formal verification với một số hệ thống vi nhân hiện đại, dù KSOS không phải dự án Rust mới. Dự án khởi đầu năm 1978 tại Ford Aerospace, sau đó được mở rộng tại Logicon; tài liệu và mã được đưa vào kho lưu trữ TUHS sau khi tình cờ phát hiện một bản tarball cũ.
Về mặt kỹ thuật, KSOS có cơ chế tương thích lời gọi hệ thống kiểu Unix ở chế độ supervisor và có thư viện userland mô phỏng phần lớn các system call. Không có CVE hay lỗ hổng cụ thể được đề cập. Khuyến nghị cho đội kỹ thuật: nếu nghiên cứu lịch sử hoặc đánh giá mô hình kiểm chứng, hãy ưu tiên đọc executive summary và theo dõi nỗ lực tìm lại trình biên dịch gốc (KSOS không tự biên dịch, được biên dịch dưới UNIX).