Công việc xác minh toán học chính thức về độ tin cậy và bảo mật của vi nhân seL4 trên các hệ thống có kiến trúc tập lệnh AArch64 đã hoàn tất. Quá trình xác minh bao gồm chứng minh toán học về tính đúng đắn của hoạt động seL4, thể hiện sự tuân thủ đầy đủ các thông số kỹ thuật được định nghĩa trong ngôn ngữ hình thức. Bằng chứng về độ tin cậy này cho phép sử dụng seL4 trong các hệ thống quan trọng dựa trên bộ xử lý ARM64, vốn yêu cầu mức độ bảo mật cao và đảm bảo không xảy ra lỗi.
Vi nhân seL4 ban đầu được kiểm chứng cho bộ xử lý ARM 32-bit, và sau đó cho bộ xử lý x86 và RISC-V 64-bit. Việc kiểm chứng đảm bảo rằng nếu xảy ra lỗi ở một phần của hệ thống, lỗi đó sẽ không lan sang phần còn lại của hệ thống và các thành phần quan trọng của nó. Trong bối cảnh bảo mật, việc kiểm chứng xác nhận rằng nhân hệ điều hành cung cấp mức độ cách ly ứng dụng phù hợp, ngăn chặn chúng truy cập thông tin trái phép và đảm bảo rằng nếu các ứng dụng phụ bị xâm phạm, cuộc tấn công sẽ không lan sang các ứng dụng quan trọng.
Kiến trúc vi hạt nhân seL4 đáng chú ý trong việc di chuyển các bộ phận để quản lý tài nguyên hạt nhân vào không gian người dùng và sử dụng cùng các công cụ kiểm soát truy cập đối với các tài nguyên đó cũng như đối với tài nguyên người dùng. Hạt nhân vi mô không cung cấp các bản tóm tắt cấp cao được tạo sẵn để quản lý tệp, quy trình, kết nối mạng và những thứ tương tự; thay vào đó, nó chỉ cung cấp các cơ chế tối thiểu để kiểm soát quyền truy cập vào không gian địa chỉ vật lý, các ngắt và tài nguyên bộ xử lý. Các trình điều khiển và trừu tượng hóa cấp cao để tương tác với phần cứng được triển khai riêng biệt trên đầu vi hạt nhân dưới dạng các tác vụ cấp người dùng. Việc truy cập các tác vụ như vậy vào các tài nguyên có sẵn cho vi hạt nhân được tổ chức thông qua việc xác định các quy tắc.
Nguồn: opennet.ru
