并行系統(tǒng)的安全性隨著其流行程度的增加,顯得日益重要。以往在這方面大多數(shù)研究的重點(diǎn)是,在并行機(jī)制的實(shí)現(xiàn)(OS,線程庫)已經(jīng)安全的假定下,如何保證并行程序本身的安全性。對于如何保證并行機(jī)制本身的安全性,目前的解決方案不是不完整,就是非常復(fù)雜。到了如今,大多數(shù)并行機(jī)制的實(shí)現(xiàn)者仍然主要依賴傳統(tǒng)的動(dòng)態(tài)測試方法。 為了探索如何用形式化驗(yàn)證的方法來保證并行機(jī)制本身的安全,本文中設(shè)計(jì)了一個(gè)類似GNU pth library的用戶級別線程庫,并用類MIPS的匯編語言編寫了它的一個(gè)實(shí)現(xiàn)。與通常的線程庫不同的是,該線程庫攜帶了安全規(guī)范及其證明。這些規(guī)范與證明保證,如果用戶程序?qū)υ摼�程庫API的調(diào)用始終滿足規(guī)范,那么線程庫的代碼必然可以安全執(zhí)行。更重要的是,從這些規(guī)范與證明不僅能得到線程庫本身的安全性,還能得到線程庫和用戶程序交互的安全性。為了讓本文的驗(yàn)證方法可以用于更復(fù)雜的代碼,文中還提出了一些簡化程序規(guī)范和降低證明代價(jià)的方法。 本文中的所有形式化工作,都是在證明輔助工具Coq上完成的。對于本文提出的線程庫,其安全性證明可以用機(jī)器檢查。而該線程庫的安全性,僅僅依賴于證明檢查工具的正確性,這意味著它是一個(gè)攜帶證明代碼包(PCC package),可以直接用于對安全性要求非常高的場合。
【學(xué)位單位】：中國科學(xué)技術(shù)大學(xué)
【學(xué)位級別】：碩士
【學(xué)位年份】：2009
【中圖分類】：TP338.6
【文章目錄】：
摘要
Abstract
第1章 緒論
    1.1 研究背景和意義
    1.2 研究現(xiàn)狀
        1.2.1 基于類型系統(tǒng)的并發(fā)系統(tǒng)安全研究
        1.2.2 基于程序驗(yàn)證的并發(fā)系統(tǒng)安全研究
    1.3 本文工作與貢獻(xiàn)
    1.4 章節(jié)安排
第2章 術(shù)語表
第3章 基本設(shè)定與主要技術(shù)
    3.1 歸納構(gòu)造演算與證明輔助工具 Coq
        3.1.1 歸納構(gòu)造演算
        3.1.2 證明輔助工具Coq
    3.2 抽象機(jī)器模型
    3.3 并發(fā)代碼的推理方法
        3.3.1 假設(shè)-保證推理方法
        3.3.2 并發(fā)分離邏輯
    3.4 基于語法的攜帶基礎(chǔ)證明代碼
        3.4.1 攜帶基礎(chǔ)證明代碼
        3.4.2 用語法制導(dǎo)的推理規(guī)則描述程序邏輯
        3.4.3 抽象控制棧
        3.4.4 支持假設(shè)-保證推理方法
        3.4.5 攜帶證明代碼模塊的連接
第4章 一個(gè)簡單的線程庫
    4.1 API
    4.2 線程模型與基本數(shù)據(jù)結(jié)構(gòu)
    4.3 實(shí)現(xiàn)簡要
第5章 線程庫的安全規(guī)范與證明
    5.1 證明方法
    5.2 接口規(guī)范
    5.3 實(shí)現(xiàn)規(guī)范
    5.4 實(shí)現(xiàn)規(guī)范的證明
    5.5 接口規(guī)范的證明
第6章 證明的簡化
第7章 實(shí)用價(jià)值分析
    7.1 實(shí)用價(jià)值
    7.2 TCB 范圍
第8章 相關(guān)工作比較
    8.1 Mth
    8.2 Verisoft XT
第9章 結(jié)論
參考文獻(xiàn)
致謝
在讀期間發(fā)表的學(xué)術(shù)論文與取得的其他研究成果

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 胡恬;王宏;;原代碼級的軟件安全問題研究[J];軟件導(dǎo)刊;2007年01期

2 羊建林;周安民;;Windows異常處理與軟件安全[J];信息安全與通信保密;2011年04期

3 ;軟件安全消費(fèi)新觀念[J];電腦采購周刊;1999年10期

4 丹三;;軟件安全不容忽視[J];電腦采購周刊;1999年10期

5 ;開卷有益[J];計(jì)算機(jī)安全;2003年07期

6 呂華鵬;;軟件反跟蹤技術(shù)淺析[J];才智;2008年11期

7 王遠(yuǎn)景;;軟件常見安全性缺陷與測試手段[J];科技創(chuàng)新導(dǎo)報(bào);2009年28期

8 林洪，陳國良;并行系統(tǒng)的通訊效率問題[J];小型微型計(jì)算機(jī)系統(tǒng);1996年01期

9 呂金和;;由指針和數(shù)組帶來的軟件安全性缺陷[J];計(jì)算機(jī)安全;2010年05期

10 趙妍;;計(jì)算機(jī)軟件安全檢測方法探討[J];科技傳播;2010年16期

相關(guān)博士學(xué)位論文 前10條

1 馮博;軟件安全開發(fā)關(guān)鍵技術(shù)的研究和實(shí)現(xiàn)[D];北京郵電大學(xué);2010年

2 王桂彬;大規(guī)模異構(gòu)并行系統(tǒng)軟件低功耗優(yōu)化關(guān)鍵技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2011年

3 成斌;基于TCPN模型的并行系統(tǒng)性能分析方法研究[D];上海大學(xué);2011年

4 郭宇;模塊化構(gòu)造軟件系統(tǒng)安全性證明的研究[D];中國科學(xué)技術(shù)大學(xué);2007年

5 王志芳;指針邏輯的擴(kuò)展與應(yīng)用[D];中國科學(xué)技術(shù)大學(xué);2009年

6 石巖;凝視紅外成像信息處理系統(tǒng)圖像預(yù)處理方法與系統(tǒng)軟件研究[D];華中科技大學(xué);2005年

7 李隆;使用事務(wù)內(nèi)存同步機(jī)制的并行程序驗(yàn)證的研究[D];中國科學(xué)技術(shù)大學(xué);2008年

8 張秀峰;AOP技術(shù)及其在軟件安全中的應(yīng)用[D];北京郵電大學(xué);2008年

9 葛琳;可信軟件開發(fā)框架下的出具證明編譯研究[D];中國科學(xué)技術(shù)大學(xué);2007年

10 陳研;面向有狀態(tài)應(yīng)用的并行系統(tǒng)設(shè)計(jì)研究[D];上海交通大學(xué);2007年

相關(guān)碩士學(xué)位論文 前10條

1 蔣信予;用形式化方法構(gòu)建安全的線程機(jī)制[D];中國科學(xué)技術(shù)大學(xué);2009年

2 翟宇;基于軟件安全契約的AOP監(jiān)控方法[D];吉林大學(xué);2011年

3 賈景璽;有限元并行系統(tǒng)用于岔管計(jì)算的研究[D];蘭州大學(xué);2011年

4 鄧凡;軟件安全檢查工具前端的設(shè)計(jì)與實(shí)現(xiàn)[D];西安電子科技大學(xué);2009年

5 賈燕成;基于以太網(wǎng)并行系統(tǒng)實(shí)時(shí)仿真調(diào)度算法研究[D];云南大學(xué);2012年

6 吳侃;星載并行系統(tǒng)主從式互連總線容錯(cuò)技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2011年

7 趙志威;基于加殼與加密技術(shù)的軟件安全的研究[D];華中科技大學(xué);2012年

8 王濤;基于安全模式的軟件安全設(shè)計(jì)方法[D];吉林大學(xué);2011年

9 劉艷;分布式網(wǎng)絡(luò)并行系統(tǒng)在艦載指控系統(tǒng)中的應(yīng)用研究[D];哈爾濱工程大學(xué);2003年

10 杜洪偉;軟件安全領(lǐng)域垂直搜索引擎的優(yōu)化設(shè)計(jì)與實(shí)現(xiàn)[D];天津大學(xué);2010年

本文編號(hào)：2879340