深入了解符號執行

2021-09-25 07:14:40 字數 2176 閱讀 3809

符號執行分類之間的不同

靜態分析方法是從語法或語義的層面分析程式文字(源**或二進位制)

動態分析方法是通過執行待測程式以獲取和分析程式執行過程中產生的動態資訊,以判斷其執行時語義性質

二進位制分析多採用動態分析方法,源**分析多採用靜態分析方法。

動態分析只獲取程式的實際可行路徑和可達狀態,但由於其大多時候並不能便歷程式的所有可行路徑,因而可能錯過了某些可以引發程式錯誤的執行路徑,進而導致漏報。但這也保證分析結果沒有誤報的根本原因。(即動態分析方法對程式的實際可達做下進似處理)

大部分的靜態分析方法為了建立用於分析的模型需要對程式的動態語義做某種形式的抽象,其抽象結果會引入實際不可行路徑和不可達狀態,而靜態分析方法難以在有限時間內判定抽象路徑的可行性,這是導致誤報的主要原因。(即靜態分析方法在對被分析程式的實際可達狀態做上近似處理)

也有一些靜態方法同時做上近似和下近似,同時引入了漏報和誤報

圖1,不同近似方式引起漏報和誤報

自動化白盒模糊測試

1)對靜態符號執行進行擴充套件,混合具體執行提出輕量級動態符號執行方法:concolic執行;

2)借助於逐漸實用化的smt求解器技術對路徑約束求解。

3)使用新的啟發式演算法探索程式的路徑空間(程式執行樹)。

由於靜態與動態分析方法在執行中只能達到近似而導致漏報和誤報,concolic執行對兩種分析方法進行了混合,在具體執行的同時對所執行到的**施行符號執行,這樣一來,具體執行的特性決定了每次的concolic執行獲取的路徑都是可行路徑,因此避免了誤報。這是concolic執行對於靜態分析方法的優勢。

另一方面,對於某種超出了求解器的求解能力範圍的**,concolic能夠進行簡化反還乙個簡化後的符號表示式。這個過程被稱為路徑約束的部分具體化

對應**的符號執行樹

例入上述**中,傳入引數x=2,y=33,x^3==y為非線性約束,超出了求解器的求解能力範圍,靜態符號執行在這個時候就會丟棄掉這個分支,因而導致了漏報。

concolic由於混合了具體執行,可以獲取到x和y的上一次執行中的具體取值,然後得到部分具體化的路徑約束為8==y,即第二次執行時使用 x==2,y==8作為新的測試輸入,使第13行得到執行。

路徑空間啟發式搜尋演算法和路徑選擇

由於路徑**問題的存在,完全遍歷整個路徑空間常常是不可能的。

1)對路徑約束變異,concolic執行在每次執行完畢一條程式路徑後會得到一組路徑約束,dart和cute對其中最後乙個約束取反以產生新的路徑約束,實際上是對符號執行樹做深度優先搜尋,這意味著對一條路徑上非葉子節點的符號執行將會執行多次,同樣,對相同的中間性路徑約束需要多次求解,按代搜尋演算法,每得到一組路徑約束後,按照不同組合對其中多個約束取反,得到多組新的路徑約束。減少了重複計算,方便並行求解。

2)對基本塊覆蓋打分,程式在每個分支處使用打分函式給當前路徑

已經執行的部分設定分值,打分的依據可以為:距離未覆蓋指令的距離、呼叫棧高度或被呼叫符號程序的最近一次執行是否覆蓋了新基本塊.klee被設計為可以同時執行多條路徑,可以視為對程式路的併發執行,每次使用排程演算法在現存的路徑集合中選取一條執行,其選取的標準就是路徑集合中分值最高者.這種方法借鑑了貪心演算法的思想,即最重要的應該被優先處理。

插裝實現對concolic執行對程式的實際執**況的觀察。

1)基於源**的手動和自動插裝

2)基於中間**的插裝

先將源**編譯成某種中間語言**,再針對每條中間語言指令插入呼叫指令。

3)動態二進位制插裝

在不能獲取程式源**的情況下,可以借助於動態插裝工具對可執行程式做動態二進位制插裝。

4)二進位制離線插裝

①抓取二進位制執行軌跡

②對其靜態插裝

③重放插裝後軌跡並獲取需要的約束條件。

路徑**

對於無限迴圈體可以採用類似於限界符號執行,對迴圈部分只做有限次數的搜尋。

一種較新疑的方法是路徑約束抽象方法,通過路徑剪裁演算法可較好的環節路徑**問題。

一種環節路徑**的動態符號執行方法

參考**一

參考文章二

『smt相關

深入了解A

一 前言 在這裡我將對a 演算法的實際應用進行一定的 並且舉乙個有關a 演算法在最短路徑搜尋的例子。值得注意的是這裡並不對a 的基本的概念作介紹,如果你還對a 演算法不清楚的話,請看姊妹篇 初識a 演算法 這裡所舉的例子是參考amit主頁中的乙個源程式,使用這個源程式時,應該遵守一定的公約。二 a ...

深入了解A

一 前言 在這裡我將對a 演算法的實際應用進行一定的 並且舉乙個有關a 演算法在最短路徑搜尋的例子。值得注意的是這裡並不對a 的基本的概念作介紹,如果你還對a 演算法不清楚的話,請看姊妹篇 初識a 演算法 這裡所舉的例子是參考amit主頁中的乙個源程式,使用這個源程式時,應該遵守一定的公約。二 a ...

深入了解Dojo Data

譯自http www.sitepen.com blog 2010 10 13 dive into dojo data 使用dojo data有助於快速建立web應用的介面,且易於嵌入各種資料來源。它在使用者介面與底層資料之間提供了一層抽象層,使得使用者介面開發人員能夠專注於ui的開發,而無需擔心資料...