作者：Paul Pazandak，Fabrizio Bertocci

通用計算、操作系統 （OS）、固有的語言功能（如 C 內存分配）和軟件質量問題導致整個行業的系統缺乏固有的安全性和彈性。這導致了許多安全漏洞，對國家安全產生了可怕的后果。有必要通過應用合理的安全和工程原則，基于適當的技術和工具設計有保證的系統。

一般來說，構建一個有保證的系統需要對問題領域有透徹的了解，對特定于領域的工作流程和要求進行深入分析，仔細的架構考慮和設計權衡，經過審查的開發，正確的配置以及最終產品的托管部署。在整個產品生命周期中也需要這種程度的護理。

具體而言，與系統體系結構相關，利用硬件和軟件技術及工具增強安全性歸結為將合理的安全原則應用于合適的目標，例如內存訪問（例如，開放設計原則、最小特權原則、特權分離原則和完全中介原則）。其他研究和開發工作可能會將這些原則的不同應用應用于其特定環境和設計目標。

構建可信賴和高保證系統的過程是復雜、昂貴的，并且需要大量的專業知識。最終目標是創建一個完整的軟件 - 硬件解決方案，其組件（單獨或集體）滿足客戶對安全和安保所需的保證級別。這將根據所需的標準而有所不同。

例如，用于飛行安全適航性的RTCA DO-178C和用于自動駕駛汽車的ISO 26262都包含與組件的關鍵級別（角色）相對應的多個級別的認證。例如，在DO-178C中，有五個級別：

A級（災難性）：阻止持續安全飛行或降落，許多致命傷害

B級（危險/嚴重）：對少數乘員造成潛在致命傷害

C 級（主要）：影響機組人員的工作效率、不適或可能對乘員造成傷害

D級（次要）：飛機安全裕度降低，但完全在機組人員能力范圍內

E級（無影響）：完全不影響飛機安全

就資金和時間而言，從上到下建立一個高保證的系統的成本太高了。相反，目標應該是開發盡可能少的代碼。人們可以獲取或許可的經過驗證的/可認證代碼越多，設計，開發，維護和認證所需的代碼就越少。這將加快開發工作并顯著降低成本。高確定性軟件堆棧提供了此功能。

此堆棧的作用是提供經過驗證的基礎。它由經過驗證或認證的實時操作系統（RTOS）和分布式通信中間件組成。

高確定性軟件堆棧的基礎

在過去的六年中，在DARPA研究資助下，RTI一直在為嵌入式系統開發經過驗證的堆棧，以加速安全/安保認證。在此堆棧中，我們使用 RTI 的可認證連接軟件框架。RTI 支持對象管理組數據分發服務標準 （OMG DDS）。如今，Connext 正在近 2，000 個關鍵系統中運行，涵蓋航空電子/國防、自主系統、醫療機器人、能源和工業系統。利用OMG DDS開放標準，能夠快速將松散耦合（分布式）的軟件組件組裝到工作系統中。

對于安全實時操作系統，我們選擇了開源 seL4 分離內核（sel4.系統）。它是一個數學上可證明的正確微內核，它將在運行過程之間提供時間和空間分離。它保證進程之間不會出現意外的數據泄漏，并且一個進程不會影響另一個進程的操作。這提供了更高的系統彈性和安全性，這也是多獨立安全級別 （MILS） 解決方案的屬性。

如今，seL4的衍生產品正被幾家大型科技公司使用。

對安全微內核的需求

要了解對像 seL4 這樣的安全微內核的需求，從仔細研究內核設計原則開始是很有幫助的。

如圖 2 所示，有兩種主要的內核設計方法 - 單片內核和微內核。在前者中，提供典型操作系統服務所需的所有代碼都直接在內核本身中實現。內核以硬件的特權模式執行，這意味著所有代碼都被授予對所有系統資源的無限制訪問和控制。

［圖2 |如果設計正確，微內核操作系統（OS）包含的代碼遠遠少于整體架構，從而減少了攻擊面，簡化了合規性等等。

這種類型的實現可能有益于整體系統性能，但如果任何內核組件具有某種類型的故障（攻擊者可以利用這種狀態），則可能導致危險情況。Linux內核提供了一個突出的例子，它包含超過2000萬行代碼，預計包含一定數量的錯誤，提供潛在的攻擊渠道。

相比之下，微內核設計通過大幅減少可信計算庫（TCB）來應對這一缺點，TCB意味著整個系統中必須可信才能正常運行的代碼子集。微內核遵循內核僅包含最基本機制（例如，進程間通信和調度）的設計原則。所有剩余的操作系統功能必須轉移到非特權用戶模式，從而在隔離的沙箱中封裝運行。

這種方法可以保護內核進程免受來自外部的任何干擾，只允許明確需要的通信。對于像 seL4 這樣設計良好的微內核，這意味著代碼庫可以減少到一萬行代碼的數量級。這大大縮小了攻擊面。

seL4 和 DDS：可靠的組合

seL4 的目的是為需要它的應用程序提供可靠、安全和可靠的基礎。例如，這包括軍事系統、醫療設備、機器人、自動駕駛汽車和能源系統。無一例外，這些高保證的應用程序需要可靠和強大的分布式通信功能，這是 seL4 無法提供的。

OMG DDS用于實時系統是一個實時，安全，松散耦合，發布/訂閱軟件連接框架，適用于分布式系統，非常適合作為高保證系統的通信層，包括任何安全RTOS，如seL4。雖然還有其他開源和商業現成的通信框架技術，但這些框架缺乏高保證認證，充其量只能提供基本的全有或全無的安全性。

對于DDS，seL4創建了一個豐富，低成本，更小的占地面積，高保證的基礎。對于 seL4，DDS 提供了一個基于開放標準的通信協議。

DDS 大大簡化了 seL4 組件間/應用程序開發，降低了相關成本，并促進了 seL4 開發社區中的組件互操作性。DDS 是一種解決方案，它將以更一致、更安全、更高效的方式標準化數據分發。它提供了一個發布-訂閱模型，使分布式系統開發更簡單、更快速、更安全。應用程序開發人員可以減輕創建自己的零碎的，也許是專有的，一次性解決方案的負擔，用于基于消息的通信和破譯消息序列，使他們能夠專注于特定于域的組件，并依靠DDS提供與系統中其他（本地和遠程）實體的標準化，安全的交互。

降低高保障軟件的進入壁壘

DDS 將顯著降低決定使用 seL4/CAmkES 的公司和開發人員的進入門檻，因為它提供了一個抽象層，隱藏了與在 seL4 之上開發應用程序相關的大部分復雜性。DDS將大大減少內部開發時間和對seL4主題專業知識的需求。

審核編輯：郭婷