微內(nèi)核seL4 7.0.0版本發(fā)布，提供了另外一種基于CMake的構(gòu)建系統(tǒng)，支持源碼樹(shù)外構(gòu)建和交互式配置。該版本還支持獨(dú)立的ia32構(gòu)建，并包含aarch64的詳細(xì)文檔。

seL4是一個(gè)高可靠性開(kāi)源微內(nèi)核，提供基于端到端驗(yàn)證的強(qiáng)隔離保障。實(shí)際上，這是說(shuō)seL4代碼庫(kù)是uestions#Does_seL4_have_zero_bugs.3F">無(wú)Bug的，當(dāng)“驗(yàn)證假設(shè)”滿足時(shí)，就發(fā)生指定的行為。正因如此，它已經(jīng)被用于將運(yùn)行在同一個(gè)處理器上的受信任組件和不受信任組件隔離。

seL4微內(nèi)核由NICTA開(kāi)發(fā)和維護(hù)，并通過(guò)了NICTA（現(xiàn)在是Data61的Trustworthy Systems Group）的正式驗(yàn)證，目前歸General Dynamics C4 Systems（GDC4S）所有。2014年，“為了幫助每個(gè)人構(gòu)建更可信賴（安全、無(wú)風(fēng)險(xiǎn)、可靠）的計(jì)算機(jī)系統(tǒng)”，NICTA和GDC4S決定開(kāi)源seL4。

功能正確性初步驗(yàn)證是在2009年通過(guò)L4.verified項(xiàng)目完成的。該項(xiàng)目表明，代碼正確地實(shí)現(xiàn)了正式的內(nèi)核規(guī)范。后續(xù)對(duì)該內(nèi)核的全面正式驗(yàn)證證明，該規(guī)范既能提供期望的高級(jí)安全屬性，如“可用性、權(quán)限限制、完整性和保密性”，又能提供那些用于代碼及二進(jìn)制級(jí)別轉(zhuǎn)譯的屬性。總的結(jié)果就是一個(gè)通用操作系統(tǒng)內(nèi)核的首次端到端驗(yàn)證。值得注意的是，10多年來(lái)，該驗(yàn)證一直隨著內(nèi)核的發(fā)展而變化，成為在這種規(guī)模下前所未有的驗(yàn)證。

按照設(shè)計(jì)，雖然seL4內(nèi)核有大量的驗(yàn)證工作，但它仍然保持著很高的性能，實(shí)際上，它已經(jīng)促進(jìn)了性能優(yōu)化的實(shí)現(xiàn)。當(dāng)前，驗(yàn)證提供的屬性和不變量用于獲悉內(nèi)核的最壞情況執(zhí)行時(shí)間（WCET），從而改進(jìn)內(nèi)核實(shí)現(xiàn)，進(jìn)一步減少WCET。類似地，增加的“快速路徑（fastpath）”在可能的時(shí)候會(huì)自動(dòng)提升進(jìn)程間通信（IPC）速度。后來(lái)，該驗(yàn)證經(jīng)過(guò)了擴(kuò)展，不管是否使用了快速路徑，都可以驗(yàn)證內(nèi)核行為是否符合規(guī)范。這項(xiàng)工作的結(jié)果就是一個(gè)速度、安全性、可靠性可證的內(nèi)核，其應(yīng)用領(lǐng)域包括國(guó)防、汽車、航空、醫(yī)療設(shè)備和工業(yè)自動(dòng)化。

美國(guó)通過(guò)SBIR（小型企業(yè)創(chuàng)新研究）項(xiàng)目發(fā)放了超過(guò)230萬(wàn)美元獎(jiǎng)金，用于資助那些與seL4相關(guān)的國(guó)防項(xiàng)目。在其中一個(gè)這樣的項(xiàng)目中，SMACCM團(tuán)隊(duì)使用seL4構(gòu)建了具有“非法入侵高度復(fù)原性”的無(wú)人機(jī)（UVV）。該團(tuán)隊(duì)使用seL4將運(yùn)行非關(guān)鍵代碼的虛擬化Linux實(shí)例和運(yùn)行在同一塊“任務(wù)板（mission board）”上的關(guān)鍵代碼隔離開(kāi)。在紅隊(duì)設(shè)法非法入侵時(shí)，藍(lán)隊(duì)仍然能夠有效地操作基于seL4的系統(tǒng)。該系統(tǒng)最初開(kāi)發(fā)時(shí)使用了一個(gè)普通的四軸飛行器，后來(lái)?yè)Q成了由Boeing開(kāi)發(fā)的“無(wú)人小鳥(niǎo)（ULB）”無(wú)人直升機(jī)。但是，seL4不限于國(guó)防承包商。由于支持Raspberry Pi 3，基于seL4開(kāi)發(fā)安全、無(wú)風(fēng)險(xiǎn)、可靠的系統(tǒng)也在學(xué)生的研究范圍內(nèi)。

雖然seL4在安全操作系統(tǒng)開(kāi)發(fā)領(lǐng)域最先進(jìn)，但按照定義，它是最小的，不是一個(gè)像Linux這樣的全功能操作系統(tǒng)，并沒(méi)有包含所有為了提供使用便利的東西，比如，支持各種設(shè)備及簡(jiǎn)單的進(jìn)程間通信。

開(kāi)發(fā)和驗(yàn)證工作的當(dāng)前狀態(tài)來(lái)自經(jīng)常更新的開(kāi)發(fā)和驗(yàn)證路線圖。常見(jiàn)問(wèn)題的答案可以從項(xiàng)目的FAQ頁(yè)查看。

查看英文原文：seL4 Bug-Free Microkernel 7.0.0