Giới thiệu về vi nhân seL4 [PDF]
(sel4.systems)- seL4 là một vi nhân OS nhắm tới các hệ thống nhúng và cyber-physical nơi bảo mật và an toàn là tối quan trọng; nó cô lập và đa hợp tài nguyên phần cứng nhưng không phải là một OS đa dụng hoàn chỉnh
- Bằng cách giảm mã chạy ở chế độ nhân xuống khoảng 10 kSLOC, seL4 thu nhỏ TCB và bề mặt tấn công, đồng thời đẩy các dịch vụ OS như hệ thống tệp, mạng và driver ra chế độ người dùng
- Đây là nhân OS đầu tiên trên thế giới có kiểm chứng hình thức ở cấp độ mã, và trong các hệ thống được cấu hình đúng, nhân còn đảm bảo các thuộc tính bảo mật như tính bí mật, toàn vẹn và sẵn sàng
- Kết hợp kiểm soát truy cập dựa trên capability, phân tích WCET, hỗ trợ hệ thống thời gian thực mixed-criticality và chức năng hypervisor, seL4 xử lý đồng thời cả cô lập chi tiết lẫn tính thời gian thực
- API của seL4 ở mức rất thấp nên khó tự xây dựng các hệ thống phức tạp trực tiếp; khi phù hợp với kiến trúc tĩnh, dùng framework như Microkit là cách thực tế hơn
Phạm vi mà seL4 đảm nhiệm
- seL4 là vi nhân, phần lõi cấp thấp của hệ điều hành
- OS kiểm soát phần cứng và tài nguyên trong kernel mode, chế độ thực thi có đặc quyền cao hơn của bộ xử lý
- Ứng dụng chạy ở chế độ người dùng và chỉ có thể truy cập phần cứng theo những cách mà OS cho phép
- Vi nhân là phần lõi của OS với lượng mã chạy ở mức đặc quyền cao được tối thiểu hóa
- seL4 thuộc dòng vi nhân L4, có lịch sử từ giữa thập niên 1990
- seL4 không liên quan đến seLinux
- seL4 không phải là một OS hoàn chỉnh mà là nhân cấp thấp để đa hợp và cô lập tài nguyên phần cứng một cách an toàn
- Các dịch vụ OS thông thường như hệ thống tệp, network stack và device driver không nằm trong nhân
- Những dịch vụ này phải được cung cấp bởi các chương trình ở chế độ người dùng
Kiến trúc vi nhân và giảm bề mặt tấn công
- Nhân nguyên khối như Linux cung cấp các dịch vụ OS như lưu trữ tệp và mạng bằng mã chạy trong kernel mode
- Mã kernel mode có thể truy cập tài nguyên hệ thống mà không bị hạn chế, nên nếu lỗi dẫn đến leo thang đặc quyền hoặc thực thi mã tùy ý thì toàn bộ hệ thống có thể bị xâm hại
- Nhân Linux có quy mô khoảng 20 MSLOC, và được ước tính có thể chứa hàng chục nghìn lỗi
- Một vi nhân được thiết kế tốt như seL4 giảm mã kernel mode xuống khoảng 10 kSLOC
- Quy mô này nhỏ hơn nhân Linux tới ba bậc độ lớn
- Khi TCB giảm, bề mặt tấn công cũng giảm theo
- Phần lớn dịch vụ OS được đưa ra ngoài nhân, và vi nhân hoạt động như một lớp bao mỏng quanh phần cứng
- Các chức năng cốt lõi mà nó cung cấp là cô lập giữa các chương trình và cơ chế gọi an toàn
- Dịch vụ không chạy trong nhân mà trở thành các chương trình user mode chạy trong các sandbox riêng
- Một nghiên cứu phân tích các vụ xâm phạm Linux đã biết với những trường hợp nghiêm trọng cho thấy thiết kế vi nhân có thể loại bỏ hoàn toàn 29% và giảm nhẹ thêm 55% đến mức không còn bị phân loại là nghiêm trọng nữa
PPC, capability và kiểm soát quyền hạn chi tiết
- seL4 cung cấp cơ chế PPC (protected procedure call)
- Vì lý do lịch sử, thuật ngữ IPC vẫn còn được dùng, nhưng cách gọi IPC có thể gây hiểu lầm và dẫn tới thiết kế kém
- PPC cho phép một chương trình gọi an toàn hàm của chương trình khác nằm trong sandbox khác
- Vi nhân truyền đầu vào và đầu ra trong PPC và ép buộc giao diện
- Hàm từ xa chỉ có thể được gọi tại các điểm vào đã được công bố
- Chỉ những client được cấp capability phù hợp và được cho phép rõ ràng mới có thể gọi
- Capability là token truy cập cho phép truy cập vào một tài nguyên cụ thể của hệ thống
- Nó cho phép kiểm soát rất chi tiết việc thực thể nào có thể truy cập tài nguyên nào
- Hỗ trợ nguyên tắc đặc quyền tối thiểu, hay POLA
- Các phương thức kiểm soát truy cập trong những hệ thống chủ đạo như Linux hay Windows không thể đạt được mức đặc quyền tối thiểu như vậy
- seL4 là OS duy nhất trên thế giới vừa dựa trên capability vừa được kiểm chứng hình thức, và nhờ sự kết hợp này được đánh giá là có thể đưa ra tuyên bố có cơ sở rằng đây là OS an toàn nhất thế giới
Kiểm chứng hình thức và đảm bảo bảo mật
- seL4 cung cấp chứng minh hình thức, toán học và được máy kiểm chứng về tính đúng đắn của hiện thực
- Chứng minh này có nghĩa rằng nhân “không có lỗi” theo nghĩa rất mạnh so với đặc tả
- seL4 là nhân OS đầu tiên trên thế giới có loại chứng minh này ở cấp độ mã
- Ngoài tính đúng đắn của hiện thực, seL4 còn cung cấp thêm các chứng minh về việc thực thi bảo mật
- Trong hệ thống dựa trên seL4 được cấu hình đúng, nhân đảm bảo tính bí mật, tính toàn vẹn và tính sẵn sàng
- Chuỗi kiểm chứng là điểm khác biệt cốt lõi của seL4
- Trong các hệ thống an toàn và bảo mật trọng yếu, để nhân trở thành nền tảng tin cậy thì cần các đảm bảo mạnh về cả hiện thực lẫn các thuộc tính bảo mật
Tính thời gian thực và hệ thống mixed-criticality
- seL4 là nhân OS đã trải qua phân tích đầy đủ và chặt chẽ về WCET (worst-case execution time)
- Nếu nhân được cấu hình phù hợp, mọi thao tác trong nhân đều có giới hạn thời gian
- Và các giới hạn đó cũng đã được biết trước
- Đặc tính này là điều kiện tiên quyết để xây dựng hệ thống thời gian thực cứng
- Nhắm tới các hệ thống mà việc không phản ứng với sự kiện trong khoảng thời gian bị ràng buộc nghiêm ngặt có thể dẫn tới hậu quả nghiêm trọng
- seL4 cũng hỗ trợ MCS (hệ thống thời gian thực mixed-criticality)
- Nhắm tới môi trường mà ngay cả khi mã có độ tin cậy thấp hơn cùng chạy trên một nền tảng, tính thời gian của các hoạt động quan trọng vẫn phải được đảm bảo
- Không giống cách phân vùng thời gian-không gian cứng nhắc và kém linh hoạt mà các OS MCS truyền thống sử dụng, seL4 cung cấp một mô hình linh hoạt vẫn duy trì được mức sử dụng tài nguyên
seL4 khi dùng làm hypervisor
- seL4 vừa là vi nhân vừa là hypervisor
- Có thể chạy máy ảo trên seL4
- Bên trong máy ảo có thể chạy các guest OS thông thường như Linux
- Guest và ứng dụng có thể giao tiếp với nhau theo các kênh liên lạc mà seL4 áp đặt
- Cũng có thể giao tiếp với các ứng dụng native
- Có thể dùng Linux VM như một phương tiện cung cấp dịch vụ hệ thống
- Trong cấu hình ví dụ, các dịch vụ như mạng và lưu trữ được lấy từ nhiều instance Linux chạy trong các VM riêng biệt
Cách xây dựng hệ thống trên seL4
- API của seL4 ở mức rất thấp, ngay cả khi so với các vi nhân khác
- Nó chỉ cung cấp các trừu tượng tối thiểu cần thiết để quản lý phần cứng một cách an toàn
- seL4 được ví như “assembly của hệ điều hành”
- Việc trực tiếp xây dựng các hệ thống phức tạp trên seL4 không phải là cách phù hợp
- Cần có framework cấp cao hơn để tập trung vào mã hiện thực dịch vụ, đồng thời tự động hóa độ phức tạp phần cứng và tích hợp hệ thống
- seL4 có ba framework thành phần mã nguồn mở chính
- Microkit: đơn giản hóa API seL4 bằng một số ít trừu tượng xoay quanh protection domain, đồng thời cung cấp SDK để tích hợp các module biên dịch riêng và binary của nhân thành image có thể khởi động
- CAmkES: tiền thân của Microkit và là framework thành phần cho các hệ thống kiến trúc tĩnh, nhưng không có SDK nên quy trình build bất tiện hơn và overhead lớn hơn
- Genode: hỗ trợ nhiều vi nhân, có phong phú dịch vụ và driver cho nền tảng x86, và không ép buộc kiến trúc tĩnh, nhưng không tận dụng được toàn bộ các tính năng an toàn và bảo mật của seL4, đồng thời không có câu chuyện bảo chứng rõ ràng
- Miễn là kiến trúc hệ thống tĩnh phù hợp với yêu cầu, Microkit được khuyến nghị để xây dựng hệ thống dựa trên seL4
- Kiến trúc tĩnh là mô hình trong đó tập hợp module và cấu trúc giao tiếp được xác định tại thời điểm cấu hình hệ thống
- Mô hình này được xem là phù hợp với yêu cầu của phần lớn hệ thống nhúng, bao gồm cả các hệ thống cyber-physical phức tạp như ô tô và máy bay
1 bình luận
Các ý kiến trên Hacker News
Bản thân seL4 đã là câu chuyện cũ, nhưng tôi tò mò liệu đã có thêm các tầng hoặc thành phần được kiểm chứng hình thức mới nào vượt ra ngoài microkernel hay chưa.
Ngoài ra, có vẻ cũng có những người cứ thấy từ “chứng minh” là bị quá tải cảm xúc và ngừng suy nghĩ. Kiểm chứng hình thức không phải là thuốc chữa bách bệnh cho bài toán vô hạn về IT an toàn, cũng không phải là cách tạo ra phần mềm hoàn hảo không tì vết.
Theo tôi hiểu, đó là chứng minh rằng trong những điều kiện nhất định, các yêu cầu nhất định được thỏa mãn; các yêu cầu và điều kiện đó có thể khá hẹp, và nó không nói gì về các chức năng hay điều kiện nằm ngoài đặc tả. Không biết hiểu như vậy có đại khái đúng không.
Về mặt thực tế, tôi cũng tò mò chuyên gia bảo mật kỳ vọng gì khi thấy “phần mềm được kiểm chứng hình thức”. Có lẽ đặc tả mà seL4 thỏa mãn mới là thông tin cốt lõi ở đây.
https://github.com/seL4/seL4/pull/243
https://github.com/seL4/l4v/pull/453
Trong trình theo dõi issue cũng có nhiều bug liên quan đến bộ nhớ.
https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
Thú vị là PR sửa lỗi “register clobbering” trong bộ nhớ lại không gắn nhãn bug, nên nếu lọc theo “bug” thì sẽ không thấy. Trước đây tôi từng nghĩ nhờ chứng minh mà seL4 miễn nhiễm với những vấn đề như vậy, nhưng sau khi thấy điều này, tôi cho rằng chứng minh đó không bao quát như cộng đồng đã tin. Dù vậy seL4 vẫn là một phần mềm rất ấn tượng.
Trả lời câu hỏi thì đặc tả mà seL4 thỏa mãn được công khai trên GitHub.
https://github.com/seL4/l4v
Lập lịch mixed-criticality cung cấp cách tiếp cận dựa trên capability đối với thời gian CPU, giới hạn trần thực thi của thread, bảo đảm ưu tiên và quyền truy cập tài nguyên cho tác vụ có mức quan trọng cao, cũng như “passive servers” chạy bằng thời gian lập lịch do bên gọi đóng góp.
Microkit là một tầng trừu tượng đã được kiểm chứng, giúp việc xây dựng hệ thống thực tế trên seL4 dễ hơn nhiều; còn Device Driver Framework là bộ mẫu driver thiết bị, phần triển khai control/data plane, cùng công cụ viết driver và ảo hóa thiết bị cho I/O hiệu năng cao trên seL4.
Kiểm chứng hình thức có thể bảo đảm rằng trong các điều kiện nhất định, các yêu cầu nhất định được thỏa mãn. Nói chung, đúng là các yêu cầu và điều kiện như vậy có thể hẹp, nhưng riêng seL4 có nhiều chứng minh bao phủ một phạm vi rộng các thuộc tính có thể kỳ vọng ở kernel, và các bảo đảm đó vẫn đúng dưới những giả định rất yếu. Thậm chí không giả định C compiler là đúng; có một công cụ riêng xem xét đầu ra của compiler và chứng minh rằng binary đã biên dịch hoạt động đúng theo ngữ nghĩa C được yêu cầu.
Các yêu cầu mà seL4 thỏa mãn bao gồm việc mã binary của kernel seL4 triển khai chính xác hành vi được mô tả trong đặc tả trừu tượng và không làm gì hơn thế. Không có buffer overflow, rò rỉ bộ nhớ, lỗi con trỏ, dereference con trỏ null, hành vi không xác định trong mã C, hay việc kernel bị kết thúc ngoài các cách tường minh được liệt kê trong đặc tả.
Đặc tả và binary seL4 cũng thỏa mãn các thuộc tính bảo mật về tính toàn vẹn và tính bí mật. Tính toàn vẹn nghĩa là tiến trình hoàn toàn không có cách nào thay đổi dữ liệu mà nó không có quyền tường minh; tính bí mật nghĩa là không thể đọc dữ liệu không được cấp quyền bằng bất kỳ cách nào. Nó còn cho thấy không thể suy luận dữ liệu gián tiếp qua một số kênh phụ nhất định. Ngoài bảo mật, nó cũng đáp ứng các bảo đảm về thời gian thực thi tệ nhất dự kiến và các thuộc tính lập lịch.
Công việc hiện tại thiên về LionsOS, nhằm hướng đến việc được áp dụng rộng hơn: https://lionsos.org/
https://docs.sel4.systems/projects/sel4/frequently-asked-que...
Dự án dùng nhiều lập trình ở cấp kiểu để theo dõi tài nguyên, quyền truy cập phần cứng và capability tại thời điểm biên dịch. Vì việc phát hiện vấn đề và debug ở runtime quá tệ, đây là một nỗ lực đưa một phần các bảo đảm của kernel nền tảng lên phía compiler.
Tôi thích microkernel host chạy guest monolithic kernel, nên các server đang chạy seL4 làm tầng an toàn và sao lưu cho FreeBSD VM, bên trong đó dùng jail cho renderfarm, cụm BEAM và Jenkins.
Điều đáng tiếc là không có bản port ARM cho threading và kernel nội bộ tiến trình của DragonflyBSD, tức thiết kế hybrid kernel. Giấc mơ là chạy OpenMoonRay hiệu quả hơn trên Ampere Altra 128 nhân.
Giờ đây có vẻ bản thân cuộc tranh luận ủng hộ hay phản đối microkernel không còn nhiều ý nghĩa nữa. Cách duy nhất để truy cập các dịch vụ có đặc quyền một cách nhanh, hiệu quả và an toàn là các biện pháp giảm thiểu ở phần cứng, còn những gì phần mềm có thể làm thì có giới hạn
Tương tự như khác biệt giữa 80286 và 80386. Loại sau bổ sung hỗ trợ phần cứng thực sự cho multitasking mà loại trước không có. Kể từ đó, các cơ chế bảo vệ ở cấp phần cứng, như những thứ đã làm hypervisor trở nên khả thi, tiếp tục tăng lên
Đặc biệt Apple đang đưa rất nhiều chức năng vào SoC để bảo vệ kernel, driver và các thành phần ở cấp chip, cũng như cưỡng chế quyền hạn khi sử dụng thread và pointer đang chạy. https://support.apple.com/guide/security/operating-system-in...
Điều đó không có nghĩa là OS không thể bị xuyên thủng, nhưng nó hiệu quả hơn nhiều so với chiến lược quản lý quyền hạn chỉ bằng phần mềm. Nếu tận dụng các tính năng như vậy hoặc những thứ tương tự, cấu trúc kernel dường như không còn quan trọng đến thế nữa; tôi tò mò không biết mình có sai không
Cũng có nhiều điều để học từ các hệ thống micro/hybrid có khả năng kết hợp tốt hơn. Ví dụ Plan 9 là một hệ thống hybrid xuất sắc, cung cấp mọi đối tượng của hệ thống cho user space qua một giao thức duy nhất là 9P. Nó là hybrid vì một số phần, như IP hay TLS, nằm trong kernel để tránh overhead của system call
Một thiết kế thú vị khác là driver bên trong kernel phần lớn chỉ ở dạng tối thiểu, đóng vai trò như giao diện 9P cho logic phần cứng. Cách này biến các đối tượng máy như pointer hay record thành file có thể duyệt, bảo vệ các file đó bằng quyền Unix tiêu chuẩn, và dễ dàng phân tán các thành phần qua mạng trên nhiều máy. Kết quả là logic driver có thể được đẩy an toàn sang các chương trình user space
9P trong suốt với mạng và kiến trúc, nên có thể làm việc ngay cùng nhau trên nhiều máy như Arm, x86, mips, v.v. Từ Plan 9 quay lại Linux/Unix hay Windows thì thấy buồn và bức bối. Độ linh hoạt gần như ngang đá magma, và các chức năng được chắp thêm theo vô số giao thức làm cùng một việc là cung cấp file/đối tượng, khiến chúng không tương thích với nhau
Từ góc nhìn kỹ thuật thực dụng, kernel nguyên khối nhanh hơn, dễ hơn và có nhiều tài nguyên hơn; còn bảo mật thì chỉ ở mức C có thể làm được, tức là nỗ lực tối đa kèm vô số bug. Rất nhiều phần cứng đã được đưa vào để giảm nhẹ mớ hỗn độn đó. Nhưng với SeL4, vì mức độ tin cậy vào cách ly giữa các process và việc không có exploit cấp root là rất cao, về lý thuyết có thể không cần bộ đồng xử lý bảo mật. Vì vậy đồng thiết kế phần cứng/phần mềm là quan trọng
Tuy nhiên, đội SeL4 cũng đã phải dùng nhiều tài nguyên kỹ thuật để loại bỏ kênh kề của phần cứng. Thế giới thực không quan tâm đến mô phỏng vật lý, nên phần cứng cũng có khiếm khuyết
Điểm mạnh của microkernel ở đây là nó đủ nhỏ để formal verification có thể xử lý. Bản chứng minh tự nó lớn gấp 10 lần kích thước kernel. Context switch của SeL4 nhanh hơn Linux một bậc độ lớn, nên ảnh hưởng hiệu năng đáng ra là có thể bỏ qua. Nhưng nếu có thể xác minh một kernel nguyên khối hàng triệu dòng một cách kỳ diệu, thì không context switch vẫn nhanh hơn. Thực tế đội SeL4 từng cố chuyển scheduler sang user space, nhưng chi phí hiệu năng quá lớn nên họ để nó lại trong kernel và cộng thêm vào gánh nặng chứng minh
Ngược lại, vai trò chính của phần cứng là tăng hiệu quả. Ví dụ microkernel ngày nay đã tận dụng tốt phần cứng như MMU nên khá vững chắc. Sau đó trusted computing base nhỏ của microkernel đem lại độ tin cậy cho kernel, và kernel cùng phần cứng tạo nên một nền tảng vững chắc
Cuối cùng đây là vấn đề cho phép “ăn gian” đến mức nào bằng phần cứng, nhưng nhìn chung microkernel tận dụng các chức năng bảo vệ tốt hơn. Hoặc cũng có thể xem exokernel
https://genode.org/index
Đây là một hệ điều hành có hỗ trợ seL4
Tôi từng thuyết trình về SeL4 tại một chapter OWASP địa phương. Không biết có còn tìm được tài liệu không
Dự án này thực sự là một thứ được làm rất tốt, nhưng đặc biệt trong điện toán đa dụng thì tôi vẫn ngần ngại xem nó là phương án thay thế Linux. Nói vậy không có nghĩa là microkernel nói chung là tệ cho mục đích đa dụng. RedoxOS gần đây có vẻ đã có một số tiến triển và dùng microkernel viết bằng Rust
Dù vậy, nếu Redox thành công thì chỉ riêng điều đó đã là một bước tiến tốt. seL4 còn cực đoan hơn ở đặc tính này. Ưu điểm kỹ thuật thì xuất sắc, nhưng cho đến nay, và có lẽ cả về sau, nó dường như sẽ không có thứ gì đó để trở thành “xu hướng lớn tiếp theo”. Nếu bỏ qua các cân nhắc chính trị, tôi nghĩ microkernel sẽ thành công, và cũng nên thành công
Để seL4 thực sự hữu ích thì cần nhiều thứ bên trên nó. May mắn là cũng đã có nhiều công việc mã nguồn mở được thực hiện ở phần đó, và hiện ở vị thế tốt hơn nhiều so với vài năm trước
Với các kịch bản tĩnh thì có LionsOS[0], và nó đã khá dùng được
Với các kịch bản động thì có Provably Secure, General-Purpose Operating System[1], nhưng vẫn còn ở giai đoạn đầu
Cả hai đều có thể tìm thấy trên trang Projects[2] của trustworthy systems, được liên kết từ website seL4
[0] https://trustworthy.systems/projects/LionsOS/
[1] https://trustworthy.systems/projects/smos/
[2] https://trustworthy.systems/projects/
Tôi tò mò liệu OS chạy trên kernel này cũng phải được kiểm chứng hình thức thì các bảo đảm bảo mật mới có hiệu lực hay không
Tất nhiên chỉ riêng kernel thì không hữu ích lắm, nên thiết kế của driver, server hệ thống tệp và các dịch vụ khác chạy trên kernel vẫn rất quan trọng
Cũng cần nhấn mạnh rằng hầu hết các hệ thống khác, bao gồm Linux, đều có khiếm khuyết ở tầng nền tảng, còn seL4 thực sự cho phép tạo ra các hệ thống an toàn và đáng tin cậy
Vì vậy có thể chạy kernel Linux bên cạnh một tiến trình bảo mật cao, đồng thời vẫn có bảo đảm rằng chúng bị cách ly với nhau, ngoại trừ IPC được cho phép
Nhưng có giới hạn. DMA phải bị tắt, và driver cũng chỉ nên dùng những cái đã được kiểm chứng hình thức
Một điểm quan trọng nữa là kernel đa lõi của seL4 vẫn chưa được kiểm chứng
Helios Microkernel của Drew DeVault cũng đáng xem. Nghe nói dựa trên SeL4
https://ares-os.org/docs/helios/
Tại Đại học Karlsruhe, L4 từng khá phổ biến. Tôi chưa từng xem xét kỹ, nhưng nó trông giống một dự án chủ yếu quan tâm đến việc thử nghiệm các ý tưởng lý thuyết hơn là tạo ra thứ gì đó hữu dụng trong thực tế
Đó là chuyện 20 năm trước, và theo tôi thì đến nay cũng không khác nhiều. Tìm nhanh thì có vẻ có vài nỗ lực xây dựng OS bên trên nó, nhưng trông giống bằng chứng khái niệm hơn là dùng thực tế
“Số lượng xuất xưởng OKL4 đã vượt 1,5 tỷ vào đầu năm 2012, phần lớn là chip modem không dây Qualcomm. Các triển khai khác bao gồm hệ thống thông tin giải trí trên ô tô”
“Các bộ xử lý Apple A-series bắt đầu từ A7 chứa một bộ đồng xử lý Secure Enclave chạy hệ điều hành L4; OS này là sepOS, dựa trên kernel L4-embedded được phát triển tại NICTA năm 2006. Kết quả là L4 có mặt trên mọi thiết bị Apple hiện đại, bao gồm cả Mac dùng Apple silicon”
Rittinghaus, cựu sinh viên của Bellosa, tham gia Unikraft[0], vốn đã vài lần được giới thiệu trên HN, và sử dụng công nghệ unikernel
[0] https://unikraft.org/
“Secure Enclave Processor chạy một phiên bản vi nhân L4 do Apple tùy biến”
https://support.apple.com/de-at/guide/security/sec59b0b31ff/...
https://www.kernkonzept.com/kk_events/elektrobit-advances-au...
Theo tôi thấy, kernel L4Re cũng là một phần của Elektrobit Safe Linux
Tôi đã làm một OS dựa trên Pistachio cho luận văn tốt nghiệp. Tôi luôn nghĩ rằng nếu mình học ở Karlsruhe thì có lẽ đã đi theo hướng nghiên cứu OS
Tôi cũng từng có ý tưởng thiết kế hệ điều hành, và capability mà tôi cân nhắc dùng các chức năng can thiệp trung gian và ủy quyền giống seL4. Ngoài những gì được viết ở đó, nó còn có lợi ích khác. Ví dụ có thể dùng proxy capability để áp dụng bộ lọc cho âm thanh hoặc triển khai tính trong suốt mạng
Tôi nghĩ có thể cho phép chức năng thời gian thực như một triển khai tùy chọn. Ý tưởng của tôi giống một đặc tả hơn là một triển khai duy nhất
Một tính năng khác tôi muốn là mọi chương trình, ngoại trừ nhập/xuất, đều hoạt động theo cách xác định. Nếu không có nhập/xuất thì không thể biết ngày/giờ hay thời gian chạy chương trình, và cũng không thể kiểm tra tính năng của bộ xử lý. Nếu dùng một tính năng mà phần cứng không hỗ trợ, hệ điều hành có thể mô phỏng
Để triển khai điều này, tôi định kết hợp hỗ trợ phần cứng và phần mềm. Tài liệu có ghi chú về một cuộc tấn công đối với capability được triển khai bằng phần cứng, nhưng tôi không có tài liệu tham khảo nên không biết cuộc tấn công đó có áp dụng cho cách tôi nghĩ tới hay không
Từ góc nhìn bảo mật, có vẻ nó có thất bại giống KVM của kernel Linux. Nếu hypervisor ở ring 0, sẽ có rủi ro thoát từ một VM sang VM khác hoặc sang chính host
Tôi tò mò họ giảm thiểu rủi ro đó như thế nào
VMM không có nhiều capability hơn chính VM, nên ngoài ý nghĩa học thuật thì việc thoát VM không có nhiều giá trị
Xem trang 8–10 của PDF gốc