世界上首個被數學證明安全的操作系統微內核seL4 成立基金會
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。