作者：Paul Pazandak，F(xiàn)abrizio Bertocci

通用計算、操作系統(tǒng) （OS）、固有語言功能（如 C 內(nèi)存分配）和軟件質(zhì)量問題導(dǎo)致整個行業(yè)的系統(tǒng)缺乏固有的安全性和彈性。這導(dǎo)致了許多安全漏洞，對國家安全造成了可怕的后果。有必要通過應(yīng)用健全的安全和工程原則，根據(jù)適當(dāng)?shù)募夹g(shù)和工具設(shè)計有保證的系統(tǒng)。

一般來說，構(gòu)建有保證的系統(tǒng)需要對問題域有透徹的了解，深入分析特定于域的工作流和要求，仔細的架構(gòu)考慮和設(shè)計權(quán)衡，審查開發(fā)，正確配置和最終產(chǎn)品的托管部署。在整個產(chǎn)品生命周期中也需要這種級別的護理。

具體而言，與系統(tǒng)架構(gòu)相關(guān)，利用硬件和軟件技術(shù)和工具增強安全性歸結(jié)為將合理的安全原則應(yīng)用于合適的目標(biāo)，例如內(nèi)存訪問（例如，開放設(shè)計、最小特權(quán)、特權(quán)分離和完全中介原則）。其他研究和開發(fā)工作可能會將這些原則應(yīng)用于其特定的環(huán)境和設(shè)計目標(biāo)。

構(gòu)建可信賴和高保證系統(tǒng)的過程復(fù)雜、昂貴，并且需要大量專業(yè)知識。最終目標(biāo)是創(chuàng)建一個完整的軟件-硬件解決方案，其組件（單獨和集體）滿足客戶所需的安全和安保保證級別。這將因所需的標(biāo)準(zhǔn)而異。

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

A級（災(zāi)難性）：防止持續(xù)安全飛行或著陸，許多致命傷害

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

C級（主要）：損害乘員效率、不適或可能對乘員造成傷害

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

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

從上到下建立一個高保證系統(tǒng)在資金和時間方面都太昂貴了。相反，目標(biāo)應(yīng)該是開發(fā)盡可能少的代碼。人們可以獲得或許可的經(jīng)過驗證/可認證的代碼越多，設(shè)計、開發(fā)、維護和認證所需的代碼就越少。這將加快開發(fā)工作并大大降低成本。高保證軟件堆棧提供了這一點。

此堆棧的作用是提供一個經(jīng)過驗證的基礎(chǔ)。它由經(jīng)過驗證或認證的實時操作系統(tǒng)（RTOS）（安全RTOS）和分布式通信中間件組成。

高保證軟件堆棧的基礎(chǔ)

在過去的六年里，在DARPA的研究資助下，RTI一直致力于嵌入式系統(tǒng)的經(jīng)過驗證的堆棧，以加速安全/安保認證。在這個堆棧中，我們使用RTI的可認證Connext軟件框架。RTI Connext 支持對象管理組數(shù)據(jù)分發(fā)服務(wù)標(biāo)準(zhǔn) （OMG DDS）。Connext目前在近2，000個關(guān)鍵系統(tǒng)中運行，涵蓋航空電子/國防，自主系統(tǒng)，醫(yī)療機器人，能源和工業(yè)系統(tǒng)。利用OMG DDS開放標(biāo)準(zhǔn)，能夠?qū)⑺缮?a href="http://www.brongaenegriffin.com/tags/耦合/" target="_blank">耦合（分布式）的軟件組件快速組裝到工作系統(tǒng)中。

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

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

對安全微內(nèi)核的需求

要了解對像seL4這樣的安全微內(nèi)核的需求，首先仔細研究內(nèi)核設(shè)計原則是有幫助的。

如圖 2 所示，有兩種主要的內(nèi)核設(shè)計方法 – 單片內(nèi)核和微內(nèi)核。在前者中，提供典型操作系統(tǒng)服務(wù)所需的所有代碼都直接在內(nèi)核本身中實現(xiàn)。內(nèi)核以硬件的特權(quán)模式執(zhí)行，這意味著所有代碼都被授予對所有系統(tǒng)資源的無限制訪問和控制。

［圖2 |如果設(shè)計得當(dāng)，微內(nèi)核操作系統(tǒng) （OS） 包含的代碼比單片架構(gòu)少得多，從而減少了攻擊面、簡化了合規(guī)性等。

這種類型的實現(xiàn)可能對整體系統(tǒng)性能有益，但如果任何內(nèi)核組件具有某種類型的故障（攻擊者可以利用這種狀態(tài)），則可能導(dǎo)致危險情況。一個突出的例子是Linux內(nèi)核，它包含超過2000萬行代碼，可以預(yù)期包含一定數(shù)量的錯誤，提供潛在的攻擊渠道。

相比之下，微內(nèi)核設(shè)計通過大幅減少可信計算基礎(chǔ)（TCB）來應(yīng)對這一缺點，這意味著整個系統(tǒng)中必須信任的代碼子集才能正常運行。微內(nèi)核遵循的設(shè)計原則是讓內(nèi)核僅包含最基本的機制（例如，進程間通信和調(diào)度）。所有剩余的操作系統(tǒng)功能必須轉(zhuǎn)移到非特權(quán)用戶模式，從而在隔離的沙箱中封裝運行。

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

seL4 和 DDS：可靠的組合

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

OMG DDS for Real-Time Systems是一個實時、安全、松散耦合的分布式系統(tǒng)發(fā)布/訂閱軟件連接框架，非常適合作為高保證系統(tǒng)的通信層，包括任何安全RTOS，如seL4。雖然還有其他開源和商業(yè)現(xiàn)成的通信框架技術(shù)，但這些框架缺乏高保證認證，充其量只能提供基本的全有或全無安全性。

對于 DDS，seL4 創(chuàng)造了一個豐富、成本更低、占用空間更小、高保證的基礎(chǔ)。對于seL4，DDS提供了一個基于開放標(biāo)準(zhǔn)的通信協(xié)議。

DDS 極大地簡化了 seL4 組件間/應(yīng)用程序開發(fā)，降低了相關(guān)成本，并促進了 seL4 開發(fā)社區(qū)中的組件互操作性。DDS 是一種解決方案，它將以更一致、安全和高效的方式標(biāo)準(zhǔn)化數(shù)據(jù)分發(fā)。它提供了一個發(fā)布-訂閱模型，可實現(xiàn)更輕松、更快速、更安全的分布式系統(tǒng)開發(fā)。應(yīng)用程序開發(fā)人員可以減輕為基于消息的通信和解密消息序列創(chuàng)建自己的零碎（可能是專有的）一次性解決方案的負擔(dān)，使他們能夠?qū)Ｗ⒂谔囟ㄓ谟虻慕M件，并依靠DDS與系統(tǒng)中的其他（本地和遠程）實體提供標(biāo)準(zhǔn)化的安全交互。

降低高保證軟件的進入門檻

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

審核編輯：郭婷