交通、電力、軍事等關(guān)鍵領(lǐng)域?qū)浖目煽啃院桶踩砸笤絹碓礁?因?yàn)槠鋰?yán)重關(guān)乎國民的人身和財(cái)產(chǎn)安全。C語言在上述基礎(chǔ)領(lǐng)域軟件的開發(fā)中有廣泛的應(yīng)用。C語言靈活高效的特性允許程序員做相當(dāng)?shù)讓拥牟僮?但也導(dǎo)致C程序容易出現(xiàn)非法指針解引用、內(nèi)存泄漏、緩沖區(qū)溢出等缺陷。形式化驗(yàn)證是一種可以嚴(yán)格保證程序可靠性的方法。本課題組正在研發(fā)一個(gè)安全C語言驗(yàn)證器,其功能是對(duì)攜有程序標(biāo)注的安全C語言程序進(jìn)行演繹推理,驗(yàn)證程序是否滿足預(yù)期規(guī)范。安全C語言驗(yàn)證器中驗(yàn)證條件生成器的作用是支持安全C語言和規(guī)范語言SCSL的語法,實(shí)現(xiàn)每條語句的演算規(guī)則,并根據(jù)演算規(guī)則遍歷源程序進(jìn)行演算,同時(shí)產(chǎn)生程序點(diǎn)的斷言和合理有效的驗(yàn)證條件。本文的工作是對(duì)安全C語言驗(yàn)證器中的驗(yàn)證條件生成器進(jìn)行擴(kuò)展。本文的主要工作和貢獻(xiàn)如下:第一、參與規(guī)范語言SCSL中邏輯變量、幽靈代碼、字符串類型、帶命名行為協(xié)議和多函數(shù)協(xié)議的設(shè)計(jì),提高了規(guī)范語言的表達(dá)能力,同時(shí)獨(dú)立設(shè)計(jì)和實(shí)現(xiàn)了對(duì)應(yīng)的演算規(guī)則。第二、基于Hoare邏輯設(shè)計(jì)和實(shí)現(xiàn)跳轉(zhuǎn)語句goto、continue和break、選擇語句switch以及函數(shù)調(diào)用語句的演算規(guī)則,使得驗(yàn)證器可以支持更多C的語法...

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

【學(xué)位級(jí)別】：碩士

【文章目錄】：
摘要
ABSTRACT
第1章 緒論
    1.1 研究背景
        1.1.1 軟件安全問題
        1.1.2 形式化驗(yàn)證
        1.1.3 研究現(xiàn)狀
    1.2 本文概述
        1.2.1 研究工作
        1.2.2 主要貢獻(xiàn)
        1.2.3 章節(jié)安排
第2章 Safe-C驗(yàn)證器
    2.1 Safe-C與程序標(biāo)注
    2.2 Hoare邏輯
    2.3 驗(yàn)證器的框架與驗(yàn)證流程
    2.4 驗(yàn)證條件生成器的架構(gòu)
    2.5 單個(gè)函數(shù)的驗(yàn)證過程
    2.6 本章小結(jié)
第3章 SCSL的擴(kuò)展設(shè)計(jì)以及對(duì)應(yīng)的演算規(guī)則
    3.1 邏輯變量
    3.2 幽靈代碼
    3.3 字符串
        3.3.1 邏輯字符串
        3.3.2 字符串類型的操作與內(nèi)置函數(shù)
        3.3.3 字符串的演算策略
        3.3.4 字符串操作語句的演算規(guī)則
    3.4 對(duì)函數(shù)協(xié)議的擴(kuò)展
        3.4.1 簡單函數(shù)協(xié)議
        3.4.2 帶命名行為的函數(shù)協(xié)議
        3.4.3 多協(xié)議
    3.5 本章小結(jié)
第4章 語句的演算規(guī)則與事務(wù)的處理
    4.1 部分語句的演算規(guī)則
        4.1.1 goto語句和label語句
        4.1.2 continue語句
        4.1.3 break語句
        4.1.4 switch語句
    4.2 函數(shù)調(diào)用語句的演算規(guī)則
        4.2.1 無邏輯變量時(shí)的演算過程
        4.2.2 有邏輯變量時(shí)的演算過程
    4.3 賦值語句前事務(wù)的處理
        4.3.1 賦值語句前對(duì)量化斷言的展開
        4.3.2 賦值語句前對(duì)謂詞的展開
    4.4 本章小結(jié)
第5章 棧區(qū)內(nèi)存模型
    5.1 Hoare邏輯賦值規(guī)則與別名
    5.2 棧區(qū)內(nèi)存模型
    5.3 驗(yàn)證點(diǎn)處斷言和內(nèi)存表的構(gòu)造
        5.3.1 函數(shù)入口處斷言與內(nèi)存表的構(gòu)造
        5.3.2 循環(huán)入口處斷言與內(nèi)存表的構(gòu)造
    5.4 取地址和解引用操作
    5.5 別名判斷算法
    5.6 棧區(qū)賦值語句演算規(guī)則
        5.6.1 棧區(qū)變量賦值
        5.6.2 指針關(guān)系運(yùn)算
    5.7 本章小結(jié)
第6章 驗(yàn)證實(shí)例與測試分析
    6.1 查找最大值和最小值函數(shù)的驗(yàn)證
    6.2 字符串拷貝函數(shù)的驗(yàn)證
    6.3 快速排序函數(shù)的驗(yàn)證
    6.4 測試結(jié)果分析
    6.5 本章小結(jié)
第7章 總結(jié)與展望
    7.1 總結(jié)和相關(guān)工作對(duì)比
    7.2 不足和進(jìn)一步工作展望
參考文獻(xiàn)
致謝
在讀期間發(fā)表的學(xué)術(shù)論文與取得的其他研究成果



本文編號(hào)：3913193