基于CEGAR的C程序數(shù)組越界檢測(cè).pdf

1、隨著計(jì)算機(jī)硬件技術(shù)的發(fā)展，軟件的復(fù)雜度越來(lái)越高，規(guī)模越來(lái)越大，應(yīng)用也越來(lái)越廣泛。與此同時(shí)，軟件中的安全缺陷和漏洞也越來(lái)越多，軟件安全問(wèn)題越來(lái)越突出。因此，如何保證軟件系統(tǒng)的正確性、可靠性和安全性是當(dāng)前軟件開(kāi)發(fā)面臨的重要問(wèn)題之一。
　　作為一種重要的自動(dòng)化驗(yàn)證技術(shù)，模型檢測(cè)是提高程序可靠性和安全性的重要途徑。C語(yǔ)言是軟件開(kāi)發(fā)中最為廣泛使用的編程語(yǔ)言之一。它的語(yǔ)法靈活，操作方便，但是如果使用不當(dāng)，就會(huì)留下被攻擊的程序漏洞。數(shù)組越界是C

2、程序中普遍存在的一種程序缺陷，該缺陷可能會(huì)成為日后程序被攻擊的漏洞，對(duì)軟件安全造成了潛在的威脅。如何檢測(cè)C程序中的數(shù)組越界是一個(gè)重要的研究課題。本文研究基于CEGAR的C程序數(shù)組越界驗(yàn)證方法。首先，研究基于CEGAR技術(shù)的C程序PPTL模型檢測(cè)算法。然后，研究數(shù)組越界的PPTL形式化描述。最后，通過(guò)檢測(cè)程序是否滿足性質(zhì)來(lái)驗(yàn)證程序中是否存在數(shù)組越界問(wèn)題。為了提高自動(dòng)化驗(yàn)證水平，本文對(duì)所關(guān)聯(lián)的數(shù)組自動(dòng)生成PPTL性質(zhì)，從而避免了手工在C程序