閱讀969 返回首頁    go 阿裏雲 go 技術社區[雲棲]

符號執行：利用Angr進行簡單CTF逆向分析

一、符號執行概括

簡單的來說，符號執行就是在運行程序時，用符號來替代真實值。符號執行相較於真實值執行的優點在於，當使用真實值執行程序時，我們能夠遍曆的程序路徑隻有一條，而使用符號進行執行時，由於符號是可變的，我們就可以利用這一特性，盡可能的將程序的每一條路徑遍曆，這樣的話，必定存在至少一條能夠輸出正確結果的分支，每一條分支的結果都可以表示為一個離散關係式，使用約束求解引擎即可分析出正確結果，這就是符號執行的簡單闡述。

符號執行：利用Angr進行簡單CTF逆向分析

Angr是一個利用python開發的二進製程序分析框架，我們可以利用這個工具嚐試對一些CTF題目進行符號執行來找到正確的解答，即flag。當然，要注意的是符號執行的路徑選擇問題到現在依舊是一個很大的問題，換句話說也就是當我們的程序存在循環時，因為符號執行會盡量遍曆所有的路徑，所以每次循環之後會形成至少兩個分支，當循環的次數足夠多時，就會造成路徑爆炸，整個機器的內存會被耗盡。

二、Angr使用

個人感覺Angr在求解REVERSE題目時很有用，但在處理PWN題目時，多用在一些輔助的位置，比如尋找 strcmp 等敏感的函數等，這次我們簡單的講解一下如何使用Angr進行REVERSE題目的分析求解。我首先講解一下Angr在實踐中的幾步關鍵操作，之後會使用一個簡單的CTF題目進行實踐。推薦大家使用ipython進行簡單的實踐，ipython的tab補全可以讓你看到Angr中很多奇妙的函數。

1. 運行程序

我們在得到一個程序時，首先需要對此程序創建一個Angr工程。



  1. 
p = angr.Project(‘program’) 


我們可以通過這個工程得到程序的一些信息，比如程序名p.filename等等。


然後需要將這個程序運行起來，並且處理程序的一些輸入，前麵已經說過，在符號執行時，我們使用的並不是真實值，而是一個個符號，可以簡單的理解為變量，所以我們需要構造一個Angr中的符號來當做程序的輸入。


(1) 命令行參數


當程序要求命令行參數時，我們首先需要使用claripy這個模塊來定義抽象的數據。




  1. import claripy 


claripy的BVS函數可以創建一個指定長度的抽象數據，BVS函數要求兩個參數，第一個參數為變量名，第二個參數為變量長度。




    

  1. 
argv = [p.filename,]  
    2. 

  2. 
arg = claripy.BVS(‘arg1′, 8)argv.append(arg1) 
    3. 



這樣，我們就創建好了一個命令行參數，我們現在可以將程序運行到程序入口處，並獲得當前的一個狀態。




  1. 
state = p.factory.entry_state(args=argv) 


P.factory是工廠函數的一個集合，在這裏麵可以調用各種各樣的函數來進行符號執行，其中entry_state()函數接收一個list作為程序的命令行參數並且返回程序入口的狀態(這個狀態將在2.2節講解)。


(2) 標準輸入


當程序需要從標準輸入處讀取數據時，需要使用read_from()函數，要注意，這個函數位於狀態中，並且我們可以對輸入進行一些約束以減少符號執行遍曆的路徑。




    

  1. for _ in xrange(5):   
    2. 

  2.     k = state.posix.files[0].read_from(1) 
    3. 

  3.     state.se.add(k!=10) 
    4. 



這表示我們從標準輸入讀入了5個字節，並且每個字節都不為換行符。


2. Angr中程序的幾種狀態


我們在之前提到了獲取程序入口點的狀態，狀態在Angr中表示著程序符號執行後的幾種結果，在Angr中，當獲取到程序入口點的狀態後，我們需要使用Angr的Simgr模擬器來進行符號執行




  1. 
sm = p.factory.simgr(state) 


表示從入口點出創建一個模擬器來進行符號執行。


在 Angr 尋找路徑時，程序的當前狀態有多種表示。


    

  • step()表示向下執行一個block(42bytes)，step()函數產生active狀態，表示該分支在執行中;
    • 

  • run()表示運行到結束，run()函數產生deadended狀態，表示分支結束;
    • 

  • explore()可以對地址進行限製以減少符號執行遍曆的路徑。例如
    • 

  • sm.explore(find=0x400676,avoid=[0x40073d])
    • 

  • explore()產生found狀態，表示探索的結果等等
    • 



3. 獲取輸出


當符號執行遍曆玩路徑後，會產生大量的狀態，我們則需要從這些狀態中找出我們所需要的一條路徑。


我們可以獲取當前狀態程序的輸出




  1. print sm.found.posix.dumps(1) 


命令行參數




  1. print sm.found.solver.eval(arg1,cast_to = str) 


標準輸入




    

  1. 
inp = sm.found.posix.files[0].all_bytes()   
    2. 

  2. print sm.found.solver.eval(inp,cast_to = str)z 
    3. 



在求解命令行參數和標準輸入的值時，我們使用了約束求解引擎來進行求解


3. Angr實踐


bin(re50)下載：


https://oj.xctf.org.cn/web/practice/defensetrain/465f6bb8f4ad4d65a70cce2bd69dfacf/


腳本編寫




    

  1. import angr 
    2. 

  2. import sys 
    3. 

  3. print "[*]start------------------------------------" 
    4. 

  4. 
p = angr.Project(sys.argv[1])  # 建立工程初始化二進製文件 
    5. 

  5. 
state = p.factory.entry_state() # 獲取入口點處狀態 
    6. 

  6.   
    7. 

  7. ''' 
    8. 

  8. state.posix.files[0].read_from(1)表示從標準輸入讀取一個字節 
    9. 

  9. ''' 
    10. 

  10.   
    11. 

  11. for _ in xrange(int(sys.argv[2])):  # 對輸入進行簡單約束（不為回車） 
    12. 

  12.     k = state.posix.files[0].read_from(1) 
    13. 

  13.     state.se.add(k!=10) 
    14. 

  14.   
    15. 

  15. 
k = state.posix.files[0].read_from(1) 
    16. 

  16. state.se.add(k==10)  # 回車為結束符 
    17. 

  17.   
    18. 

  18. state.posix.files[0].seek(0) 
    19. 

  19. state.posix.files[0].length = int(sys.argv[2])+1 # 約束輸入長度（大於實際長度也可） 
    20. 

  20.   
    21. 

  21. print "[*]simgr start-------------------------------" 
    22. 

  22.   
    23. 

  23. 
sm = p.factory.simgr(state)   # 初始化進程模擬器 
    24. 

  24. sm.explore(find=lambda s:"correct!" in s.posix.dumps(1)) # 尋找運行過程中存在 “correct！”的路徑，並丟棄其他路徑 
    25. 

  25. print "[*]program excuted---------------------------" 
    26. 

  26.   
    27. 

  27. for pp in sm.found: 
    28. 

  28.     out = pp.posix.dumps(1)   # 表示程序的輸出 
    29. 

  29.     print out 
    30. 

  30.     inp = pp.posix.files[0].all_bytes()  # 取輸入的變量 
    31. 

  31.     print pp.solver.eval(inp,cast_to = str)  # 利用約束求解引擎求解輸入 
    32. 



運行




    

  1. root@kali:~# python re50.py ppp 4 
    2. 

  2. [*]start------------------------------------ 
    3. 

  3. /usr/local/lib/python2.7/dist-packages/cle/loader.py:729: UnicodeWarning: Unicode equal comparison failed to convert both arguments to Unicode - interpreting them as being unequal 
    4. 

  4.   if ilibname.strip('.0123456789') == spec.strip('.0123456789'): 
    5. 

  5. [*]simgr start------------------------------- 
    6. 

  6. [*]program excuted--------------------------- 
    7. 

  7. please input the key:correct! 
    8. 

  8.   
    9. 

  9. 9563 
    10. 

  10.   
    11. 

  11. root@kali:~# 
    12. 



我們就得到了正確的key值 9563





本文作者：hellowuzekai


來源：51CTO


最後更新：2017-11-02 15:34:27
  上一篇：go  解析阻止機器學習的十種網絡攻擊 
  下一篇：go  物聯網的應用會讓黑客掌控一切嗎？