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

【相似文獻】

相關期刊論文 前10條

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

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

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

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

5 ;開卷有益[J];計算機安全;2003年07期

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

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

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

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

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

相關博士學位論文 前10條

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

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

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

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

5 王志芳;指針邏輯的擴展與應用[D];中國科學技術大學;2009年

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

7 李隆;使用事務內存同步機制的并行程序驗證的研究[D];中國科學技術大學;2008年

8 張秀峰;AOP技術及其在軟件安全中的應用[D];北京郵電大學;2008年

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

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

相關碩士學位論文 前10條

1 蔣信予;用形式化方法構建安全的線程機制[D];中國科學技術大學;2009年

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

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

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

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

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

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

8 王濤;基于安全模式的軟件安全設計方法[D];吉林大學;2011年

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

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

本文編號：2879340