高可信嵌入式系統(tǒng)軟件的關(guān)鍵技術(shù)研究
發(fā)布時(shí)間：2021-01-11 01:07
為了滿足先進(jìn)工業(yè)制造和裝備控制智能化的需求,嵌入式系統(tǒng)已成為關(guān)鍵基礎(chǔ)設(shè)施的核心控制組件,并在工業(yè)制造、船舶、交通、國防安全、信息通信等領(lǐng)域起著影響全局系統(tǒng)安全的重要作用。近年來,隨著嵌入式應(yīng)用的廣泛普及,以及網(wǎng)絡(luò)化、智能化的發(fā)展趨勢,系統(tǒng)運(yùn)行的可靠性和敏感數(shù)據(jù)的安全性成為了嵌入式領(lǐng)域亟待解決的關(guān)鍵問題。倘若嵌入式軟件系統(tǒng)失效或遭受安全入侵,則可能產(chǎn)生危及到國家政治、經(jīng)濟(jì)以及軍事安全的重大事故。因此,如何針對此類安全關(guān)鍵的應(yīng)用場景,設(shè)計(jì)和開發(fā)一種功能正確、滿足所需安全（Security）和防危（Safety）屬性,并能對所宣稱的正確性提供確鑿可信證據(jù)的嵌入式系統(tǒng),成為了一個(gè)重要的研究課題。針對上述問題,本文全面分析并總結(jié)了高可信嵌入式應(yīng)用對于系統(tǒng)軟件的安全要求,提出滿足安全隔離和形式化驗(yàn)證的軟件體系架構(gòu)。并針對系統(tǒng)軟件中,硬件機(jī)制建模、可中斷代碼驗(yàn)證、不可信組件的安全訪問控制以及基于虛擬化的隔離保護(hù)等關(guān)鍵問題,分別提出了相應(yīng)的解決方法。最終,形成了一套可組合、可伸縮的高可信嵌入式系統(tǒng)基礎(chǔ)軟件開發(fā)和形式化驗(yàn)證框架與工具鏈,并實(shí)現(xiàn)了原型系統(tǒng)的開發(fā)和實(shí)驗(yàn)評估。結(jié)果表明,通過采用隔離、硬件保護(hù)機(jī)...
【文章來源】：電子科技大學(xué)四川省 211工程院校 985工程院校 教育部直屬院校
【文章頁數(shù)】：184 頁
【學(xué)位級別】：博士
【部分圖文】：
命令填充及不同類型命令解釋時(shí)延
第四章 非安全關(guān)鍵驅(qū)動的安全運(yùn)行環(huán)境4.7.2 命令解釋吞吐量實(shí)驗(yàn)比較內(nèi)核態(tài) AHCI 驅(qū)動與相同功能的用戶態(tài)驅(qū)動在被連續(xù)調(diào)用模塊中磁盤讀寫函數(shù)時(shí)，單位時(shí)間內(nèi)可以訪問磁盤的數(shù)據(jù)量。為了消除由于進(jìn)程搶占所導(dǎo)致的抖動，測試時(shí)終止除測試進(jìn)程和 idle 以外的其他進(jìn)程，并對于用戶態(tài)驅(qū)動而言，測試被代碼直接運(yùn)行于 AHCI 驅(qū)動進(jìn)程中。實(shí)驗(yàn)結(jié)果如圖 4-16 所示，其中橫軸表示每次磁盤訪問（即發(fā)送 FrameInformationStructure，F(xiàn)IS）時(shí) DMA 的數(shù)據(jù)塊大小，單位為 KB，縱軸為每秒可以讀取或?qū)懭氲臄?shù)據(jù)量。隨著單次 DMA 數(shù)據(jù)塊大小的增加，磁盤訪問效率提升，吞吐量也隨之提升，但用戶態(tài)驅(qū)動與內(nèi)核態(tài)驅(qū)動在 DMA 數(shù)據(jù)塊大小相同時(shí)，吞吐量非常接近。其原因在于用戶態(tài)執(zhí)行驅(qū)動程序并沒有成為磁盤讀寫的性能瓶頸。
圖 4-17 用戶態(tài)與內(nèi)核態(tài)串口數(shù)據(jù)發(fā)送時(shí)延4.7.4 綜合吞吐量實(shí)驗(yàn)測量在綜合環(huán)境下，框架對驅(qū)動吞吐量產(chǎn)生的影響。實(shí)驗(yàn)由兩臺計(jì)算機(jī)組成，輔助機(jī)向?qū)嶒?yàn)機(jī)串口中盡可能多地輸出數(shù)據(jù)，通過測量實(shí)驗(yàn)驗(yàn)機(jī)內(nèi)核態(tài)與用戶態(tài)串口驅(qū)動每秒最大可接收的字符數(shù)，獲得框架對驅(qū)動吞吐量帶來的影響。實(shí)驗(yàn)結(jié)果如圖 4-18 所示，試驗(yàn)中串口運(yùn)行在波特率為 115200，數(shù)據(jù)位 8，停止位 1，無奇偶校驗(yàn)的狀態(tài)下，理論最大吞吐量應(yīng)為 12800char/s（即圖中 baseline 一項(xiàng)）。由于串口控制器、中斷響應(yīng)與系統(tǒng)調(diào)用等額外負(fù)載，內(nèi)核態(tài)驅(qū)動最大吞吐量為理論值的 89%，而用戶態(tài)驅(qū)動的吞吐量與內(nèi)核態(tài)相差 1%左右。
【參考文獻(xiàn)】：
期刊論文
[1]嵌入式系統(tǒng)安全綜述[J]. 趙波,倪明濤,石源,樊佩茹. 武漢大學(xué)學(xué)報(bào)(理學(xué)版). 2018(02)
[2]未來網(wǎng)絡(luò)與工業(yè)互聯(lián)網(wǎng)發(fā)展綜述[J]. 吳文君,姚海鵬,黃韜,王露瑤,張延華,劉韻潔. 北京工業(yè)大學(xué)學(xué)報(bào). 2017(02)
[3]基于可信計(jì)算基的主機(jī)可信安全體系結(jié)構(gòu)研究[J]. 黃強(qiáng),常樂,張德華,汪倫偉. 信息網(wǎng)絡(luò)安全. 2016(07)
[4]關(guān)鍵基礎(chǔ)設(shè)施信息安全分析及防護(hù)[J]. 劉松,朱錢祥,陳開放. 智慧工廠. 2016(03)
[5]嵌入式操作系統(tǒng)的形式化驗(yàn)證研究[J]. 陳麗蓉,李允,羅蕾. 計(jì)算機(jī)科學(xué). 2015(08)
[6]設(shè)備驅(qū)動程序可靠性和正確性保障方法與技術(shù)研究進(jìn)展[J]. 張一帆,黃超,歐建生,湯恩義,陳鑫. 軟件學(xué)報(bào). 2015(02)
[7]微內(nèi)核中斷機(jī)制的形式化設(shè)計(jì)與驗(yàn)證[J]. 李康杰,錢振江,黃皓. 計(jì)算機(jī)科學(xué). 2013(03)
[8]操作系統(tǒng)對象語義模型（OSOSM）及形式化驗(yàn)證[J]. 錢振江,劉葦,黃皓. 計(jì)算機(jī)研究與發(fā)展. 2012(12)
[9]網(wǎng)卡驅(qū)動程序的用戶態(tài)移植和優(yōu)化[J]. 王燕飛,華蓓. 電子技術(shù). 2012(08)
[10]用戶態(tài)驅(qū)動框架的研究與實(shí)現(xiàn)[J]. 劉軍衛(wèi),李曦,陳香蘭,徐軍. 計(jì)算機(jī)系統(tǒng)應(yīng)用. 2011(11)
博士論文
[1]安全操作系統(tǒng)形式化設(shè)計(jì)與驗(yàn)證方法研究[D]. 錢振江.南京大學(xué) 2013
[2]面向目標(biāo)代碼的實(shí)時(shí)操作系統(tǒng)形式化驗(yàn)證方法研究[D]. 史建琦.華東師范大學(xué) 2012
[3]高可信嵌入式操作系統(tǒng)體系架構(gòu)研究[D]. 楊霞.電子科技大學(xué) 2010
[4]基于模型檢測的安全操作系統(tǒng)驗(yàn)證方法研究[D]. 程亮.中國科學(xué)技術(shù)大學(xué) 2009
碩士論文
[1]基于AUTOSAR的汽車電子操作系統(tǒng)及其應(yīng)用的建模與分析[D]. 彭云輝.華東師范大學(xué) 2014
本文編號：2969767
【文章來源】：電子科技大學(xué)四川省 211工程院校 985工程院校 教育部直屬院校
【文章頁數(shù)】：184 頁
【學(xué)位級別】：博士
【部分圖文】：
命令填充及不同類型命令解釋時(shí)延
第四章 非安全關(guān)鍵驅(qū)動的安全運(yùn)行環(huán)境4.7.2 命令解釋吞吐量實(shí)驗(yàn)比較內(nèi)核態(tài) AHCI 驅(qū)動與相同功能的用戶態(tài)驅(qū)動在被連續(xù)調(diào)用模塊中磁盤讀寫函數(shù)時(shí)，單位時(shí)間內(nèi)可以訪問磁盤的數(shù)據(jù)量。為了消除由于進(jìn)程搶占所導(dǎo)致的抖動，測試時(shí)終止除測試進(jìn)程和 idle 以外的其他進(jìn)程，并對于用戶態(tài)驅(qū)動而言，測試被代碼直接運(yùn)行于 AHCI 驅(qū)動進(jìn)程中。實(shí)驗(yàn)結(jié)果如圖 4-16 所示，其中橫軸表示每次磁盤訪問（即發(fā)送 FrameInformationStructure，F(xiàn)IS）時(shí) DMA 的數(shù)據(jù)塊大小，單位為 KB，縱軸為每秒可以讀取或?qū)懭氲臄?shù)據(jù)量。隨著單次 DMA 數(shù)據(jù)塊大小的增加，磁盤訪問效率提升，吞吐量也隨之提升，但用戶態(tài)驅(qū)動與內(nèi)核態(tài)驅(qū)動在 DMA 數(shù)據(jù)塊大小相同時(shí)，吞吐量非常接近。其原因在于用戶態(tài)執(zhí)行驅(qū)動程序并沒有成為磁盤讀寫的性能瓶頸。
圖 4-17 用戶態(tài)與內(nèi)核態(tài)串口數(shù)據(jù)發(fā)送時(shí)延4.7.4 綜合吞吐量實(shí)驗(yàn)測量在綜合環(huán)境下，框架對驅(qū)動吞吐量產(chǎn)生的影響。實(shí)驗(yàn)由兩臺計(jì)算機(jī)組成，輔助機(jī)向?qū)嶒?yàn)機(jī)串口中盡可能多地輸出數(shù)據(jù)，通過測量實(shí)驗(yàn)驗(yàn)機(jī)內(nèi)核態(tài)與用戶態(tài)串口驅(qū)動每秒最大可接收的字符數(shù)，獲得框架對驅(qū)動吞吐量帶來的影響。實(shí)驗(yàn)結(jié)果如圖 4-18 所示，試驗(yàn)中串口運(yùn)行在波特率為 115200，數(shù)據(jù)位 8，停止位 1，無奇偶校驗(yàn)的狀態(tài)下，理論最大吞吐量應(yīng)為 12800char/s（即圖中 baseline 一項(xiàng)）。由于串口控制器、中斷響應(yīng)與系統(tǒng)調(diào)用等額外負(fù)載，內(nèi)核態(tài)驅(qū)動最大吞吐量為理論值的 89%，而用戶態(tài)驅(qū)動的吞吐量與內(nèi)核態(tài)相差 1%左右。
【參考文獻(xiàn)】：
期刊論文
[1]嵌入式系統(tǒng)安全綜述[J]. 趙波,倪明濤,石源,樊佩茹. 武漢大學(xué)學(xué)報(bào)(理學(xué)版). 2018(02)
[2]未來網(wǎng)絡(luò)與工業(yè)互聯(lián)網(wǎng)發(fā)展綜述[J]. 吳文君,姚海鵬,黃韜,王露瑤,張延華,劉韻潔. 北京工業(yè)大學(xué)學(xué)報(bào). 2017(02)
[3]基于可信計(jì)算基的主機(jī)可信安全體系結(jié)構(gòu)研究[J]. 黃強(qiáng),常樂,張德華,汪倫偉. 信息網(wǎng)絡(luò)安全. 2016(07)
[4]關(guān)鍵基礎(chǔ)設(shè)施信息安全分析及防護(hù)[J]. 劉松,朱錢祥,陳開放. 智慧工廠. 2016(03)
[5]嵌入式操作系統(tǒng)的形式化驗(yàn)證研究[J]. 陳麗蓉,李允,羅蕾. 計(jì)算機(jī)科學(xué). 2015(08)
[6]設(shè)備驅(qū)動程序可靠性和正確性保障方法與技術(shù)研究進(jìn)展[J]. 張一帆,黃超,歐建生,湯恩義,陳鑫. 軟件學(xué)報(bào). 2015(02)
[7]微內(nèi)核中斷機(jī)制的形式化設(shè)計(jì)與驗(yàn)證[J]. 李康杰,錢振江,黃皓. 計(jì)算機(jī)科學(xué). 2013(03)
[8]操作系統(tǒng)對象語義模型（OSOSM）及形式化驗(yàn)證[J]. 錢振江,劉葦,黃皓. 計(jì)算機(jī)研究與發(fā)展. 2012(12)
[9]網(wǎng)卡驅(qū)動程序的用戶態(tài)移植和優(yōu)化[J]. 王燕飛,華蓓. 電子技術(shù). 2012(08)
[10]用戶態(tài)驅(qū)動框架的研究與實(shí)現(xiàn)[J]. 劉軍衛(wèi),李曦,陳香蘭,徐軍. 計(jì)算機(jī)系統(tǒng)應(yīng)用. 2011(11)
博士論文
[1]安全操作系統(tǒng)形式化設(shè)計(jì)與驗(yàn)證方法研究[D]. 錢振江.南京大學(xué) 2013
[2]面向目標(biāo)代碼的實(shí)時(shí)操作系統(tǒng)形式化驗(yàn)證方法研究[D]. 史建琦.華東師范大學(xué) 2012
[3]高可信嵌入式操作系統(tǒng)體系架構(gòu)研究[D]. 楊霞.電子科技大學(xué) 2010
[4]基于模型檢測的安全操作系統(tǒng)驗(yàn)證方法研究[D]. 程亮.中國科學(xué)技術(shù)大學(xué) 2009
碩士論文
[1]基于AUTOSAR的汽車電子操作系統(tǒng)及其應(yīng)用的建模與分析[D]. 彭云輝.華東師范大學(xué) 2014
本文編號：2969767
本文鏈接：http://www.wukwdryxk.cn/kejilunwen/jisuanjikexuelunwen/2969767.html
最近更新
教材專著
