RISC-V đã xác minh kênh vi mạch seL4 trên bộ xử lý RV64 của họ

RISC-V Foundation thông báo rằng họ đã xác minh cách thức hoạt động của kênh nhỏ seL4 trong hệ thống với kiến trúc tập lệnh RISC-V. Trong đó quá trình xác minh được rút gọn thành bằng chứng toán học về độ tin cậy của seL4, cho thấy sự tuân thủ đầy đủ các thông số kỹ thuật được chỉ định bằng ngôn ngữ chính thức.

Kiểm tra độ tin cậy cho phép seL4 được sử dụng trong các hệ thống quan trọng dựa trên bộ xử lý RISC-V RV64, đòi hỏi mức độ tin cậy cao hơn và không đảm bảo hỏng hóc.

Các nhà phát triển phần mềm chạy trên nhân seL4 có thể hoàn toàn chắc chắn rằng trong trường hợp xảy ra lỗi ở một phần của hệ thống, lỗi 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à đến các bộ phận quan trọng của nó.

Về seL4

Kiến trúc seL4 đáng chú ý là loại bỏ các phần để quản lý tài nguyên nhân trong không gian người dùng và sử dụng các phương pháp kiểm soát truy cập tương tự cho các tài nguyên đó như cho 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 đã được chuẩn bị để quản lý tệp, quy trình, kết nối mạng, v.v. nhưng thay vào đó 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 bộ điều khiển và trừu tượng cấp cao để tương tác với máy tính đượ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 thực hiện ở cấp người dùng.

Việc truy cập các nhiệm vụ như vậy vào các tài nguyên có sẵn trong kênh vi mô được tổ chức thông qua định nghĩa các quy tắc.

RISC-V cung cấp một hệ thống mở và linh hoạt hướng dẫn máy móc cho phép tạo bộ vi xử lý cho các ứng dụng tùy ý, không yêu cầu khấu trừ và không áp đặt các điều kiện sử dụng.

RISC-V cho phép bạn tạo các bộ xử lý và SoC hoàn toàn mở. Hiện tại, trên cơ sở đặc tả RISC-V, một số công ty và cộng đồng theo nhiều giấy phép miễn phí khác nhau (BSD, MIT, Apache 2.0) đang phát triển hàng chục biến thể của lõi, SoC và chip vi xử lý đã được sản xuất.

Hỗ trợ RISC-V đã có từ khi phát hành Glibc 2.27, binutils 2.30, gcc 7 và nhân Linux 4.15.

Giới thiệu về thử nghiệm kênh vi mô seL4

Ban đầu, kênh vi mô seL4 đã được xác minh cho bộ xử lý ARM 32-bit, Và sau cho bộ xử lý x86 64-bit.

Có thể thấy rằng sự kết hợp của kiến ​​trúc phần cứng mở RISC-V với kênh vi mạch mở seL4 sẽ đạt được cấp độ bảo mật mới, vì các thành phần phần cứng trong tương lai cũng có thể được xác minh đầy đủ, điều này không thể đạt được đối với các kiến ​​trúc phần cứng độc quyền.

Khi chúng tôi kiểm tra seL4, chúng tôi phải giả định rằng phần cứng đang hoạt động bình thường (nghĩa là, như được chỉ định). Điều đó giả định rằng có một thông số kỹ thuật rõ ràng ngay từ đầu, điều này không đúng với tất cả các phần cứng. 

Nhưng ngay cả khi một đặc tả như vậy tồn tại, và nó là chính thức (nghĩa là, theo một chủ nghĩa hình thức toán học hỗ trợ lý luận toán học về các thuộc tính của nó), làm sao chúng ta biết rằng nó thực sự nắm bắt được hành vi của phần cứng? 

Thực tế là chúng ta có thể chắc chắn rằng không phải như vậy. Phần cứng không khác gì phần mềm ở chỗ cả hai đều có lỗi.

Nhưng có một ISA mở có những lợi thế vượt ra ngoài việc được miễn phí bản quyền. Một là nó cho phép triển khai phần cứng mã nguồn mở.

Khi kiểm tra seL4, người ta cho rằng thiết bị hoạt động như được chỉ ra và thông số kỹ thuật mô tả đầy đủ hoạt động của hệ thống, nhưng trên thực tế thiết bị không có lỗi, điều này được thể hiện rõ qua các vấn đề thường xuyên phát sinh trong cơ chế thực thi suy đoán. .

Nền tảng phần cứng mở giúp đơn giản hóa việc tích hợp các thay đổi liên quan đến bảo mật, chẳng hạn, để chặn tất cả các kênh rò rỉ có thể có thông qua các kênh của bên thứ ba, trong đó việc khắc phục sự cố bằng phần cứng hiệu quả hơn nhiều so với việc cố gắng tìm giải pháp bằng phần mềm.

Cuối cùng, nếu bạn muốn biết thêm về nó, bạn có thể tham khảo ghi chú trong liên kết theo dõi.