Giới thiệu về vi nhân seL4 [PDF]

• seL4 là một vi nhân hệ điều hành, chạy ở chế độ kernel với lượng mã tối thiểu để kiểm soát tài nguyên phần cứng và tăng cường bảo mật
• Thuộc họ vi nhân L4 và đã được phát triển từ giữa những năm 1990
• Có thể hoạt động như một hypervisor, hỗ trợ chạy các hệ điều hành khách như Linux
• Là nhân hệ điều hành đầu tiên trên thế giới được chứng minh về tính đúng đắn chức năng, với chứng minh toán học ở cấp độ mã đã hoàn tất
• Sử dụng mô hình bảo mật dựa trên Capability (năng lực) để kiểm soát truy cập chi tiết

Cấu trúc của seL4 và chức năng hypervisor

• Kernel nguyên khối vs vi nhân
  • Kernel nguyên khối (Linux, v.v.): mã kernel rất đồ sộ nên có nhiều lỗ hổng bảo mật hơn → khoảng 20 triệu dòng mã (20M SLOC)
  • Vi nhân (seL4): chỉ dùng lượng mã kernel tối thiểu → khoảng 10 nghìn dòng mã (10K SLOC)
  • Thu nhỏ kích thước kernel → tăng cường bảo mật và giảm bề mặt tấn công
• seL4 đóng vai trò hypervisor
  • Có thể chạy đầy đủ hệ điều hành khách như Linux trong VM
  • Mỗi VM chạy độc lập và không thể can thiệp lẫn nhau → bảo đảm cô lập mạnh mẽ
  • Gọi thủ tục được bảo vệ (PPC) → cho phép giao tiếp an toàn giữa các VM

Kiểm chứng và mô hình bảo mật của seL4

• Kiểm chứng tính đúng đắn chức năng
  • seL4 đã được chứng minh bằng toán học là hoạt động đúng ở cấp độ mã
  • Bảo đảm mọi hành vi của kernel đều tuân theo đặc tả
• Kiểm chứng chuyển đổi (Translation Validation)
  • Chứng minh rằng mã nhị phân do trình biên dịch tạo ra khớp chính xác với mã C gốc
  • Được thực hiện thông qua chuỗi công cụ tự động hóa
• Kiểm chứng các thuộc tính bảo mật
  • Tính bí mật: chỉ có thể truy cập dữ liệu khi được cho phép rõ ràng
  • Tính toàn vẹn: chỉ có thể sửa đổi dữ liệu khi được cho phép rõ ràng
  • Tính sẵn sàng: chỉ có thể sử dụng tài nguyên khi được cho phép rõ ràng

Mô hình bảo mật dựa trên Capability

• Capability là gì?
  • Một token bảo mật cấp quyền truy cập vào một đối tượng cụ thể
  • Mã hóa đồng thời tham chiếu đến đối tượng và quyền truy cập
  • Cho phép kiểm soát truy cập chi tiết → áp dụng nguyên tắc đặc quyền tối thiểu (Principle of Least Privilege, POLA)
• Ưu điểm của Capability
  • Kiểm soát truy cập chi tiết → có thể giảm thiểu đặc quyền
  • Có thể ủy quyền (delegation) và thu hồi quyền
  • Mô hình bảo mật mạnh mẽ → vượt trội hơn mô hình kiểm soát truy cập truyền thống (ACL)
• Giải quyết bài toán confused deputy
  • Trong các hệ thống truyền thống dựa trên ACL, trạng thái bảo mật được quyết định theo security ID của chủ thể
  • Trong seL4, Capability trực tiếp quyết định quyền bảo mật → cho phép kiểm soát quyền hạn rõ ràng

Hỗ trợ hệ thống thời gian thực và hệ thống mixed-criticality

• Hỗ trợ hệ thống thời gian thực
  • seL4 hỗ trợ lập lịch dựa trên mức ưu tiên
  • Đã hoàn tất phân tích thời gian thực thi tệ nhất (WCET) của mọi tác vụ kernel → bảo đảm hard real-time
• Hỗ trợ hệ thống mixed-criticality (Mixed-Criticality System, MCS)
  • Phân bổ và cô lập tài nguyên CPU dựa trên scheduling context
  • Kiểm soát để các tác vụ có ưu tiên cao không chiếm dụng toàn bộ CPU
  • Có thể chạy đồng thời tác vụ quan trọng và không quan trọng

Hiệu năng và hiệu quả

• Vi nhân có hiệu năng hàng đầu
  • Không làm suy giảm bảo mật ngay cả khi hiệu năng là yếu tố quan trọng
  • Chi phí system call và IPC được giảm xuống mức tối thiểu → nhanh hơn hơn 5 lần so với các hệ thống cạnh tranh
• Hiệu năng vượt trội so với các hệ thống cạnh tranh
  • Fiasco.OC: chậm hơn khoảng 2 lần so với seL4
  • Zircon: chậm hơn khoảng 9 lần so với seL4
  • CertiKOS: chậm hơn khoảng 5 lần so với seL4

Ứng dụng thực tế và cyber retrofit

• Các trường hợp sử dụng thực tế

  • Đã được áp dụng thành công trong ULB (trực thăng không người lái) của Boeing
  • Xác nhận tăng cường bảo mật và độ ổn định hệ thống

• Tăng cường bảo mật dần dần cho hệ thống hiện có (Incremental Cyber Retrofit)

  • Chạy hệ thống hiện có trong VM đồng thời từng bước mô-đun hóa
  • Tăng cường bảo mật và giảm thiểu suy giảm hiệu năng

Kết luận

• seL4 là vi nhân an toàn nhất thế giới với tính đúng đắn chức năng, bảo mật và hiệu năng đã được chứng minh
• Với mô hình bảo mật đã được kiểm chứng và hỗ trợ hệ thống mixed-criticality, nó có thể được sử dụng thực tiễn trong nhiều lĩnh vực
• Có thể tăng cường bảo mật và cải thiện hiệu năng cho các hệ thống hiện có → một vi nhân đổi mới cân bằng giữa bảo mật và hiệu năng