一種基于契約的安全分析方法的研究與實現(xiàn)
發(fā)布時間:2021-10-17 00:34
本文針對C/C++程序安全漏洞,提出并實現(xiàn)了一種基于契約的安全分析方法。該方法采用自下而上分析遍歷程序中的函數(shù)體,將跨過程分析轉(zhuǎn)變?yōu)檫^程內(nèi)分析;提供安全規(guī)則描述方法,使得用戶可以擴展安全規(guī)則;通過為變量和函數(shù)附加契約以記錄其前置和后置條件,并在程序分析的過程中按照規(guī)則更新契約,使得在程序分析時自動進行安全檢查。該方法具有代價小,靈活性強的特點,可以用來檢查程序中指針非法引用、函數(shù)調(diào)用時實參或全局變量的狀態(tài)不合法、內(nèi)存泄漏及其他資源泄漏等安全漏洞。
【文章來源】:西安電子科技大學陜西省 211工程院校 教育部直屬院校
【文章頁數(shù)】:85 頁
【學位級別】:碩士
【文章目錄】:
摘要
ABSTRACT
第一章 緒論
1.1 研究背景
1.2 課題解決方案
1.3 本文主要工作
第二章 自下而上分析方法中的契約
2.1 自下而上分析
2.2 變量契約與函數(shù)契約
2.3 契約信息
第三章 基于契約的安全分析方法的設計
3.1 安全判定規(guī)則
3.2 契約更新規(guī)則
3.3 基于契約的安全分析算法
第四章 基于契約的安全分析方法的實現(xiàn)
4.1 程序框架
4.2 配置文件格式定義模塊
4.2.1 配置文件格式定義
4.2.2 系統(tǒng)默認契約信息
4.3 契約信息模塊
4.3.1 契約信息的定義
4.3.2 契約信息的提取
4.3.2.1 Expat介紹
4.3.2.2 使用Expat編寫XML解析器提取契約信息
4.4 前后置條件的狀態(tài)保存模塊
4.4.1 狀態(tài)條件表達式
4.4.2 構建狀態(tài)條件語法樹
4.4.3 消除非運算符節(jié)點
4.4.4 轉(zhuǎn)化為析取范式語法樹
4.4.5 提取狀態(tài)二重集合
4.4.6 優(yōu)化狀態(tài)二重集合
4.4.7 方法的優(yōu)化
4.4.8 方法的整合
4.4.9 實例
4.5 契約結(jié)構定義模塊
4.5.1 變量契約的數(shù)據(jù)結(jié)構
4.5.2 函數(shù)契約的數(shù)據(jù)結(jié)構
4.6 安全判定的實現(xiàn)
4.6.1 變量契約的安全判定
4.6.2 變量失效前的安全判定
4.6.3 函數(shù)調(diào)用時的安全判定
4.7 契約更新的實現(xiàn)
4.7.1 變量契約更新
4.7.1.1 順序結(jié)構中變量契約的更新
4.7.1.2 分支結(jié)構中變量契約的更新
4.7.2 函數(shù)調(diào)用時的契約更新
4.7.3 函數(shù)返回時的契約更新
第五章 安全實例分析
結(jié)束語
致謝
參考文獻
作者在讀期間研究成果
附錄A 配置文件格式定義
附錄B 系統(tǒng)默認契約信息
附錄C 細化的安全分析算法
附錄D 對程序P的安全分析過程
本文編號:3440784
【文章來源】:西安電子科技大學陜西省 211工程院校 教育部直屬院校
【文章頁數(shù)】:85 頁
【學位級別】:碩士
【文章目錄】:
摘要
ABSTRACT
第一章 緒論
1.1 研究背景
1.2 課題解決方案
1.3 本文主要工作
第二章 自下而上分析方法中的契約
2.1 自下而上分析
2.2 變量契約與函數(shù)契約
2.3 契約信息
第三章 基于契約的安全分析方法的設計
3.1 安全判定規(guī)則
3.2 契約更新規(guī)則
3.3 基于契約的安全分析算法
第四章 基于契約的安全分析方法的實現(xiàn)
4.1 程序框架
4.2 配置文件格式定義模塊
4.2.1 配置文件格式定義
4.2.2 系統(tǒng)默認契約信息
4.3 契約信息模塊
4.3.1 契約信息的定義
4.3.2 契約信息的提取
4.3.2.1 Expat介紹
4.3.2.2 使用Expat編寫XML解析器提取契約信息
4.4 前后置條件的狀態(tài)保存模塊
4.4.1 狀態(tài)條件表達式
4.4.2 構建狀態(tài)條件語法樹
4.4.3 消除非運算符節(jié)點
4.4.4 轉(zhuǎn)化為析取范式語法樹
4.4.5 提取狀態(tài)二重集合
4.4.6 優(yōu)化狀態(tài)二重集合
4.4.7 方法的優(yōu)化
4.4.8 方法的整合
4.4.9 實例
4.5 契約結(jié)構定義模塊
4.5.1 變量契約的數(shù)據(jù)結(jié)構
4.5.2 函數(shù)契約的數(shù)據(jù)結(jié)構
4.6 安全判定的實現(xiàn)
4.6.1 變量契約的安全判定
4.6.2 變量失效前的安全判定
4.6.3 函數(shù)調(diào)用時的安全判定
4.7 契約更新的實現(xiàn)
4.7.1 變量契約更新
4.7.1.1 順序結(jié)構中變量契約的更新
4.7.1.2 分支結(jié)構中變量契約的更新
4.7.2 函數(shù)調(diào)用時的契約更新
4.7.3 函數(shù)返回時的契約更新
第五章 安全實例分析
結(jié)束語
致謝
參考文獻
作者在讀期間研究成果
附錄A 配置文件格式定義
附錄B 系統(tǒng)默認契約信息
附錄C 細化的安全分析算法
附錄D 對程序P的安全分析過程
本文編號:3440784
本文鏈接:http://sikaile.net/falvlunwen/hetongqiyue/3440784.html