隨著軟件規(guī)模的越來越大，軟件的安全越來越引起軟件開發(fā)人員的關注，而現(xiàn)有的編程語言以及軟件開發(fā)方法所能提供的安全保證是脆弱和不可靠的，例如通過標準的軟件工程方法和大量的測試減少軟件漏洞的發(fā)生，但是即使經過高強度測試的軟件，也不能保證它沒有漏洞，另外一方面，對一個漏洞的修復也往往會引起新的漏洞�？梢哉f，現(xiàn)有的軟件工程方法對軟件安全的提高已經越來越微弱。而基于語言的程序驗證方法能為軟件安全提供可靠的保證。 基于語言的程序驗證方法通過對程序設計語言添加靜態(tài)的類型以及規(guī)范結構，使得用這種語言寫出的良形式程序是安全的。現(xiàn)有的關于認證代碼技術以及類型系統(tǒng)方面的研究已經能夠驗證低級語言和高級語言程序的多種安全屬性。例如，當前的大部分程序設計語言都有一個類型系統(tǒng)，它一般用于檢查程序的一些簡單語義錯誤，可靠的類型系統(tǒng)可以以較低的代價保證程序的一些基本安全屬性。安全的高級語言和通用中間層語言的類型系統(tǒng)的研究已經對安全計算做了有意義的貢獻，但是用這些語言寫就的安全程序還需經過多步的未經編譯和優(yōu)化才能在最終的硬件上運行，這使得最終運行的代碼是未經驗證的�；谶@個原因，很多工作轉向研究低級代碼的驗證，特別...

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

【學位級別】：博士

【文章目錄】：
摘要
Abstract
第一章 背景介紹
    1.1 基本概念
        1.1.1 程序的安全屬性
        1.1.2 信任計算基
        1.1.3 規(guī)范語言的表達能力
    1.2 Curry-Howard同構
    1.3 Hoare邏輯
    1.4 類型系統(tǒng)
        1.4.1 類型化高級語言
        1.4.2 類型化匯編語言
    1.5 傳統(tǒng)的攜帶證明的代碼
        1.5.1 基于語義的基礎攜帶證明的代碼FPCC
        1.5.2 基于語法的FPCC
    1.6 本文的內容
第二章 程序規(guī)范語言GALLINA和定理證明工具Coq
    2.1 項語法
    2.2 GALLINA的命令語言Vernacular
    2.3 使用Coq描述程序規(guī)范
    2.4 Coq的交互式定理證明
    2.5 本節(jié)小結
第三章 一個簡單的支持函數(shù)調用返回的認證匯編語言RCAL86
    3.1 引言
    3.2 RCAL86的設計目標
    3.3 目標機器和操作語義
        3.3.1 RCAL86的抽象存儲模型
        3.3.2 RCAL86的操作語義
    3.4 靜態(tài)語義
        3.4.1 RCAL86程序良型性推理規(guī)則
        3.4.2 靜態(tài)推理規(guī)則的可靠性定理
    3.5 RCAL86下的程序安全性證明
        3.5.1 分離邏輯
        3.5.2 分離邏輯的Coq模塊
        3.5.3 Buddy空閑頁分配算法
        3.5.4 程序規(guī)范標注
        3.5.5 安全證明開發(fā)
    3.6 本章小結
第四章 一個MIPS認證匯編語言SCAP下的安全代碼開發(fā)
    4.1 SCAP的語法和目標機器模型
        4.1.1 語法
        4.1.2 操作語義
        4.1.3 操作語義的Coq表示
    4.2 SCAP的靜態(tài)推理規(guī)則
        4.2.1 規(guī)范結構
        4.2.2 推理規(guī)則
        4.2.3 可靠性定理
    4.3 SCAP下認證的動態(tài)存儲分配函數(shù)庫的開發(fā)
        4.3.1 動態(tài)存儲分配算法
        4.3.2 程序規(guī)范標注
        4.3.3 安全證明開發(fā)
    4.4 本章小結
第五章 機器字位級別抽象的擴展
    5.1 支持位運算的抽象機器模型
        5.1.1 機器字的位矢量表示
        5.1.2 抽象機器模型
    5.2 位運算的形式化推理
    5.3 位級別抽象的Coq實現(xiàn)
    5.4 在SCAP中增加位運算的支持
    5.5 本章小結
第六章 結論
    6.1 基于邏輯的高可信軟件開發(fā)方式分析
        6.1.1 開發(fā)效率
        6.1.2 軟件維護
        6.1.3 對傳統(tǒng)軟件開發(fā)模式的指導意義
    6.2 相關研究
        6.2.1 Hoare邏輯和分離邏輯
        6.2.2 認證匯編編程CAP
        6.2.3 攜帶證明的代碼PCC
        6.2.4 類型化匯編語言TAL
    6.3 未來工作
參考文獻
附錄
致謝
攻讀學位期間的主要研究工作和論文發(fā)表情況



本文編號：3737844