動態(tài)符號執(zhí)行約束求解優(yōu)化設計與實現(xiàn).pdf

1、從上個世紀至今，計算機的各個領域都取得了長足的進步，軟件作為存儲和管理信息的工具，已廣泛深入到現(xiàn)實社會的各個領域，成為整個社會的支柱產業(yè)之一，正是因為軟件的重要性日益提升，軟件漏洞可能帶來的損失也越來越大，特別是在對軟件漏洞比較敏感的領域，例如：金融、瓦斯檢測、航天等行業(yè)，任何一個不易察覺的漏洞都可能引災難性事故。程序分析技術和軟件測試技術的目的在于，確保待分析程序的正確性、一致性以及確保程序在安全狀態(tài)下運行。軟件測試的發(fā)展過程中，出現(xiàn)

2、了一系列的測試技術，從最初的靜態(tài)代碼分析技術到曾經被廣泛使用的糊測試技術，軟件測試技術也隨著現(xiàn)代計算機水平的進步和軟件行業(yè)對安全需求的提升而不斷地發(fā)展。
　　符號執(zhí)行技術于上世紀70年代被提出，受限于當時的軟硬件條件未被廣泛應用，隨著近些年計算機技術的發(fā)展，符號執(zhí)行技術被再一次重視起來。動態(tài)符號執(zhí)行技術是一種衍生于傳統(tǒng)符號執(zhí)行的新技術，采用符號與具體值相結合的方式，有著代碼覆蓋率高、可以自動生成測試用例等特點。動態(tài)符號執(zhí)行技術一經

3、提出就受到了眾多軟件公司和研究人員的重視，在學術界和產業(yè)界均取得了較大的進步，并且形成了了一系列工具，在實際應用中有著較好的效果。但是，目前為止，動態(tài)符號執(zhí)行技術還存在一些難以解決的問題，例如，路徑爆炸以及面對應用領域復雜性和程序設計語言復雜性時所受到的局限等等。
　　本文著眼于動態(tài)符號執(zhí)行的約束求解優(yōu)化問題，提出一種針對約束集合的基于線性規(guī)劃技術的優(yōu)化方法，通過此優(yōu)化方法可以降低約束集合中約束條件的復雜性，降低后續(xù)求解生成測試用

4、例過程的計算復雜度，從一定程度上提升了約束求解過程的效率，本文選擇KLEE作為研究對象，為其約束求解部分增加一個LP_OP模塊，在該模塊中實現(xiàn)了線性規(guī)劃優(yōu)化過程，以達到提高動態(tài)符號執(zhí)行約束求解過程效率的目的。
　　為驗證LP_OP模塊對KLEE約束求解效率的提升，本文選擇幾個常用工具作為分析對象，使用KLEE對這些程序進行程序分析并生成相應的測試用例。通過對比加入LP_OP模塊前后約束求解過程消耗的時間和整個KLEE執(zhí)行過程消耗的