符號執行-基於python的二進制分析框架angr

轉載：All Right

符號執行概述

在學習這個框架之前首先要知道符號執行。
符號執行技術使用符號值代替數字值執行程序，得到的變量的值是由輸入變 量的符號值和常量組成的表達式。符號執行技術首先由King在1976年提出 ，經過三十多年的發展，現在仍然被廣泛研究，它在軟件測試和程序驗證中發揮着重 要作用。符號執行是一種重要的形式化方法和靜態分析技術，它使用數學和邏輯 首先定義一些基本概念。程序的路徑（path）是程序的一個語句序列，這個 語句序列包括程序的一些順序的代碼片段，代碼片段之間的連接是由於分支語句 導致的控制轉移。一個路徑是可行的（feasible），是指存在程序輸入變量的至少一組值，如果以這組值作為輸入，程序將沿着這條路徑執行。否則，路徑就是不 可行的（infeasible）。路徑條件（path condition,PC）是針對一個路徑的，它是一 個關於程序輸入變量的符號值的約束，一組輸入值使得程序沿着這條路徑執行當 且僅當這組輸入值滿足這條路徑的路徑條件。具體看這里，鏈接

angr框架介紹

在二進制代碼中尋找並且利用漏洞是一項非常具有挑戰性的工作，它的挑戰性主要在於人工很難直觀的看出二進制代碼中的數據結構、控制流信息等。angr是一個基於python的二進制漏洞分析框架，它將以前多種分析技術集成進來，方便后續的安全研究人員的開發。­­­它能夠進行動態的符號執行分析（如，KLEE和Mayhem），也能夠進行多種靜態分析。
當然這款工具在CTF中的運用還是比較火的，在一些國際比賽中經常會看到它所帶來的神奇之處，比如下面我們將要講的的DEFCON CTF Qualifier 2016 baby-re這道題它僅僅用了10min就完成看了自動化分析拿到了flag。angr的github地址為，鏈接

angr的安裝

理論上來說angr目前支持linux、windows、MAC多個平台。但是支持的最好的還是linux平台。Windows平台下由於相關的依賴庫文件較難安裝，因此不太建議在windows上安裝。
接下來我們介紹一下ubuntu上的安裝。

• 安裝獨立python虛擬環境，virtualenvwrapper是一個python的虛擬環境，使用這個的主要原因是angr會對於libz3 or libVEX產生修改，為了防止對已經安裝的庫的修改而影響到到之后其他程序的使用，使用一個python的虛擬機環境是一個不錯的選擇。

  1	sudo apt-get install python-dev libffi-dev build-essential virtualenvwrapper

此時virtualenvwrapper就可以使用了,常用命令如下：

1. 列出虛擬環境列表:workon，也可以使用：lsvirtualenv
2. 新建虛擬環境:mkvirtualenv [虛擬環境名稱]
3. 啟動/切換虛擬環境:workon [虛擬環境名稱]
4. 刪除虛擬環境:rmvirtualenv [虛擬環境名稱]
5. 離開虛擬環境:deactivate

• 接着angr安裝

1	pip install angr

安裝好以后我們啟動虛擬環境，進入虛擬的python庫后就可以載入angr庫了

1 2 3 4 5 6

longlong@ubuntu:~/examples/defcon2016quals_baby-re_0$ workon angr (angr) longlong@ubuntu:~/examples/defcon2016quals_baby-re_0$ python Python 2.7.6 (default, Oct 26 2016, 20:30:19) [GCC 4.8.4] on linux2 Type "help", "copyright", "credits" or "license" for more information. >>> import angr

 

angr的使用之簡單例子一

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44

#include <stdio.h> #include <string.h> #include <unistd.h> #include <fcntl.h> #include <stdlib.h> char *sneaky = "SOSNEAKY"; int authenticate(char *username, char *password) { char stored_pw[9]; stored_pw[ 8] = 0; int pwfile; // evil back d00r if (strcmp(password, sneaky) == 0) return 1; pwfile = open(username, O_RDONLY); read(pwfile, stored_pw, 8); if (strcmp(password, stored_pw) == 0) return 1; return 0; } int accepted() { printf("Welcome to the admin console, trusted user!\n"); } int rejected() { printf("Go away!"); exit(1); } int main(int argc, char **argv) { char username[9]; char password[9]; int authed; username[ 8] = 0; password[ 8] = 0; printf("Username: \n"); read( 0, username, 8); read( 0, &authed, 1); printf("Password: \n"); read( 0, password, 8); read( 0, &authed, 1); authed = authenticate(username, password); if (authed) accepted(); else rejected(); }

這個程序的邏輯很簡單，樣例程序的功能就是讓你輸入用戶名和密碼，然后authenticate函數會進行檢驗，如果失敗就顯示Go away，反之就顯示認證成功。
接下來我們用angr編寫利用腳本

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25

#!/usr/bin/env python #_*_ coding:utf-8 _*_ import angr   def basic_symbolic_execution(): p = angr.Project( 'fauxware') #新建一個angr的工程，括號中是目標二進制程序的路徑 state = p.factory.entry_state() #接着新建一個SimState的對象 path = p.factory.path(state) #使用factory.path這個容器獲取state的起點path對象 pathgroup = p.factory.path_group(path) #根據前面獲取的函數入口點的path對象，利用path_group容器獲取沿着path開端下面將會執行的path列表 pathgroup.step(until= lambda lpg: len(lpg.active) > 1)#接下來就讓pathgroup對象一直執行下去，直到執行到可選擇的路徑個數大於一個，即產生選擇分支的時候，再停止。 #對應在上述的簡單程序中authenticate函數的 if (strcmp(password, sneaky) == 0)這個條件判斷語句     input_0 = pathgroup.active[ 0].state.posix.dumps(0) #dump出所有分支的內容，看看哪個答案應該是最可能的 input_1 = pathgroup.active[ 1].state.posix.dumps(0)   if 'SOSNEAKY' in input_0: return input_0 else: return input_1   def test(): pass if __name__ == '__main__': print basic_symbolic_execution()

 

結果如下：

1 2 3

(angr) longlong@ubuntu:~/examples/fauxware$ python solve.py SOSNEAKY (angr) longlong@ubuntu:~/examples/fauxware$

 

angr的使用之簡單例子二（CTF題）

這道題是DEFCON CTF Qualifier 2016 baby-re0，在打開二進制可執行文件后，我們向下移動到主要的底部，看到0x4028e7有兩條非常明顯的路徑，一條路徑是0x402941，打印出錯誤。另一條是0x4028e9，將會打印出flag。但是這個程序的中間有大量的繁瑣的指令，看的人眼花繚亂，接下來我們用angr解決這個問題。

腳本如下：

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18

#!/usr/bin/env python2 #_*_ coding:UTF-8 _*_ import angr   def main(): proj = angr.Project( './baby-re', load_options={'auto_load_libs': False})   path_group = proj.factory.path_group(threads= 4) # 設置了四個線程，對於這個程序線程再多了沒意義   # 如果是0x40294b就執行，如果是0x402941就不去執行 path_group.explore(find= 0x40294b, avoid=0x402941) # flag在0x40292c的位置 print path_group.found[0].state.posix.dumps(0) return path_group.found[0].state.posix.dumps(1) # dumps出flag     if __name__ == '__main__': print(repr(main()))

 

結果如下：

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17

(angr) longlong@ubuntu:~/examples/defcon2016quals_baby-re_0$ python solve.py WARNING | 2017-04-09 16:34:11,976 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2017-04-09 16:34:14,865 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2017-04-09 16:34:19,274 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2017-04-09 16:34:26,447 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2017-04-09 16:34:38,414 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2017-04-09 16:34:58,141 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2017-04-09 16:35:24,905 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2017-04-09 16:36:00,673 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2017-04-09 16:36:45,998 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2017-04-09 16:37:48,193 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2017-04-09 16:39:20,551 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2017-04-09 16:41:20,080 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2017-04-09 16:44:18,468 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. +000000077+000000097+000000116+000000104+000000032+000000105+000000115+000000032+000000104+000000097+000000114+000000100+000000033B 'Var[0]: Var[1]: Var[2]: Var[3]: Var[4]: Var[5]: Var[6]: Var[7]: Var[8]: Var[9]: Var[10]: Var[11]: Var[12]: The flag is: Math is hard!\n' (angr) longlong@ubuntu:~/examples/defcon2016quals_baby-re_0$

 

大概10min后我們得到的flag 是Math is hard!