形式化驗(yàn)證在安全操作系統(tǒng)的發(fā)展中成為了熱門話題！sel4在其官方網(wǎng)站上宣稱：安全絕不應(yīng)成為表現(xiàn)不佳的借口！

seL4是什么？seL4是L4微內(nèi)核家族中最先進(jìn)的成員，以其全面的形式驗(yàn)證而著稱，這使其與其他操作系統(tǒng)截然不同。seL4在實(shí)現(xiàn)這一目標(biāo)的同時(shí)，性能并未受損。

什么是微內(nèi)核？微內(nèi)核是操作系統(tǒng)（OS）的核心最小部分。它通常被視為今天的操作系統(tǒng)的一個(gè)小型子集。微內(nèi)核的定義由利特克在[SOSP’95]中提出。因此，微內(nèi)核不提供如Linux或Windows等現(xiàn)代操作系統(tǒng)那樣在硬件上實(shí)現(xiàn)的高層次抽象（如文件、進(jìn)程、套接字等）。相反，它提供了最基本的機(jī)制來(lái)控制物理地址空間訪問(wèn)、中斷和處理器時(shí)間。在L4微內(nèi)核使用的模式中（seL4亦是如此），一旦內(nèi)核啟動(dòng)，一個(gè)初始的用戶級(jí)任務(wù)（根任務(wù)）將獲得完全權(quán)限來(lái)管理所有資源（通常包括物理內(nèi)存、x86的IO端口和中斷）。根任務(wù)負(fù)責(zé)設(shè)置其他任務(wù)，并向其他任務(wù)授予權(quán)限以構(gòu)建完整的系統(tǒng)。在seL4中，像其他第三代微內(nèi)核一樣，這樣的訪問(wèn)權(quán)限是通過(guò)能力授予的（不可偽造的令牌代表特權(quán)），且是完全可委托的。

L4微內(nèi)核家族是什么？L4家族是一系列非常小型且高性能的微內(nèi)核。第一個(gè)L4微內(nèi)核由約亨·利特克在90年代初研制，并不斷演化。參見(jiàn)《From L3 to seL4 What Have We Learnt in 20 Years of L4 Microkernels?》，這是一篇2013年關(guān)于微內(nèi)核發(fā)展的系統(tǒng)性介紹論文。原文下載地址：https://www.php.cn/link/0c5bcd68aebc9060a7f2e5047bb962de：

seL4的性能與其他微內(nèi)核相比如何？據(jù)我們所知，seL4在常見(jiàn)的乒乓指標(biāo)上，即跨地址空間的消息傳遞（IPC）的操作成本，是世界上最快的微內(nèi)核之一，欲了解更多信息，請(qǐng)查看L4HQ的性能頁(yè)面：https://www.php.cn/link/78106a0fa774284d86ec3585a5112ca5。

需要注意的是，L4HQ記錄的IPC時(shí)間是經(jīng)過(guò)微優(yōu)化的結(jié)果，這些優(yōu)化尚未包含在公開(kāi)版本中。發(fā)布的內(nèi)核大約慢了10-20%的速度（這仍然使其比我們已知的其他性能數(shù)據(jù)快）。我們計(jì)劃一旦這些優(yōu)化成熟，就推動(dòng)其應(yīng)用。

seL4運(yùn)行在什么硬件上？它支持哪些處理器架構(gòu)？目前，seL4運(yùn)行在ARMv6（ARM11）、ARMv7（Cortex A8、A9、A15）和x86核心上。支持的ARM平臺(tái)包括飛思卡爾的i.MX31、OMAP3的BeagleBoard、Exynos Arndale 5250、Odroid-X、Odroid-XU、Inforce IFC6410和Freescale i.MX6 Sabre Lite。也支持所有現(xiàn)代的x86機(jī)器。

seL4支持什么設(shè)備？seL4像任何真正的微內(nèi)核一樣，在用戶模式下執(zhí)行所有的設(shè)備驅(qū)動(dòng)程序，因此設(shè)備支持不是內(nèi)核的問(wèn)題。唯一的例外是一個(gè)時(shí)鐘驅(qū)動(dòng)程序，seL4需要它來(lái)執(zhí)行時(shí)間片搶占，以及seL4處理的中斷控制器訪問(wèn)。當(dāng)啟用調(diào)試時(shí)編譯內(nèi)核時(shí)，內(nèi)核還包含了一個(gè)串口驅(qū)動(dòng)程序。除此之外，設(shè)備支持是用戶的問(wèn)題。seL4提供了用戶模式設(shè)備驅(qū)動(dòng)程序的機(jī)制，尤其是映射設(shè)備內(nèi)存到驅(qū)動(dòng)和將IRQ作為（異步）消息傳遞的能力。

DMA如何處理？在ARM平臺(tái)上，seL4的形式化驗(yàn)證假設(shè)MMU完全控制內(nèi)存，這意味著證明假設(shè)DMA是關(guān)閉的。DMA設(shè)備理論上可以覆蓋機(jī)器上的任何內(nèi)核，包括內(nèi)核數(shù)據(jù)和代碼。你仍然可以安全地使用DMA設(shè)備，但你必須單獨(dú)確保它們正常工作，即不覆蓋內(nèi)核代碼或數(shù)據(jù)結(jié)構(gòu)，只寫(xiě)入按照系統(tǒng)策略分配給它們的幀上。在實(shí)踐中，這意味著驅(qū)動(dòng)程序和DMA硬件設(shè)備必須是可靠的。未經(jīng)驗(yàn)證的seL4 x86版本在實(shí)驗(yàn)分支上支持VT-d擴(kuò)展。VT-d擴(kuò)展允許內(nèi)核限制DMA，從而使DMA設(shè)備能與不受信任的用戶級(jí)驅(qū)動(dòng)程序交互。目前，我們正在為具備SystemMMU的A15 ARM板提供類似的驗(yàn)證支持。

我可以在seL4上運(yùn)行Linux嗎？是的，seL4可以在虛擬機(jī)上運(yùn)行Linux。目前僅支持x86處理器，同時(shí)seL4要求機(jī)器支持英特爾EPT VT-X。此外，目前的VMM需要支持MSI delivery的HPET。我們正在研究基于ARM處理器上的Linux的虛擬化擴(kuò)展支持（目前是A15/A7核心），發(fā)布應(yīng)該不會(huì)太久。

為了支持虛擬機(jī)，seL4本身作為一個(gè)虛擬機(jī)管理程序運(yùn)行（x86 Ring-0根模式或ARM hyp模式）并轉(zhuǎn)發(fā)虛擬化事件到虛擬機(jī)監(jiān)視器（VMM），VMM執(zhí)行必要的仿真。VMM運(yùn)行在脫特權(quán)模式（x86 Ring-3根模式或ARM supv模式）。

seL4支持多核嗎？在x86上，seL4可以配置為支持多個(gè)CPU。目前多核的支持是通過(guò)一個(gè)多核配置實(shí)現(xiàn)，每個(gè)啟動(dòng)CPU被分配一部分可用內(nèi)存。然后，內(nèi)核可以通過(guò)受限的共享內(nèi)存和內(nèi)核支持的IPI通信。

我可以在沒(méi)有MMU的微控制器上運(yùn)行seL4嗎？在沒(méi)有完整的存儲(chǔ)器管理單元（MMU）上使用seL4沒(méi)有意義，因?yàn)樗馁Y源管理基本上是基于虛擬內(nèi)存的。對(duì)于只有一個(gè)內(nèi)存保護(hù)單元（MPU）或完全沒(méi)有內(nèi)存保護(hù)的低端處理器，你應(yīng)該看看NICTA的eChronos實(shí)時(shí)操作系統(tǒng)（RTOS），這是專為這樣的處理器設(shè)計(jì)的，也經(jīng)過(guò)形式化驗(yàn)證。

seL4為哪些應(yīng)用程序服務(wù)？seL4是一個(gè)通用的微內(nèi)核，因此適用于所有應(yīng)用程序。主要目標(biāo)是有安全性或可靠性要求的嵌入式系統(tǒng)，但這不是唯一的。采用像seL4的微內(nèi)核能夠提供虛擬內(nèi)存保護(hù)平臺(tái)，并應(yīng)用于需要在軟件的不同部分之間隔離的應(yīng)用領(lǐng)域。直接的應(yīng)用領(lǐng)域包括金融、醫(yī)療、汽車、航空電子設(shè)備和國(guó)防部門。

什么是形式驗(yàn)證？形式軟件驗(yàn)證是用數(shù)學(xué)證明來(lái)說(shuō)明一款軟件滿足特定屬性。傳統(tǒng)上，形式驗(yàn)證已被廣泛用于說(shuō)明設(shè)計(jì)或一個(gè)軟件的規(guī)范都有一定的屬性，或者一個(gè)設(shè)計(jì)正確地實(shí)現(xiàn)了一個(gè)規(guī)范。在最近幾年，已經(jīng)可能直接應(yīng)用形式驗(yàn)證到實(shí)現(xiàn)該軟件的代碼上，并表明該代碼具有特定的性質(zhì)。形式驗(yàn)證有兩種方式：完全自動(dòng)化的方法，如有限的系統(tǒng)和屬性的模型檢驗(yàn)工作，以及交互的數(shù)學(xué)證明，需要手動(dòng)操作。seL4驗(yàn)證使用了Isabelle/HOL定理證明的形式數(shù)學(xué)證明。該定理證明是交互的，但提供的自動(dòng)化程度較高。它也提供了高度的保證來(lái)確保所產(chǎn)生的證明是正確的。

seL4的形式驗(yàn)證意味著什么？seL4的獨(dú)特之處是通過(guò)形式驗(yàn)證來(lái)實(shí)現(xiàn)前所未有程度的保證。具體來(lái)說(shuō)，seL4的ARM版本是第一個(gè)（也是目前唯一）帶有一個(gè)完整的代碼級(jí)的功能正確性證明的通用操作系統(tǒng)內(nèi)核，這意味著一個(gè)數(shù)學(xué)證明的實(shí)現(xiàn)（用編寫(xiě)c語(yǔ)言）支持其規(guī)格。簡(jiǎn)言之，實(shí)現(xiàn)被證明是無(wú)缺陷的（見(jiàn)下文）。這也意味著一些其他屬性，如避免緩沖區(qū)溢出、空指針異常、釋放后使用等等。更進(jìn)一步，有在硬件上執(zhí)行的二進(jìn)制代碼是C代碼的正確轉(zhuǎn)換的相關(guān)證明。這意味著，編譯器不必被信任，并且擴(kuò)展了二進(jìn)制的功能正確性屬性。此外，也有證明來(lái)證實(shí)seL4的規(guī)格，如果使用得當(dāng)，會(huì)強(qiáng)制完整性和保密性，核心安全屬性。結(jié)合上面提到的證明，不僅在內(nèi)核模型上（規(guī)范），也在執(zhí)行的二進(jìn)制的硬件上，這些屬性都被保證強(qiáng)制實(shí)施。因此，seL4是世界上第一個(gè)（也是目前唯一）在一個(gè)極強(qiáng)的意義上被證明是安全的操作系統(tǒng)。最后，seL4是第一個(gè)（也是目前唯一），保護(hù)模式的操作系統(tǒng)內(nèi)核與健全完善的時(shí)間性分析。這意味著其有對(duì)中斷延遲（以及任何其他的內(nèi)核操作的延遲）的可證明的上限。因此，它是有內(nèi)存保護(hù)的內(nèi)核中唯一的可以給你硬實(shí)時(shí)保證的。

seL4是否具有零錯(cuò)誤？功能正確性的證明指出，如果證明假設(shè)得到滿足，seL4內(nèi)核的實(shí)現(xiàn)與其規(guī)格相比就沒(méi)有偏差。安全證明指出，如果內(nèi)核是根據(jù)證據(jù)假設(shè)配置的，并進(jìn)一步滿足硬件的假設(shè)，本規(guī)范（和它的seL4內(nèi)核實(shí)現(xiàn)）強(qiáng)制執(zhí)行了一些強(qiáng)大的安全屬性：完整性、保密性和可用性。仍然有可能存在本規(guī)格中未意料到的功能，同時(shí)一種或多個(gè)的假設(shè)可能是不適用的。安全屬性可能足夠滿足你的系統(tǒng)的需求，但也可能并非如此。例如，保密證明沒(méi)有關(guān)于不存在的隱藏定時(shí)通道的保證。

因此，問(wèn)題的答案取決于你對(duì)錯(cuò)誤的理解。在形式軟件驗(yàn)證（代碼實(shí)現(xiàn)規(guī)范）的理解中，答案是肯定的。在一般的軟件用戶的理解中，答案是有可能的，因?yàn)檫€有可能是硬件錯(cuò)誤或未得到滿足的證明假設(shè)。對(duì)于高保障系統(tǒng)來(lái)說(shuō)，這不是一個(gè)問(wèn)題，因?yàn)橛布姆治龊妥C明的假設(shè)比分析具備相同的硬件，和測(cè)試假設(shè)的大型軟件系統(tǒng)容易的多。

seL4證明是安全嗎？這取決于你所說(shuō)安全的意思。在傳統(tǒng)的操作系統(tǒng)的安全性的解釋，答案是肯定的。特別是，seL4已被證明強(qiáng)制執(zhí)行特定的安全性能，即在一定條件下的完整性和保密性。這些證明都是關(guān)于seL4的程序用于構(gòu)建安全系統(tǒng)的非常有力的證據(jù)。一些證據(jù)的假設(shè)可能有限制條件，例如DMA的使用被排除在外，或僅允許由正式由用戶進(jìn)行驗(yàn)證的受信任驅(qū)動(dòng)程序。雖然這些限制對(duì)高保障系統(tǒng)是常見(jiàn)的，我們正在努力地以減少它們，例如通過(guò)在x86上使用IOMMU或在ARM上使用System MMU。

如果我運(yùn)行了seL4，我的系統(tǒng)就是安全嗎？這并不是自動(dòng)保證的。安全是一個(gè)跨越整個(gè)系統(tǒng)，包括與人交互那一部分的問(wèn)題。OS內(nèi)核，無(wú)論驗(yàn)證與否，并不會(huì)自動(dòng)使系統(tǒng)安全。事實(shí)上，任何系統(tǒng)，無(wú)論多么安全的，都可能在不安全的方式下使用。

但是，如果被正確地使用，seL4通過(guò)具體的安全理論的支持，給系統(tǒng)架構(gòu)師和用戶提供了強(qiáng)大的機(jī)制來(lái)實(shí)現(xiàn)安全策略。

什么是證明假設(shè)？簡(jiǎn)明的版本是：我們假設(shè)在內(nèi)核的匯編代碼是正確的，硬件表現(xiàn)是正常的，內(nèi)核的硬件管理（TLB和高速緩存）是正確的，啟動(dòng)代碼是正確的。硬件模型假設(shè)DMA將被關(guān)閉或者被信任。安全證明額外給出了一個(gè)系統(tǒng)配置的條件列表。

我該如何充分利用了seL4的形式證明？seL4證明僅僅是在構(gòu)建安全的系統(tǒng)的第一步。它們提供應(yīng)用程序和系統(tǒng)開(kāi)發(fā)人員需要的工具來(lái)提供證據(jù)證明他們的系統(tǒng)是安全的。

例如，可以使用功能的正確性證明來(lái)表明與內(nèi)核的應(yīng)用程序接口是正確的。我們可以使用完整屬性來(lái)證明別人無(wú)法干擾私有數(shù)據(jù)，以及保密的證據(jù)來(lái)證明其他人將無(wú)法訪問(wèn)私有數(shù)據(jù)。可以將所有的整個(gè)（one-machine）系統(tǒng)綁定到一個(gè)證明中，而不需要驗(yàn)證整個(gè)系統(tǒng)的代碼。

有之前未被驗(yàn)證的操作系統(tǒng)的內(nèi)核嗎？操作系統(tǒng)驗(yàn)證至少可以追溯到40年前的20世紀(jì)70年代中期，所以關(guān)于操作系統(tǒng)內(nèi)核的驗(yàn)證有大量的前期工作。還可以看一個(gè)關(guān)于2008年來(lái)的OS驗(yàn)證全面性概述的論文以及2014年來(lái)的seL4概述論文的相關(guān)工作部分。

seL4的新的和令人興奮的事情是，

a）強(qiáng)大的屬性，如功能正確性、完整性、保密性，

b）具有直接針對(duì)代碼的正式驗(yàn)證屬性 – 最開(kāi)始是C，現(xiàn)在可以針對(duì)二進(jìn)制。此外，seL4證明是機(jī)器檢查，不只是基于筆和紙。

之前的驗(yàn)證要么沒(méi)有完成其證明，或只針對(duì)更淺的屬性，如沒(méi)有未定義執(zhí)行，或者它們驗(yàn)證代碼的手動(dòng)構(gòu)造模型而不是代碼本身。先前的驗(yàn)證中有一部分是令人印象深刻的成就，它們奠定了基礎(chǔ)，沒(méi)有這些基礎(chǔ)，seL4證明就不會(huì)被實(shí)現(xiàn)。只是在最近五到十年，代碼驗(yàn)證和定理證明技術(shù)進(jìn)步到足以使大量的代碼級(jí)證明是可行的。

我可以用seL4做什么？你可以將seL4用于研究、教育和商業(yè)。詳情參見(jiàn)標(biāo)準(zhǔn)開(kāi)放源代碼規(guī)定的許可證附帶的代碼。不同的許可證適用于代碼的不同部分，但這些條件都是為了方便代碼的采用。

許可證條件是什么？seL4內(nèi)核是在GPL2許可證下發(fā)布。用戶空間工具和庫(kù)大多是在BSD。

我該如何給seL4做貢獻(xiàn)？簡(jiǎn)單地說(shuō)，seL4是在擁有代碼的合作伙伴之間的復(fù)雜協(xié)議下發(fā)布的。發(fā)布的條件是，我們跟蹤的所有貢獻(xiàn)，并從所有參與者那獲取一個(gè)簽名的協(xié)議許可。

我怎樣才能構(gòu)建seL4系統(tǒng)？與linux操作系統(tǒng)相比，在seL4系統(tǒng)上構(gòu)建一個(gè)系統(tǒng)要求多的多。將你的系統(tǒng)分解為模塊，你需要找出每個(gè)模塊需要訪問(wèn)哪些硬件資源，你需要為你的平臺(tái)構(gòu)建設(shè)備驅(qū)動(dòng)程序（在libplatsupport下有少量為支持的平臺(tái)提供的驅(qū)動(dòng)），你必須把它集成成某物來(lái)運(yùn)行。為了做到這一點(diǎn)，有兩種推薦的方式。

CAmKES是基于微內(nèi)核的嵌入式系統(tǒng)的組件架構(gòu)。它提供了一種語(yǔ)言用于描述組件的資源的分配和組件的地址空間的分配。建立在libsel4utils上，它提供了如進(jìn)程之類的有用的抽象，但一般級(jí)別比較低。此外，新南威爾士大學(xué)的先進(jìn)操作系統(tǒng)課程有一個(gè)擴(kuò)展項(xiàng)目組件來(lái)在seL4之上創(chuàng)建一個(gè)OS。如果你有機(jī)會(huì)得到Sabre Lite開(kāi)發(fā)板，你應(yīng)該能夠自己進(jìn)行項(xiàng)目開(kāi)發(fā)工作來(lái)做為熟悉seL4的一種方式。

哪里可以了解更多信息？從L3到了seL4 – 20年內(nèi)在微內(nèi)核我們學(xué)到了什么？20年L4微內(nèi)核的回顧; https://www.php.cn/link/95ef1128340226d8325ba751bfac05eb

原始的2009論文描述了seL4及其形式化驗(yàn)證;https://www.php.cn/link/4cb4a0aadcf427341c1fe9ae93a5cf31

更長(zhǎng)的論文，詳細(xì)說(shuō)明了seL4的完整驗(yàn)證的故事，其中包括高層次的安全性證明，二進(jìn)制校驗(yàn)和時(shí)間性分析。它還包含驗(yàn)證成本的分析，以及和傳統(tǒng)設(shè)計(jì)系統(tǒng)的比較。https://www.php.cn/link/b61be50f3f8a606a09d3614e09937e3a

本文來(lái)自：https://www.php.cn/link/6b387ebbcb8020ce186644d4a4669c6a 譯者：網(wǎng)絡(luò)整理，有刪改

seL4代碼托管地址: https://www.php.cn/link/3b81467c62f5cdcc01fdebe09a88faa0 seL4項(xiàng)目主頁(yè):https://www.php.cn/link/b32016b92746d5f303795b24402950e5