Linux 基金會正在與澳大利亞國家科學機構 CSIRO 合作，打造 seL4 操作系統微內核生態。

近日 Linux 基金會宣布托管 seL4 基金會，該基金會以澳大利亞國家科學機構 CSIRO 的數字機構?Data61 創建的 seL4?操作系統微內核為基礎項目。seL4 是一個安全操作系統內核，旨在確保現實世界中關鍵計算機系統的機密性、安全性和可靠性。

基金會創始成員包括 Cog Systems、DornerWorks、Ghost Locomotion、HENSOLD Cyber 與 UNSW Sydney。

seL4 是 L4 微內核家族的成員，它為系統中運行的應用之間的隔離提供了最高級別保障，可以遏制系統某一部分的危害，并防止損害系統中其它可能更關鍵的部分。

據介紹，seL4 是世界上第一個通過數學方法被證明安全的操作系統內核，并且在安全的基礎上還強調高性能，是世界上最快、最先進的 OS 微內核。

它對于嵌入式計算系統的安全可信賴方面將會有極大意義，具體來看可能影響到航空電子、自動駕駛汽車、醫療設備、關鍵基礎設施與國防等行業。

理論上，SeL4 可以用作 Linux 和其它類 Unix 操作系統的底層基礎，甚至此前曾被考慮用于 GNU/Linux “真內核” GNU Hurd。?

推薦閱讀

Django采用新的項目治理模型

開源：從“復興”走向“商業化”

蘋果招兵買馬，或在開源領域有大動作？

Eclipse Theia 1.0發布，VS Code真正的開源替代方案

Linus談居家辦公：不要在家中重新搞一個辦公室

總結

以上是生活随笔為你收集整理的世界上首个被数学证明安全的OS微内核seL4成立基金会的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。