形式化驗證在安全操作系統的發展中成為了熱門話題！sel4在其官方網站上宣稱：安全絕不應成為表現不佳的借口！

seL4是什么？seL4是L4微內核家族中最先進的成員，以其全面的形式驗證而著稱，這使其與其他操作系統截然不同。seL4在實現這一目標的同時，性能并未受損。

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

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

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

需要注意的是，L4HQ記錄的IPC時間是經過微優化的結果，這些優化尚未包含在公開版本中。發布的內核大約慢了10-20%的速度（這仍然使其比我們已知的其他性能數據快）。我們計劃一旦這些優化成熟，就推動其應用。

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

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

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

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

為了支持虛擬機，seL4本身作為一個虛擬機管理程序運行（x86 Ring-0根模式或ARM hyp模式）并轉發虛擬化事件到虛擬機監視器（VMM），VMM執行必要的仿真。VMM運行在脫特權模式（x86 Ring-3根模式或ARM supv模式）。

seL4支持多核嗎？在x86上，seL4可以配置為支持多個CPU。目前多核的支持是通過一個多核配置實現，每個啟動CPU被分配一部分可用內存。然后，內核可以通過受限的共享內存和內核支持的IPI通信。

我可以在沒有MMU的微控制器上運行seL4嗎？在沒有完整的存儲器管理單元（MMU）上使用seL4沒有意義，因為它的資源管理基本上是基于虛擬內存的。對于只有一個內存保護單元（MPU）或完全沒有內存保護的低端處理器，你應該看看NICTA的eChronos實時操作系統（RTOS），這是專為這樣的處理器設計的，也經過形式化驗證。

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

什么是形式驗證？形式軟件驗證是用數學證明來說明一款軟件滿足特定屬性。傳統上，形式驗證已被廣泛用于說明設計或一個軟件的規范都有一定的屬性，或者一個設計正確地實現了一個規范。在最近幾年，已經可能直接應用形式驗證到實現該軟件的代碼上，并表明該代碼具有特定的性質。形式驗證有兩種方式：完全自動化的方法，如有限的系統和屬性的模型檢驗工作，以及交互的數學證明，需要手動操作。seL4驗證使用了Isabelle/HOL定理證明的形式數學證明。該定理證明是交互的，但提供的自動化程度較高。它也提供了高度的保證來確保所產生的證明是正確的。

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

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

因此，問題的答案取決于你對錯誤的理解。在形式軟件驗證（代碼實現規范）的理解中，答案是肯定的。在一般的軟件用戶的理解中，答案是有可能的，因為還有可能是硬件錯誤或未得到滿足的證明假設。對于高保障系統來說，這不是一個問題，因為硬件的分析和證明的假設比分析具備相同的硬件，和測試假設的大型軟件系統容易的多。

seL4證明是安全嗎？這取決于你所說安全的意思。在傳統的操作系統的安全性的解釋，答案是肯定的。特別是，seL4已被證明強制執行特定的安全性能，即在一定條件下的完整性和保密性。這些證明都是關于seL4的程序用于構建安全系統的非常有力的證據。一些證據的假設可能有限制條件，例如DMA的使用被排除在外，或僅允許由正式由用戶進行驗證的受信任驅動程序。雖然這些限制對高保障系統是常見的，我們正在努力地以減少它們，例如通過在x86上使用IOMMU或在ARM上使用System MMU。

如果我運行了seL4，我的系統就是安全嗎？這并不是自動保證的。安全是一個跨越整個系統，包括與人交互那一部分的問題。OS內核，無論驗證與否，并不會自動使系統安全。事實上，任何系統，無論多么安全的，都可能在不安全的方式下使用。

但是，如果被正確地使用，seL4通過具體的安全理論的支持，給系統架構師和用戶提供了強大的機制來實現安全策略。

什么是證明假設？簡明的版本是：我們假設在內核的匯編代碼是正確的，硬件表現是正常的，內核的硬件管理（TLB和高速緩存）是正確的，啟動代碼是正確的。硬件模型假設DMA將被關閉或者被信任。安全證明額外給出了一個系統配置的條件列表。

我該如何充分利用了seL4的形式證明？seL4證明僅僅是在構建安全的系統的第一步。它們提供應用程序和系統開發人員需要的工具來提供證據證明他們的系統是安全的。

例如，可以使用功能的正確性證明來表明與內核的應用程序接口是正確的。我們可以使用完整屬性來證明別人無法干擾私有數據，以及保密的證據來證明其他人將無法訪問私有數據。可以將所有的整個（one-machine）系統綁定到一個證明中，而不需要驗證整個系統的代碼。

有之前未被驗證的操作系統的內核嗎？操作系統驗證至少可以追溯到40年前的20世紀70年代中期，所以關于操作系統內核的驗證有大量的前期工作。還可以看一個關于2008年來的OS驗證全面性概述的論文以及2014年來的seL4概述論文的相關工作部分。

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

a）強大的屬性，如功能正確性、完整性、保密性，

b）具有直接針對代碼的正式驗證屬性 – 最開始是C，現在可以針對二進制。此外，seL4證明是機器檢查，不只是基于筆和紙。

之前的驗證要么沒有完成其證明，或只針對更淺的屬性，如沒有未定義執行，或者它們驗證代碼的手動構造模型而不是代碼本身。先前的驗證中有一部分是令人印象深刻的成就，它們奠定了基礎，沒有這些基礎，seL4證明就不會被實現。只是在最近五到十年，代碼驗證和定理證明技術進步到足以使大量的代碼級證明是可行的。

我可以用seL4做什么？你可以將seL4用于研究、教育和商業。詳情參見標準開放源代碼規定的許可證附帶的代碼。不同的許可證適用于代碼的不同部分，但這些條件都是為了方便代碼的采用。

許可證條件是什么？seL4內核是在GPL2許可證下發布。用戶空間工具和庫大多是在BSD。

我該如何給seL4做貢獻？簡單地說，seL4是在擁有代碼的合作伙伴之間的復雜協議下發布的。發布的條件是，我們跟蹤的所有貢獻，并從所有參與者那獲取一個簽名的協議許可。

我怎樣才能構建seL4系統？與linux操作系統相比，在seL4系統上構建一個系統要求多的多。將你的系統分解為模塊，你需要找出每個模塊需要訪問哪些硬件資源，你需要為你的平臺構建設備驅動程序（在libplatsupport下有少量為支持的平臺提供的驅動），你必須把它集成成某物來運行。為了做到這一點，有兩種推薦的方式。

CAmKES是基于微內核的嵌入式系統的組件架構。它提供了一種語言用于描述組件的資源的分配和組件的地址空間的分配。建立在libsel4utils上，它提供了如進程之類的有用的抽象，但一般級別比較低。此外，新南威爾士大學的先進操作系統課程有一個擴展項目組件來在seL4之上創建一個OS。如果你有機會得到Sabre Lite開發板，你應該能夠自己進行項目開發工作來做為熟悉seL4的一種方式。

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

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

更長的論文，詳細說明了seL4的完整驗證的故事，其中包括高層次的安全性證明，二進制校驗和時間性分析。它還包含驗證成本的分析，以及和傳統設計系統的比較。https://www.php.cn/link/b61be50f3f8a606a09d3614e09937e3a

本文來自：https://www.php.cn/link/6b387ebbcb8020ce186644d4a4669c6a 譯者：網絡整理，有刪改

seL4代碼托管地址: https://www.php.cn/link/3b81467c62f5cdcc01fdebe09a88faa0 seL4項目主頁:https://www.php.cn/link/b32016b92746d5f303795b24402950e5