為了滿足先進工業(yè)制造和裝備控制智能化的需求,嵌入式系統(tǒng)已成為關鍵基礎設施的核心控制組件,并在工業(yè)制造、船舶、交通、國防安全、信息通信等領域起著影響全局系統(tǒng)安全的重要作用。近年來,隨著嵌入式應用的廣泛普及,以及網(wǎng)絡化、智能化的發(fā)展趨勢,系統(tǒng)運行的可靠性和敏感數(shù)據(jù)的安全性成為了嵌入式領域亟待解決的關鍵問題。倘若嵌入式軟件系統(tǒng)失效或遭受安全入侵,則可能產(chǎn)生危及到國家政治、經(jīng)濟以及軍事安全的重大事故。因此,如何針對此類安全關鍵的應用場景,設計和開發(fā)一種功能正確、滿足所需安全（Security）和防危（Safety）屬性,并能對所宣稱的正確性提供確鑿可信證據(jù)的嵌入式系統(tǒng),成為了一個重要的研究課題。針對上述問題,本文全面分析并總結了高可信嵌入式應用對于系統(tǒng)軟件的安全要求,提出滿足安全隔離和形式化驗證的軟件體系架構。并針對系統(tǒng)軟件中,硬件機制建模、可中斷代碼驗證、不可信組件的安全訪問控制以及基于虛擬化的隔離保護等關鍵問題,分別提出了相應的解決方法。最終,形成了一套可組合、可伸縮的高可信嵌入式系統(tǒng)基礎軟件開發(fā)和形式化驗證框架與工具鏈,并實現(xiàn)了原型系統(tǒng)的開發(fā)和實驗評估。結果表明,通過采用隔離、硬件保護機... 

【文章來源】：電子科技大學四川省 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：184 頁

【學位級別】：博士

【部分圖文】：

命令填充及不同類型命令解釋時延

第四章 非安全關鍵驅動的安全運行環(huán)境4.7.2 命令解釋吞吐量實驗比較內核態(tài) AHCI 驅動與相同功能的用戶態(tài)驅動在被連續(xù)調用模塊中磁盤讀寫函數(shù)時，單位時間內可以訪問磁盤的數(shù)據(jù)量。為了消除由于進程搶占所導致的抖動，測試時終止除測試進程和 idle 以外的其他進程，并對于用戶態(tài)驅動而言，測試被代碼直接運行于 AHCI 驅動進程中。實驗結果如圖 4-16 所示，其中橫軸表示每次磁盤訪問（即發(fā)送 FrameInformationStructure，F(xiàn)IS）時 DMA 的數(shù)據(jù)塊大小，單位為 KB，縱軸為每秒可以讀取或寫入的數(shù)據(jù)量。隨著單次 DMA 數(shù)據(jù)塊大小的增加，磁盤訪問效率提升，吞吐量也隨之提升，但用戶態(tài)驅動與內核態(tài)驅動在 DMA 數(shù)據(jù)塊大小相同時，吞吐量非常接近。其原因在于用戶態(tài)執(zhí)行驅動程序并沒有成為磁盤讀寫的性能瓶頸。

圖 4-17 用戶態(tài)與內核態(tài)串口數(shù)據(jù)發(fā)送時延4.7.4 綜合吞吐量實驗測量在綜合環(huán)境下，框架對驅動吞吐量產(chǎn)生的影響。實驗由兩臺計算機組成，輔助機向實驗機串口中盡可能多地輸出數(shù)據(jù)，通過測量實驗驗機內核態(tài)與用戶態(tài)串口驅動每秒最大可接收的字符數(shù)，獲得框架對驅動吞吐量帶來的影響。實驗結果如圖 4-18 所示，試驗中串口運行在波特率為 115200，數(shù)據(jù)位 8，停止位 1，無奇偶校驗的狀態(tài)下，理論最大吞吐量應為 12800char/s（即圖中 baseline 一項）。由于串口控制器、中斷響應與系統(tǒng)調用等額外負載，內核態(tài)驅動最大吞吐量為理論值的 89%，而用戶態(tài)驅動的吞吐量與內核態(tài)相差 1%左右。

【參考文獻】：
期刊論文
[1]嵌入式系統(tǒng)安全綜述[J]. 趙波,倪明濤,石源,樊佩茹.  武漢大學學報(理學版). 2018(02)
[2]未來網(wǎng)絡與工業(yè)互聯(lián)網(wǎng)發(fā)展綜述[J]. 吳文君,姚海鵬,黃韜,王露瑤,張延華,劉韻潔.  北京工業(yè)大學學報. 2017(02)
[3]基于可信計算基的主機可信安全體系結構研究[J]. 黃強,常樂,張德華,汪倫偉.  信息網(wǎng)絡安全. 2016(07)
[4]關鍵基礎設施信息安全分析及防護[J]. 劉松,朱錢祥,陳開放.  智慧工廠. 2016(03)
[5]嵌入式操作系統(tǒng)的形式化驗證研究[J]. 陳麗蓉,李允,羅蕾.  計算機科學. 2015(08)
[6]設備驅動程序可靠性和正確性保障方法與技術研究進展[J]. 張一帆,黃超,歐建生,湯恩義,陳鑫.  軟件學報. 2015(02)
[7]微內核中斷機制的形式化設計與驗證[J]. 李康杰,錢振江,黃皓.  計算機科學. 2013(03)
[8]操作系統(tǒng)對象語義模型（OSOSM）及形式化驗證[J]. 錢振江,劉葦,黃皓.  計算機研究與發(fā)展. 2012(12)
[9]網(wǎng)卡驅動程序的用戶態(tài)移植和優(yōu)化[J]. 王燕飛,華蓓.  電子技術. 2012(08)
[10]用戶態(tài)驅動框架的研究與實現(xiàn)[J]. 劉軍衛(wèi),李曦,陳香蘭,徐軍.  計算機系統(tǒng)應用. 2011(11)

博士論文
[1]安全操作系統(tǒng)形式化設計與驗證方法研究[D]. 錢振江.南京大學 2013
[2]面向目標代碼的實時操作系統(tǒng)形式化驗證方法研究[D]. 史建琦.華東師范大學 2012
[3]高可信嵌入式操作系統(tǒng)體系架構研究[D]. 楊霞.電子科技大學 2010
[4]基于模型檢測的安全操作系統(tǒng)驗證方法研究[D]. 程亮.中國科學技術大學 2009

碩士論文
[1]基于AUTOSAR的汽車電子操作系統(tǒng)及其應用的建模與分析[D]. 彭云輝.華東師范大學 2014



本文編號：2969767