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

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

一般來(lái)說(shuō)，構(gòu)建一個(gè)有保證的系統(tǒng)需要對(duì)問(wèn)題領(lǐng)域有透徹的了解，對(duì)特定于領(lǐng)域的工作流程和要求進(jìn)行深入分析，仔細(xì)的架構(gòu)考慮和設(shè)計(jì)權(quán)衡，經(jīng)過(guò)審查的開(kāi)發(fā)，正確的配置以及最終產(chǎn)品的托管部署。在整個(gè)產(chǎn)品生命周期中也需要這種程度的護(hù)理。

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

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

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

A級(jí)（災(zāi)難性）：阻止持續(xù)安全飛行或降落，許多致命傷害

B級(jí)（危險(xiǎn)/嚴(yán)重）：對(duì)少數(shù)乘員造成潛在致命傷害

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

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

E級(jí)（無(wú)影響）：完全不影響飛機(jī)安全

就資金和時(shí)間而言，從上到下建立一個(gè)高保證的系統(tǒng)的成本太高了。相反，目標(biāo)應(yīng)該是開(kāi)發(fā)盡可能少的代碼。人們可以獲取或許可的經(jīng)過(guò)驗(yàn)證的/可認(rèn)證代碼越多，設(shè)計(jì)，開(kāi)發(fā)，維護(hù)和認(rèn)證所需的代碼就越少。這將加快開(kāi)發(fā)工作并顯著降低成本。高確定性軟件堆棧提供了此功能。

此堆棧的作用是提供經(jīng)過(guò)驗(yàn)證的基礎(chǔ)。它由經(jīng)過(guò)驗(yàn)證或認(rèn)證的實(shí)時(shí)操作系統(tǒng)（RTOS）和分布式通信中間件組成。

高確定性軟件堆棧的基礎(chǔ)

在過(guò)去的六年中，在DARPA研究資助下，RTI一直在為嵌入式系統(tǒng)開(kāi)發(fā)經(jīng)過(guò)驗(yàn)證的堆棧，以加速安全/安保認(rèn)證。在此堆棧中，我們使用 RTI 的可認(rèn)證連接軟件框架。RTI 支持對(duì)象管理組數(shù)據(jù)分發(fā)服務(wù)標(biāo)準(zhǔn) （OMG DDS）。如今，Connext 正在近 2，000 個(gè)關(guān)鍵系統(tǒng)中運(yùn)行，涵蓋航空電子/國(guó)防、自主系統(tǒng)、醫(yī)療機(jī)器人、能源和工業(yè)系統(tǒng)。利用OMG DDS開(kāi)放標(biāo)準(zhǔn)，能夠快速將松散耦合（分布式）的軟件組件組裝到工作系統(tǒng)中。

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

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

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

要了解對(duì)像 seL4 這樣的安全微內(nèi)核的需求，從仔細(xì)研究?jī)?nèi)核設(shè)計(jì)原則開(kāi)始是很有幫助的。

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

［圖2 |如果設(shè)計(jì)正確，微內(nèi)核操作系統(tǒng)（OS）包含的代碼遠(yuǎn)遠(yuǎn)少于整體架構(gòu)，從而減少了攻擊面，簡(jiǎn)化了合規(guī)性等等。

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

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

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

seL4 和 DDS：可靠的組合

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

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

對(duì)于DDS，seL4創(chuàng)建了一個(gè)豐富，低成本，更小的占地面積，高保證的基礎(chǔ)。對(duì)于 seL4，DDS 提供了一個(gè)基于開(kāi)放標(biāo)準(zhǔn)的通信協(xié)議。

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

降低高保障軟件的進(jìn)入壁壘

DDS 將顯著降低決定使用 seL4/CAmkES 的公司和開(kāi)發(fā)人員的進(jìn)入門(mén)檻，因?yàn)樗峁┝艘粋€(gè)抽象層，隱藏了與在 seL4 之上開(kāi)發(fā)應(yīng)用程序相關(guān)的大部分復(fù)雜性。DDS將大大減少內(nèi)部開(kāi)發(fā)時(shí)間和對(duì)seL4主題專業(yè)知識(shí)的需求。

審核編輯：郭婷