感謝 https://github.com/jakespringer/angr_ctf/blob/master/SymbolicExecution.pptx 這篇 PPT 和 https://www.bilibili.com/video/BV167411o7WK?t=1043 這個視頻，本文章的出現和我能入門angr，這兩個教程功不可沒，如果你們有興趣也可以看看。angr 官方項目地址：https://github.com/angr/angr
這篇文章主要是帶大家入門如何用 angr 進行符號執行。
符號執行介紹
隨着時代的發展，程序的流程越來越復雜，如果我們繼續像以前那樣在 ida 里仔細分析，肯定是太累了，所以有些科學家想要用自動化的算法來進行逆向工程，然后，他們就想到了符號執行這個算法。
符號執行算法聽起來很高端，其實內部算法卻並不難理解。接下來就介紹一下這個符號執行的內部算法：
假如有這樣一個程序
這里采用 Python 只是為了方便理解。。。事實上符號執行可以解決所有語言的程序，這個算法和程序所采用的語言沒啥關系
user_input = int(input())
if user_input - 10 >= 0:
print('Success.')
else:
print('Try again.')
我們現在想要知道為了讓程序到達 print('Success.')這一行，需要的輸入條件是什么，那我們要怎么得出到達這一行的條件呢？首先我們來看看執行這個程序的時候，user_input 都經歷了什么。
user_input 經過了一個判斷語句，其中 user_input - 10>= 0 就是成功的條件。所以很顯然，我們只要將這個不等式接出來，就能知道需要的條件了。
那么接下來假如說有一個這樣的程序呢：
user_input = int(input())
if user_input - 10 >= 0:
if user_input <= 20:
print('Success.')
else:
print('Try again.')
else:
print('Try again.')
這個程序稍微復雜了那么一點。但是這不是問題，我們照着解決上一個程序的方法，先看看 user_input 都經歷了什么：
不難看出，user_input經歷了個兩個判斷條件，所以這回我們為了得出輸出成功的條件，我們得解一個方程組：
然后我們只要愉快的解出這個不等式組，就可以得到可能的輸出了。
不難發現，就算你if語句再多，只要我能夠一個個收集齊全，然后將這些條件形成一個不等式組，然后解出這個不等式組，就可以得到我們想要的輸出了。
但是現實生活中的程序不可能這么簡單，單憑人力是無法收集全的，那么我們自然是要用程序來收集。這個時候就該我們的angr登場了。
接下來我們通過一個程序來看看angr的使用方法和大概的工作流程。
angr 的安裝
在用之前，我們得先安裝這個東西。安裝這個十分的簡單，為了避免 python 庫版本混亂的問題。我們在使用這個庫之前將這個庫裝進 python 虛擬環境里隔離起來。如何建立虛擬環境這個可以自行百度，畢竟這屬於python的基礎知識。建立好以后，我們在終端中激活這個虛擬環境，然后用 pip3 install angr 安裝 angr即可。
angr 上手教程
樣例程序下載：
百度網盤鏈接: https://pan.baidu.com/s/1tdL3RmAm9VZz5wsR-IGA6g 密碼: 6tf2
Github 鏈接: https://github.com/jakespringer/angr_ctf/blob/master/dist/00_angr_find
由於這個程序比較簡單，因此我們這次用 ipython 來操作。（沒裝的自己百度哦）
首先進入 python 虛擬環境的 ipython，然后我們 import angr，如果沒有問題，那就是安裝好了。如果有報錯，建議自行百度。其實 angr 官方有一個打包好的 docker 鏡像，如果本機因為各種問題沒法正常使用，就用這個docker環境吧。
接下來我們要新建一個 angr 工程：
>>> proj = angr.Project('程序的路徑') # 相對路徑和絕對路徑均可
接下來我們就要新建一個模擬運行管理器，然后讓angr搜索需要的分支信息。
>>> sm = proj.factory.simulation_manager()
>>> sm = sm.explore(find=0x08048675) # 探索到達 0x08048678 的路徑
其中 factory 這個對象是用來生成和項目有關的一些分析工具，然后我們用這個對象生成了一個SimulationManager對象，存儲在變量 sm 中。那么什么是模擬運行管理器呢。那就要涉及到angr是如何收集所有的分支信息了。
用過 ida 的人，應該都相當熟悉這個畫面
可以說，這個圖中的一個個代碼塊就是 angr 框架中所謂的 state（這只是方便說明的說辭，實際上angr的一個state還存儲了執行這個代碼塊后的寄存器狀態，內存狀態等信息），這一個一個state組合在一起，就形成了執行路徑，然后我們用 SimulationManager 來生成，管理執行路徑。
然后 angr 會將入口點那塊 state 作為起點，將find的值對應的那塊匯編代碼作為終點，進行寬度優先搜索（還是要了解一下這個算法，這樣才能理解其他的一些參數設置，如avoid參數的含義）。找到一條從起點到達終點的可行路徑，然后將這條路上的所有if條件收集起來。最后自動對收集起來的條件形成的不等式組進行求解。（貌似具體的方法較為復雜，這里可以稍微這樣簡單理解一下）
其實我們還可以用 proj.factory.entry_state()來生成一個關於該程序入口點的state。然后將這個state作為proj.factory.simulation_manager()的參數，實際上proj.factory.simulation_manager()的默認參數就是proj.factory.entry_state()所以我就不手動指定了。
如果這步執行結束了，那么我們就可以導出能夠讓程序到達成功狀態的輸入了，
>>> final_state = sm.found[0] # 0 代表找到的第一個結果
>>> final_state.posix.dumps(0) # 導出結果
其中 posix 表示終點狀態中存儲的系統接口信息，然后通過dumps函數來導出系統輸入，系統輸出等信息。
final_state.posix.dumps(0) 表示導出輸入，final_state.posix.dumps(1)表示導出輸出。
然后我們就可以找到angr爆破出來的輸出 b'JXWVXRKX'。
如何進階
1: 學習一下寬度優先搜索。
2: https://github.com/jakespringer/angr_ctf 這個項目的 dist 文件夾中存着難度從易到難的題目。完成這些水平就會有不小的提升。
3: https://space.bilibili.com/386563875 這個 UP 有關於上面這個題庫的題解視頻，上面的這些題目完全沒必要自己先做，可以先看一下這個 UP 如何操作，然后在吸收 angr 的不同用法。