摘要：

整數(shù)缺陷是一類與整數(shù)的有限表示相關(guān)的程序缺陷,對軟件系統(tǒng)的可靠性和安全性均有重要影響.人工審查難以發(fā)現(xiàn)涉及復(fù)雜程序邏輯的,由邊界輸入觸發(fā)的缺陷.此外,由于C的整數(shù)語義的復(fù)雜性,整數(shù)缺陷的修復(fù)是極易出錯的.為了實現(xiàn)準(zhǔn)確且高效的自動化整數(shù)缺陷檢測與修復(fù),本文從邏輯推理,靜態(tài)分析和修復(fù)實施3個自底向上的層次開展了研究,主要內(nèi)容包括:1.提出了面向多核CPU的理論域上可滿足性判定的并行化框架LDC,并給出了LDC的可靠性和完備性證明.本文將該框架應(yīng)用于無量詞等值理論域,證明了終止性,并實現(xiàn)了并行SMT求解器PZ3.在SMT-LIB測試集以及隨機問題上的實驗結(jié)果表明PZ3能夠成功加速多種不同類型問題的求解,并且其并行加速的效果勝過了最先進的基于配置組合方法的并行求解器.2.為了高效地對程序的局部性質(zhì)進行精確分析,提出了基于分而治之思想的組合靜態(tài)分析框架C~2PA并證明了其可靠性.本文面向C~2PA設(shè)計了一種新的C程序整數(shù)數(shù)值語義分析算法,并實現(xiàn)了靜態(tài)分析工具Tsmart-BD.實驗結(jié)果表明,Tsmart-BD在標(biāo)準(zhǔn)測試集上漏報率為0.0%,誤報率為12.7%,領(lǐng)先于知名開源靜態(tài)分析工具和軟件驗證工具.此外Tsmart-BD能夠在7.5分鐘內(nèi)完整分析規(guī)模超過320kLOC的開源軟件Vim.3.提出了兩種整數(shù)缺陷自動修復(fù)方法:(1)對C程序的整數(shù)操作進行精度提升,以消除編譯得到的可執(zhí)行程序中的整數(shù)缺陷,(2)面向缺陷的基于典型修復(fù)模式的修復(fù)生成.兩種方法分別實現(xiàn)為工具CIntFix和IntPTI,且均能正確修復(fù)測試集上的所有目標(biāo)缺陷.在開源項目上,CIntFix以1.18kLOC/s的速率完成對556.416kLOC代碼的變形;IntPTI能夠避免對96.3%的關(guān)鍵程序位置的更改,且修復(fù)引入的額外時間開銷僅為0.5%.本文的研究成果均已集成到軟件可信保障工具集Tsmart,并在實際的列車控制系統(tǒng)嵌入式軟件的開發(fā)流程中進行了工程化應(yīng)用實踐,成功發(fā)現(xiàn)并修復(fù)了67個新的整數(shù)缺陷.

展開

總結(jié)

以上是生活随笔為你收集整理的c语言整数检验,C程序整数缺陷的检测与修复的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。