[[182416]]

一、前言

代碼覆蓋測試主要用于漏洞研究領域。主要目的是使用不同輸入覆蓋程序代碼的不同部分。如果某個輸入導致程序崩潰，我們將檢測崩潰是否能被利用。有很多代碼覆蓋測試的方法，比如隨機測試等。但是本文重點關注使用動態(tài)符號執(zhí)行進行代碼覆蓋測試。覆蓋代碼不意味著能找到所有的可能的缺陷。一些缺陷不會引起程序崩潰。然而2017年剛到，勒索軟件以驚人的速度爆發(fā)。這周我們發(fā)現了大量的新變種，尤其是以很有名的名次命名的FSociety。我們也發(fā)現了一些解密工具，圣誕節(jié)有關的勒索軟件，CryptoMix/CryptFile2的分析，大量的小的勒索軟件。

二、代碼覆蓋和動態(tài)符號執(zhí)行(DSE)

不像SSE(靜態(tài)符號執(zhí)行)，DSE應用于跟蹤，并且只有在執(zhí)行期間達到這些分支時才能發(fā)現新的分支。要想到達另一個路徑，我們必須搞清楚從上個跟蹤發(fā)現的分支約束條件。然后我們重復操作，直到到達所有分支。

舉個例子，我們假設程序P 有稱為I的輸入。I可以是模型M或者隨機種子R。執(zhí)行P(I)能返回一組PC約束。所有的φi表示基礎塊，πi表示分支約束。模型Mi是約束πi的一種可靠的解決方案，M1 = Solution(¬π1 ∧ π2)。為了發(fā)現所有的路徑，我們維護一個叫W的工作列表，它是一組M。

在***輪迭代，執(zhí)行I = R, W = ∅ 和P(I) → PC。然后是∀π ∈ PC, W = W ∪ {Solution(π)} ，再次執(zhí)行∀M ∈ W, P(M)。當模型M作為程序的輸入后，將它從列表W中刪除。重復操作知道W為空。

符號執(zhí)行的代碼覆蓋測試既有優(yōu)點又有缺點。它對于在混淆的二進制文件中很有幫助。確實利用符號覆蓋能檢測到隱藏的、不可達到的代碼但會是個平面的圖表。最糟糕的是當你的表達式太復雜，可能會超時或巨大的內存消耗(在過去，我們符號表達式在超時前消耗了差不多450 G的 RAM)。這種場景主要發(fā)生在分析超大二進制文件或者包含復雜功能的混淆的二進制文件。

三、使用Triton進行代碼覆蓋測試

從版本v0.1 build 633開始，Triton整合了我們代碼覆蓋測試需要的一切。它可以讓我們更好的處理及計算SMT2-lib表達的AST。下面我們將關注代碼覆蓋的設計和使用的算法。

1. 算法

以下面的代碼為例。

01. char *serial = "\x31\x3e\x3d\x26\x31"; 
02. int check(char *ptr) 
03. { 
04.   int i = 0; 
05.   while (i < 5){ 
06.     if (((ptr[i] - 1) ^ 0x55) != serial[i]) 
07.       return 1; 
08.     i++; 
09.   } 
10.   return 0; 
11. } 

函數控制流圖如下顯示。它是一個好例子，因為我們需要找到好的輸入才能覆蓋所有的基礎塊。

可以看到可以看到只有一個變量可控，位于地址rbp+var_18，指向argv[1]的指針。目標是通過計算約束條件和使用快照引擎到達check函數的所有基礎塊。例如到達位于地址0x4005C3基礎塊的約束條件是[rbp+var_4] > 4，但是我們不能直接控制這個變量。另一方面，在地址0x4005B0處的跳轉依賴于用戶的輸入并且這個約束條件可以通過符號執(zhí)行解決。

歸納以前的想法的算法是使用基于微軟的Fuzzer算法(SAGE)，下圖表示包含約束條件的check函數。這個start和end節(jié)點表示了我們的函數開端(0x40056D)和函數的結尾(0x4005C8)

在***執(zhí)行前，我們不知道任何的分支約束。因此我們按照上文所述，我們注入一些隨機種子來收集***個PC并且構建我們的W集合。***執(zhí)行P(I)的跟蹤結果由下圖藍色表示。

執(zhí)行結果給了我們***條路徑約束P(I) → (π0 ∧ ¬π1)。

基于***次跟蹤，我們知道發(fā)現了兩條分支(π0 ∧ ¬π1)，并且還有兩條沒有發(fā)現。為了到達基礎塊φ3，我們計算***個分支約束的否定條件。當且僅當Solution(¬π0) 是SAT，我們將它添加到模型工作列表W中。

同樣到達 φ4 可以得到W = W ∪ {Solution(π0 ∧ ¬(¬π1))}。所有解決方案都生成了并且模型被添加到工作列表中，我們執(zhí)行工作列表中每個模型。

2. 實現

執(zhí)行代碼覆蓋的一個條件是在一個跳轉指令處能預測下一條指令的地址。這是構建路徑約束的必要條件。

我們不能在一個分支指令后放置一個回調，因為RIP寄存器已經改變了。因為Triton為所有的寄存器創(chuàng)建語義表達式，所以在分支指令時可以判定RIP。

***次，我們開發(fā)了一個SMT判定器用來計算RIP，但是我們發(fā)現Pin提供的用于獲得下一個RIP值的IARG_BRANCH_TARGET_ADDR和IARG_BRANCH_TAKEN有點滯后。使用Pin計算下一個地址非常簡單，但是SMT判定器用來檢查指令的語義是很有用的。

為了更好的演示判定，我們實現了visitor pattern來將SMT的抽象語法樹(AST)轉化為Z3的抽象語法樹。這個設計能夠用于將SMT AST轉化為任意其他的表達。

Z3的AST使用Z3 API處理更加簡單。轉化代碼是src/smt2lib/z3AST.h 和 src/smt2lib/z3AST.cpp

現在我們解釋代碼覆蓋的工具如何工作。讓我們假定輸入來自命令行。

首先，我們有：

160. def run(inputSeed, entryPoint, exitPoint, whitelist = []): 
161. ... 
175. if __name__=='__main__': 
176.   TritonExecution.run("bad !", 0x400480, 0x40061B, ["main", "check"]) # crackme_xor 

在176行，我們定義了輸入種子bad!，代表程序的***個參數。然后我們給出代碼覆蓋的起始地址，在這個地址我們將做一個快照。第三個參數將匹配***一個塊，這個地址我們將恢復快照。***，我們設置一個避免庫函數、加密函數等的白名單。

134. def mainAnalysis(threadId): 
135. 
136.    print "[+] In main" 
137.    rdi = getRegValue(IDREF.REG.RDI) # argc 
138.    rsi = getRegValue(IDREF.REG.RSI) # argv 
139. 
140.    argv0_addr = getMemValue(rsi, IDREF.CPUSIZE.QWORD)      # argv[0] pointer 
141.    argv1_addr = getMemValue(rsi + 8, IDREF.CPUSIZE.QWORD)  # argv[1] pointer 
142. 
143.    print "[+] In main() we set :" 
144.    od = OrderedDict(sorted(TritonExecution.input.dataAddr.items())) 
145. 
146.    for k,v in od.iteritems(): 
147.        print "\t[0x%x] = %x %c" % (k, v, v) 
148.        setMemValue(k, IDREF.CPUSIZE.BYTE, v) 
149.        convertMemToSymVar(k, IDREF.CPUSIZE.BYTE, "addr_%d" % k) 
150. 
151.    for idx, byte in enumerate(TritonExecution.input.data): 
152.        if argv1_addr + idx not in TritonExecution.input.dataAddr: # Not overwrite the previous setting 
153.            print "\t[0x%x] = %x %c" % (argv1_addr + idx, ord(byte), ord(byte)) 
154.            setMemValue(argv1_addr + idx, IDREF.CPUSIZE.BYTE, ord(byte)) 
155.            convertMemToSymVar(argv1_addr + idx, IDREF.CPUSIZE.BYTE, "addr_%d" % idx) 

下一個執(zhí)行的代碼是mainAnalysis回調函數，我們注入一些值到輸入中(行148，154)，我們能通過符號變量覆蓋這些輸入(行149，155)。

所有被選擇的輸入存儲在全局變量TritonExecution.input中。然后我們開始代碼檢測。

58. if instruction.getAddress() == TritonExecution.entryPoint and not isSnapshotEnabled(): 
59.        print "[+] Take Snapshot" 
60.        takeSnapshot() 
61.        return 

當我們在入口點時，我們做一個快照，為了用新的輸入重新執(zhí)行代碼檢測。

52. if instruction.getAddress() == TritonExecution.entryPoint + 2: 
53.   TritonExecution.myPC = []                                  # Reset the path constraint 
54.   TritonExecutionTritonExecution.input = TritonExecution.worklist.pop()     # Take the first input 
55.   TritonExecution.inputTested.append(TritonExecution.input)  # Add this input to the tested input 
56.   return 

我們重置路徑約束(行53)，從工作列表中取出一個新的輸入。

63. if instruction.isBranch() and instruction.getRoutineName() in TritonExecution.whitelist: 
64. 
65.   addr1 = instruction.getAddress() + 2                # Address next to this one 
66.   addr2 = instruction.getOperands()[0].getValue()     # Address in the instruction condition 
67. 
68.   # [PC id, address taken, address not taken] 
69.   if instruction.isBranchTaken(): 
70.     TritonExecution.myPC.append([ripId, addr2, addr1]) 
71.   else: 
72.     TritonExecution.myPC.append([ripId, addr1, addr2]) 
73. 
74.   return 

上述代碼檢測是否位于分支指令(如jnz，jle等)或者位于白名單中的函數中。如果是，我們得到兩種可能的地址(addr1和addr2)，通過isBranchTaken()(行69)計算有效的地址。

然后，我們將條件約束存儲在RIP表達式中。

81. if instruction.getAddress() == TritonExecution.exitPoint: 
82.  print "[+] Exit point" 
83. 
84.  # SAGE algorithm 
85.  # http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf 
86.  for j in range(TritonExecution.input.bound, len(TritonExecution.myPC)): 
87.      expr = [] 
88.      for i in range(0,j): 
89.          ripId = TritonExecution.myPC[i][0] 
90.          symExp = getFullExpression(getSymExpr(ripId).getAst()) 
91.          addr = TritonExecution.myPC[i][1] 
92.          expr.append(smt2lib.smtAssert(smt2lib.equal(symExp, smt2lib.bv(addr,  64)))) 
93. 
94.      ripId = TritonExecution.myPC[j][0] 
95.      symExp = getFullExpression(getSymExpr(ripId).getAst()) 
96.      addr = TritonExecution.myPC[j][2] 
97.      expr.append(smt2lib.smtAssert(smt2lib.equal(symExp, smt2lib.bv(addr,  64)))) 
98. 
99. 
100.      expr = smt2lib.compound(expr) 
101.      model = getModel(expr) 
102. 
103.      if len(model) > 0: 
104.          newInput = TritonExecution.input 
105.          newInput.setBound(j + 1) 
106. 
107.          for k,v in model.items(): 
108.              symVar = getSymVar(k) 
109.              newInput.addDataAddress(symVar.getKindValue(), v) 
110.          print newInput.dataAddr 
111. 
112.          isPresent = False 
113. 
114.          for inp in TritonExecution.worklist: 
115.              if inp.dataAddr == newInput.dataAddr: 
116.                  isPresent = True 
117.                  break 
118.          if not isPresent: 
119.              TritonExecution.worklist.append(newInput) 
120. 
121.  # If there is input to test in the worklist, we restore the snapshot 
122.  if len(TritonExecution.worklist) > 0 and isSnapshotEnabled(): 
123.      print "[+] Restore snapshot" 
124.      restoreSnapshot() 
125. 
126.  return 

當我們在出口點是是***一步。行84-120是SAGE的實現。簡言之，我們?yōu)g覽路徑約束列表，對于每個PC，我們嘗試獲得滿足否定的模型。如果有不可靠的模型到達了新的目標塊中，我們將這個模型添加到工作列表中。一旦所有的模型被插入工作列表中，我們恢復快照并且重新執(zhí)行每個模型。

全部代碼能在這里找到，我們例子的執(zhí)行過程如下：

四、總結

盡管代碼覆蓋使用符號執(zhí)行是一個好的方法，但它是個復雜的任務。路徑遍歷意味著內存消耗，并且一些情況下要計算的表達式太過復雜。目前，判定器非常慢，判定表達式非常慢。