KataOS, một hệ điều hành định hướng bảo mật phần cứng nhúng.
Tin tức đã được phát hành rằng Google đã công bố việc phát hành mã nguồn của diễn biến liên quan đến dự án Hệ điều hành Kata, mục tiêu của họ là tạo ra một hệ điều hành an toàn cho phần cứng nhúng.
Hệ thống cung cấp hỗ trợ cho các nền tảng dựa trên kiến trúc RISC-V và ARM64. Để mô phỏng hoạt động của seL4 và môi trường KataOS trên phần cứng trong quá trình phát triển, khung Renode được sử dụng.
Như một cách triển khai tham khảo, phức hợp phần mềm và phần cứng Sparrow được đề xuất, kết hợp KataOS với các chip an toàn dựa trên nền tảng OpenTitan. Giải pháp đề xuất hCó thể kết hợp một nhân hệ điều hành được xác minh hợp lý với các thành phần phần cứng Root of Trust (RoT) được xây dựng sử dụng nền tảng OpenTitan và kiến trúc RISC-V.
Ngoài mã KataOS, nó có kế hoạch mở tất cả các thành phần Sparrow khác, bao gồm cả thành phần phần cứng, trong tương lai.
Để làm nền tảng cho hệ điều hành mới này, chúng tôi đã chọn seL4 làm kênh vi mô vì nó đặt bảo mật lên hàng đầu và trung tâm; nó được chứng minh về mặt toán học là an toàn, với tính bảo mật, tính toàn vẹn và tính khả dụng được đảm bảo. Thông qua khuôn khổ seL4 CAmkES, chúng tôi cũng có thể cung cấp các thành phần hệ thống được xác định tĩnh và có thể phân tích cú pháp. KataOS cung cấp một nền tảng an toàn có thể xác minh để bảo vệ quyền riêng tư của người dùng vì về mặt logic, các ứng dụng không thể vi phạm các biện pháp bảo mật phần cứng nhân và các thành phần hệ thống an toàn có thể xác minh được.
Nền tảng đang được phát triển với các chip đặc biệt là được thiết kế để chạy các ứng dụng bảo mật và học máy yêu cầu mức độ bảo vệ cụ thể và đảm bảo rằng không có hỏng hóc. Hệ thống thao tác hình ảnh của người và ghi âm giọng nói được đưa ra làm ví dụ về các ứng dụng như vậy. Việc sử dụng kiểm tra độ tin cậy trong KataOS đảm bảo rằng trong trường hợp có sự cố xảy ra ở một phần của hệ thống, sự cố này sẽ không lây lan sang phần còn lại của hệ thống và đặc biệt là đối với hạt nhân và các phần quan trọng.
Kiến trúc seL4 vượt trội trong các bộ phận chuyển động để quản lý tài nguyên hạt nhân trong không gian người dùng và áp dụng các kiểm soát truy cập tương tự cho các tài nguyên đó như đối với tài nguyên người dùng.
Kênh nhỏ không cung cấp thông tin trừu tượng cấp cao out-of-the-box để quản lý tệp, quy trình, kết nối mạng và những thứ tương tự, nhưng 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ý, ngắt và tài nguyên bộ xử lý. Các trình điều khiển và trừu tượng cấp cao để tương tác với phần cứng được triển khai riêng biệt trên đầu kênh vi mô dưới dạng các tác vụ cấp người dùng. Việc truy cập của các nhiệm vụ như vậy vào các tài nguyên có sẵn cho kênh vi mô được tổ chức thông qua định nghĩa các quy tắc.
Để được bảo vệ thêm, tất cả các thành phần ngoại trừ microkernel ban đầu được phát triển trong Rust sử dụng các kỹ thuật lập trình an toàn để giảm thiểu lỗi khi làm việc với bộ nhớ, dẫn đến các vấn đề như truy cập một vùng bộ nhớ sau khi giải phóng nó, bỏ tham chiếu đến con trỏ rỗng và tràn bộ đệm.
Trình tải ứng dụng trong môi trường seL4, dịch vụ hệ thống, khung phát triển ứng dụng, API để truy cập các lệnh gọi hệ thống, trình quản lý quy trình, cơ chế cấp phát bộ nhớ động, v.v. chúng được viết bằng Rust. Đối với lắp ráp đã được xác minh, bộ công cụ CAmkES do dự án seL4 phát triển sẽ được sử dụng. Các thành phần cho CAmkES cũng có thể được tạo trong Rust.
An toàn bộ nhớ được cung cấp trong Rust tại thời điểm biên dịch bằng cách kiểm tra các tham chiếu, theo dõi quyền sở hữu đối tượng và thời gian tồn tại của đối tượng (phạm vi), cũng như bằng cách đánh giá tính đúng đắn của quyền truy cập bộ nhớ trong quá trình thực thi mã. Rust cũng cung cấp tính năng bảo vệ chống tràn số nguyên, yêu cầu các biến phải được khởi tạo trước khi sử dụng, thực thi khái niệm về biến và tham chiếu bất biến theo mặc định, đồng thời cung cấp tính năng nhập tĩnh mạnh mẽ để giảm thiểu lỗi logic.
Cuối cùng đối với những người quan tâm, bạn nên biết rằng các thành phần của hệ thống KataOS được viết bằng Rust và chạy trên kênh vi mô seL4, nơi cung cấp bằng chứng toán học về độ tin cậy trong hệ thống RISC-V, cho thấy rằng mã hoàn toàn tuân thủ các thông số kỹ thuật được chỉ định trong ngôn ngữ chính thức.
Mã dự án được mở theo giấy phép Apache 2.0, bạn có thể tham khảo thêm thông tin chi tiết về mã này trong liên kết theo dõi.