seL4操作系統(tǒng)內(nèi)核

seL4 是一個安全操作系統(tǒng)內(nèi)核，旨在確保現(xiàn)實(shí)世界中關(guān)鍵計(jì)算機(jī)系統(tǒng)的機(jī)密性、安全性和可靠性。

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

seL4 是世界上第一個通過數(shù)學(xué)方法被證明安全的操作系統(tǒng)內(nèi)核，并且是世界上最快、最先進(jìn)的 OS 微內(nèi)核。它對于嵌入式計(jì)算系統(tǒng)的安全可信賴方面將會有極大意義，具體來看可能影響到航空電子、自動駕駛汽車、醫(yī)療設(shè)備、關(guān)鍵基礎(chǔ)設(shè)施與國防等行業(yè)。

理論上，SeL4 可以用作 Linux 和其它類 Unix 操作系統(tǒng)的底層基礎(chǔ)，甚至此前曾被考慮用于 GNU/Linux “真內(nèi)核” GNU Hurd。