Sau tám năm phát triển, dự án Muen 1.0 đã được phát hành, phát triển hạt nhân Tách biệt, việc không có lỗi trong mã nguồn đã được xác nhận bằng các phương pháp toán học để xác minh độ tin cậy chính thức. Hạt nhân có sẵn cho kiến trúc x86_64 và có thể được sử dụng trong các hệ thống quan trọng đòi hỏi mức độ tin cậy cao hơn và đảm bảo không có lỗi. Mã nguồn của dự án được viết bằng ngôn ngữ Ada và phương ngữ SPARK 2014 có thể kiểm chứng được. Mã được phân phối theo giấy phép GPLv3.
Hạt nhân phân tách là một vi hạt nhân cung cấp môi trường để thực thi các thành phần tách biệt với nhau, sự tương tác của chúng được quy định chặt chẽ bởi các quy tắc nhất định. Sự cô lập dựa trên việc sử dụng các phần mở rộng ảo hóa Intel VT-x và bao gồm các cơ chế bảo mật để chặn việc tổ chức các kênh liên lạc bí mật. Hạt nhân phân vùng tối giản và tĩnh hơn các hạt vi mô khác, giúp giảm số lượng các tình huống có thể gây ra lỗi.
Hạt nhân chạy ở chế độ gốc VMX, tương tự như trình ảo hóa và tất cả các thành phần khác chạy ở chế độ không phải gốc VMX, tương tự như hệ thống khách. Việc truy cập vào thiết bị được thực hiện bằng cách sử dụng các tiện ích mở rộng Intel VT-d DMA và ánh xạ lại ngắt, giúp có thể thực hiện liên kết an toàn các thiết bị PCI với các thành phần chạy trong Muen.
Các khả năng của Muen bao gồm hỗ trợ cho các hệ thống đa lõi, các trang bộ nhớ lồng nhau (EPT, Bảng trang mở rộng), MSI (Ngắt tín hiệu tin nhắn) và bảng thuộc tính trang bộ nhớ (PAT, Bảng thuộc tính trang). Muen cũng cung cấp bộ lập lịch quay vòng cố định dựa trên bộ hẹn giờ ưu tiên Intel VMX, thời gian chạy nhỏ gọn không ảnh hưởng đến hiệu suất, hệ thống kiểm tra sự cố, cơ chế phân bổ tài nguyên tĩnh dựa trên quy tắc, hệ thống xử lý sự kiện và các kênh bộ nhớ dùng chung cho giao tiếp trong các thành phần đang chạy.
Nó hỗ trợ chạy các thành phần với mã máy 64 bit, máy ảo 32 hoặc 64 bit, ứng dụng 64 bit bằng ngôn ngữ Ada và SPARK 2014, máy ảo Linux và các “unikernels” độc lập dựa trên MirageOS trên Muen.
Những cải tiến chính được đưa ra khi phát hành Muen 1.0:
- Các tài liệu đã được xuất bản cùng với các thông số kỹ thuật cho nhân (thiết bị và kiến trúc), hệ thống (chính sách hệ thống, Tau0 và bộ công cụ) và các thành phần, ghi lại tất cả các khía cạnh của dự án.
- Bộ công cụ Tau0 (Muen System Composer) đã được thêm vào, bao gồm một tập hợp các thành phần đã được xác minh sẵn sàng để soạn hình ảnh hệ thống và phát triển các dịch vụ tiêu chuẩn chạy trên Muen. Các thành phần được cung cấp bao gồm trình điều khiển AHCI (SATA), Trình quản lý thiết bị (DM), bộ tải khởi động, trình quản lý hệ thống, thiết bị đầu cuối ảo, v.v.
- Trình điều khiển muenblock Linux (triển khai thiết bị khối chạy trên bộ nhớ dùng chung Muen) đã được chuyển đổi để sử dụng API blockdev 2.0.
- Triển khai các công cụ để quản lý vòng đời của các thành phần gốc.
- Hình ảnh hệ thống đã được chuyển đổi để sử dụng SBS (Luồng khối đã ký) và CSL (Trình tải luồng lệnh) để bảo vệ tính toàn vẹn.
- Trình điều khiển AHCI-DRV đã được xác minh đã được triển khai, được viết bằng ngôn ngữ SPARK 2014 và cho phép bạn kết nối các ổ đĩa hỗ trợ giao diện ATA hoặc phân vùng đĩa riêng lẻ với các thành phần.
- Cải thiện hỗ trợ unikernel từ các dự án MirageOS và Solo5.
- Bộ công cụ ngôn ngữ Ada đã được cập nhật cho bản phát hành GNAT Community 2021.
- Hệ thống tích hợp liên tục đã được chuyển từ trình mô phỏng Bochs sang môi trường lồng nhau QEMU/KVM.
- Hình ảnh thành phần Linux sử dụng nhân Linux 5.4.66.
Nguồn: opennet.ru