C程序精確形狀分析中的規(guī)范語言設(shè)計.pdf

1、隨著計算機技術(shù)的快速發(fā)展，計算機軟件的規(guī)模越來越大，軟件調(diào)試和維護越來越困難，其成本也越來越高，軟件的安全形勢變得越來越重要。特別是在安全攸關(guān)領(lǐng)域（例如，航空航天、高鐵、核電、醫(yī)療等領(lǐng)域），人們對高可信軟件的需求越來越大。在這些領(lǐng)域，C語言仍是最普遍使用的編程語言。而C程序中的空指針脫引用、內(nèi)存泄漏、緩沖區(qū)溢出等諸多內(nèi)存安全問題在軟件開發(fā)中依然突出。
　　提高軟件質(zhì)量的方法有很多種，如軟件測試、程序分析和程序驗證等;在眾多方法中，

2、相對有效而又經(jīng)濟的方法是程序靜態(tài)分析。針對C程序中內(nèi)存安全問題，作者所在實驗室的課題組開發(fā)了一個靜態(tài)分析工具，該工具采用了符號執(zhí)行的靜態(tài)分析技術(shù)，并加入了形狀分析，為了降低靜態(tài)分析的誤報率和漏報率，以及提高分析的效率，設(shè)計了表達能力較為豐富的規(guī)范語言來描述程序狀態(tài)和函數(shù)行為。
　　在該靜態(tài)分析工具的實現(xiàn)中，設(shè)計了描述函數(shù)行為的規(guī)范語言，包括描述程序狀態(tài)的基本斷言，描述內(nèi)存狀態(tài)的謂詞以及描述單鏈表、雙鏈表、二叉樹的形狀謂詞。該工具基

3、于編譯框架LLVM和符號執(zhí)行分析工具KLEE，以函數(shù)為單位分析并構(gòu)造函數(shù)行為規(guī)范，該過程中需要用斷言描述程序狀態(tài)并按需抽象成形狀謂詞。為此，針對斷言設(shè)計了一系列的規(guī)范化和抽象化規(guī)則。
　　本文的貢獻主要有三方面:第一，設(shè)計并實現(xiàn)了描述函數(shù)行為的規(guī)范語言，包括描述程序狀態(tài)的基本斷言，描述內(nèi)存的謂詞以及描述單鏈表、雙鏈表、二叉樹的形狀謂詞。通過規(guī)范語言來記錄已分析函數(shù)的行為，可以避免重復分析，提高分析的效率。通過使用描述內(nèi)存的謂詞和形

4、狀謂詞，該工具可以檢測內(nèi)存泄漏、空指針脫引用等內(nèi)存安全問題以及進行形狀分析。第二，設(shè)計并實現(xiàn)了一系列的規(guī)則來規(guī)范和抽象斷言，將程序狀態(tài)抽象成形狀謂詞，用于形狀分析。第三，利用已有的規(guī)范語言為C語言標準庫函數(shù)構(gòu)造函數(shù)行為規(guī)范。許多程序中會頻繁調(diào)用C的庫函數(shù)，為這些常用的庫函數(shù)手動構(gòu)造行為規(guī)范可以提高分析的精度和效率。
　　本文工作的意義在于針對C程序內(nèi)存安全問題，提出了一套規(guī)范語言;并針對形狀分析，提出了一系列的抽象化規(guī)則，用于精確