每天一道CTF秽荤，日積月累，期待進步瘾英！
符號執(zhí)行工具Angr在CTF中的應用
符號執(zhí)行
概念及原理介紹
符號執(zhí)行是程序分析的一種思路，可以類比解方程：我不知道該怎如何確定輸入（或感興趣的變量等）和程序執(zhí)行路徑之間的關系，但我可以把輸入設為變量x（此為“符號”）描验，然后對照紙面上的程序，每執(zhí)行一步坑鱼，我就記錄下來它執(zhí)行的條件（此為“執(zhí)行”）膘流，作為方程的一部分。如果碰到分支語句鲁沥，就分為兩個方程呼股，一個方程對應一個分支執(zhí)行條件。如此等到程序結束画恰，我就有了一堆方程彭谁，每個方程對應一個執(zhí)行路徑。想分析哪個路徑允扇，解對應的方程就行了缠局。通過這樣的分析技術则奥，就可以獲得讓特定區(qū)域執(zhí)行的輸入。
符號執(zhí)行技術是一種白盒的靜態(tài)分析技術狭园。符號執(zhí)行(symbolic execution)本身是靜態(tài)的截亦，因為它只是把具體的輸入值(input value)用符號值(symbolic value)替換踏堡，然后根據(jù)符號值的的約束條件在約束求解器(constraint solver)允許的條件下求解出滿足條件的輸入值侧漓。如果把上述最終狀態(tài)屬性替換成程序形成的bug狀態(tài)培愁，比如，存在數(shù)組越界復制的狀態(tài)绎谦，那么管闷，我們就能夠利用此技術挖掘漏洞的輸入向量了。
左邊的代碼中燥滑，testme()函數(shù)有3條執(zhí)行路徑渐北，組成了右圖中的執(zhí)行樹。直觀上來看铭拧，我們只要給出三個輸入就可以遍歷這三個路徑赃蛛，即圖中綠色的x和y取值。符號執(zhí)行的目標就是能夠生成這樣的輸入集合搀菩，在給定的時間內探索所有的路徑呕臂。
符號執(zhí)行通過維護符號狀態(tài)和路徑約束，以便在運行過程中傳遞信息肪跋。
- 符號狀態(tài)(symbolic state)：符號執(zhí)行維護一個符號狀態(tài)σ歧蒋，將變量映射到符號表達式。
- 符號路徑約束(symbolic path constraint)：符號路徑約束PC州既，它是符號表達式上無量詞的一階公式谜洽。
- 在執(zhí)行開始時，將σ初始化為一個空映射吴叶，將PC初始化為true阐虚；
- 在符號執(zhí)行過程中，σ和PC都會更新蚌卤。
- 在沿著程序執(zhí)行路徑的符號執(zhí)行結束時实束，使用約束求解器對PC進行求解，以生成具體的輸入值逊彭。 如果程序在這些具體的輸入值上執(zhí)行咸灿，它將采用與符號執(zhí)行完全相同的路徑，并以相同的方式終止侮叮。
對于樣例代碼避矢，具體的過程如下
初始化：初始化符號狀態(tài)σ為空，符號路徑約束PC為true；
在每個賦值v = e處审胸，符號執(zhí)行都通過將 v 映射到σ(e)來更新σ分尸，該映射是通過對當前符號狀態(tài)求值, 而獲得的符號表達式。 例如：
- main（）函數(shù)的前兩行（第16-17行）的符號執(zhí)行導致σ= {x ?x0歹嘹，y ? y0}，其中x0孔庭，y0是兩個初始不受約束的符號值尺上；
- 在執(zhí)行第6行之后，σ = {x ?x0圆到，y ?y0怎抛，z ? 2y0}。
對于每個條件語句：if（e） then S1 else S2芽淡。
- 在第7行之后马绝，分別創(chuàng)建了兩個符號執(zhí)行實例，分別具有路徑約束x0 = 2y0和x =? 2y0;
- 在第8行之后挣菲，分別創(chuàng)建兩個具有路徑約束的符號執(zhí)行實例（x0 = 2y0）∧（x0 > y0 + 10）和（x0 = 2y0）∧（x0 ≤ y0 + 10）富稻。
- “then”分支： PC被更新為PC ∧ σ(e)；
- “else”分支： 生成一個新的PC’, PC’被初始化為：PC∧? σ(e)白胀；
- 如果分支的狀態(tài)σ的PC可滿足椭赋，則符號執(zhí)行沿著分支繼續(xù)，否則路徑終止或杠。
例如:
如果一個符號執(zhí)行實例碰到了exit或error時哪怔，當前符號執(zhí)行實例就會被終止，并利用一個現(xiàn)成的約束求解器來生成一個可滿足當前路徑約束的賦值向抢。 例如：
- 三條路徑按照約束求解后认境，分別得到我們期望的三組輸入：{x=0, y=1}，{x=2, y=1}和{x=30, y=15}挟鸠。
若代碼中包含循環(huán)或遞歸結構叉信，且它們的終止條件是符號化的，則可能導致有無窮多條路徑兄猩。在實踐過程中茉盏，需要對路徑搜索設置一個限制，例如timeout枢冤，限制路徑數(shù)量鸠姨，循環(huán)迭代次數(shù)或探測深度。
經典的符號執(zhí)行有一個關鍵的缺點淹真，若符合執(zhí)行路徑的符號路徑約束無法使用約束求解器進行有效的求解讶迁，則無法生成輸入。
CTF_Angr
angr是一個基于python的二進制漏洞分析框架核蘸，它將以前多種分析技術集成進來巍糯，---它能夠進行動態(tài)的符號執(zhí)行分析（如啸驯，KLEE和Mayhem），也能夠進行多種靜態(tài)分析
基本思路：
①.新建一個Angr工程祟峦，并且載入二進制文件
②.創(chuàng)建程序入口點的state
③.將要求解的變量符號化
④.創(chuàng)建SimulationManager進行程序執(zhí)行管理
⑤.搜索滿足我們目標的state
⑥.求解程序執(zhí)行到state時罚斗，符號化變量所需要的約束條件
⑥.解出約束條件，獲得目標值
github: https://github.com/jakespringer/angr_ctf. 可以看到有每一個題目的文件夾（題目生成包宅楞，用來生成可執(zhí)行文件针姿，只需刷題的話大概沒用），還有dist和solutions兩個文件夾厌衙。
dist里有：
XX_xxxx：每道題的elf距淫。scaffoldXX.py：解題腳本挖空范例（題面，需要填空婶希，注釋用來解釋語句的作用很詳細）榕暇。
solutions里各道題的文件夾里有：
XX_xxxx：每道題的elf。scaffoldXX.py：解題腳本挖空范例（同上）喻杈。solveXX.py：解題腳本（正確答案=v=）彤枢。
這里面都是典型的angr使用方法，這里僅以第一個范例進行演示筒饰，剩下的可以按照相同的思路求解堂污。
0X00-angr_find
使用IDA打開dist/00_angr_find,F5轉化為偽C代碼
程序輸入password，經過complex_function函數(shù)處理龄砰，如果最終等于“JACEJGCS”就輸出Good Job盟猖。complex_fuction函數(shù)判斷了輸入的取值范圍。
本題使用傳統(tǒng)的“爆破”方法也可以解決换棚，一位一位拼出符合題意的輸入（“JXWVXRKX”）式镐。腳本如下：
str1 = "JACEJGCS"
flag = ""
def complex_function(a1,a2):
return (3 * a2 + a1 - 65) % 26 + 65
if __name__ == "__main__":
for i in range(len(str1)):
for j in range(64,90):
if ord(str1[i]) == complex_function(j,i):
flag += chr(j)
break
print(flag)
知道目標輸出，構造合適的輸入固蚤，可以使用Angr這個符號執(zhí)行工具解題娘汞。
①.新建一個Angr工程，并且載入二進制文件
path_to_binary = 'D:\WinAFL\angr_ctf\dist\00_angr_find'
project = angr.Project(path_to_binary, auto_load_libs=False)
②.創(chuàng)建程序入口點的state
state = p.factory.entry_state(add_options={angr.options.SYMBOLIC_WRITE_ADDRESSES})
③.將要求解的變量符號化
本題目中可以省略這步操作(當然也可以保留夕玩，但后面就不能用dump你弦，要用eval)，因為不是手動設置的輸入燎孟，是在程序運行時用戶任意輸入的禽作。
詳細解釋見下“注”。
u = claripy.BVS("u", 8)
initial_state.memory.store(0x080485C7, u) //main地址
④.創(chuàng)建SimulationManager進行程序執(zhí)行管理
sm = p.factory.simulation_manager(state)</pre>
⑤.搜索滿足我們目標的state
目標state是"good job", IDA中確定地址為0x8048678
print_good_address = 0x8048678
⑥.求解程序執(zhí)行到state時揩页，符號化變量所需要的約束條件
sm.explore(find=print_good_address)
⑥.解出約束條件旷偿，獲得目標值
solution_state.posix.dumps(0)代表該狀態(tài)執(zhí)行路徑的所有輸入
solution_state.posix.dumps(1)代表該狀態(tài)執(zhí)行路徑的所有輸出
if sm.found:
solution_state = sm.found[0]
print(solution_state.posix.dumps(0))
else:
raise Exception('Could not find the solution')
完整代碼見 "./angr_ctf/solutions/00_angr_find/solve00.py", 與爆破得到的結果一致。
注：本題中不是手動設置的輸入，而是程序運行過程中進行的輸入萍程，因此可以使用dump(0) dump標準輸入來得到輸入幢妄。但如果題目修改為char s1[9]="00000000",并去掉scanf，這時就要將輸入符號化茫负，使用angr求解器（solver）提供的eval函數(shù)蕉鸳，得到滿足條件的可能的輸入。
solver.eval（）函數(shù)詳細說明：
https://blog.csdn.net/doudoudouzoule/article/details/79394447
baby-re（DEFCON 2016 quals）
github：https://github.com/angr/angr-doc/tree/master/examples忍法，這里有很多例子置吓，之前已經實踐過sym_write，這次選擇一個復雜點的缔赠，defcon2016quals_baby-re，作為一道經典的CTF真題友题，《從0到1 CTFer成長之路》一書也對這個例子進行了詳細的分析嗤堰。
首先IDA打開二進制文件，F(xiàn)5查看C偽代碼度宦，了解程序邏輯踢匣。輸入13個字符，然后通過CheckSolution判斷輸入字符是否滿足約束條件戈抄。（截圖為部分程序代碼）
分析可知成功的地址是0x4028E9离唬，失敗的地址是0x402941
然后用最樸素的方式構造payload，代碼如下：
import angr
import claripy
import re
import math
proj = angr.Project('./baby-re', auto_load_libs=False)
state = proj.factory.entry_state(add_options={angr.options.SYMBOLIC_WRITE_ADDRESSES})
sm = proj.factory.simulation_manager(state)
sm.explore(find=0x4028E9, avoid=0x402941)
if sm.found:
solution_state = sm.found[0]
text = solution_state.posix.dumps(0).decode("utf-8") #bytes轉化為string
str = re.findall(r'.{%d}' % int(10), text) #每10位進行切割划鸽，asc碼轉字符串输莺，拼接組成flag
flag = ''
for i in str:
flag += (chr(int(i)))
print(flag)
else:
raise Exception('Could not find the solution')
程序輸出正確的結果，但用時較長裸诽，下面要想辦法優(yōu)化嫂用。
-
LAZY_SOLVES
在LAZY_SOLVES打開的情況下，只要路徑在基本塊的末尾分支為幾個丈冬，angr就不會主動檢查每個成功的狀態(tài)是否可以滿足嘱函。相反，angr認為他們都是可以滿足的埂蕊，并且繼續(xù)創(chuàng)造成功的路徑往弓。LAZY_SOLVES指在不運行的時候檢查當前的條件是否能夠成功到達目標位置。這樣無法避免一些無解的情況蓄氧，但是可以顯著提高腳本的運行速度函似，是在路徑爆炸（創(chuàng)建更多路徑）和花費在約束求解上的時間之間的平衡。
在早期angr版本中默認LAZY_SOLVES是開啟的喉童，它可以加快我們分析的速度缴淋，因為它不會對每個狀態(tài)都進行判斷。新版本可通過下面的語句開啟：
sm.one_active.options.add(angr.options.LAZY_SOLVES
經過實踐，時間大大縮短重抖，從449.51s降低到15.78s
-
blank_state
有些時候程序的輸入數(shù)據(jù)被分類很多組露氮，或者程序獲取輸入的邏輯實現(xiàn)的很復雜，嚴重干擾了angr分析钟沛，這時候就要跳過那些輸入指令畔规，加載程序，提高符號執(zhí)行效率恨统。創(chuàng)建
initial_state時叁扫，使用factory的blank_state方法，傳入地址畜埋，表示從該地址的狀態(tài)開始莫绣，實現(xiàn)任意位置加載程序。
state = proj.factory.blank_state(addr=0x4025E7) #main函數(shù)地址
-
hook
在scanf函數(shù)前面存在fflush函數(shù)悠鞍，它的功能是清空緩沖區(qū)对室，將輸入寫入stream。注意到在每次輸入時咖祭，都會調用printf和fflush這兩個對程序關鍵算法分析沒有幫助的函數(shù)浪費時間掩宜，因此hook這兩個函數(shù)，讓他們直接return么翰。
proj.hook_symbol('printf',angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained'](return_value=0), replace = True)
proj.hook_symbol('fflush',angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained'](return_value=0),replace = True)
優(yōu)化scanf：用自己的my_scanf()來代替__isoc99_scanf牺汤，我們在保持scanf功能不變的情況下，將我們的符號變量存儲進去浩嫌。
class my_scanf(angr.SimProcedure):
def run(self, fmt, des): # 參數(shù)為 (self + 該函數(shù)實際參數(shù))
simfd = self.state.posix.get_fd(0) # 創(chuàng)建一個標準輸入對對象
data, real_size = simfd.read_data(4) # 從標準輸入中讀取一個整數(shù)檐迟，返回值第一個是讀到的數(shù)據(jù)內容 第二個數(shù)內容長度
self.state.memory.store(des, data) # 將數(shù)據(jù)保存到相應參數(shù)內
return 1 # 返回原本函數(shù)該返回的東西
proj.hook_symbol('__isoc99_scanf', my_scanf(), replace=True)
# 這里%d對應int 是4個字節(jié) 但是讀取到一個int所以返回1 所以這完全是模擬的原來的函數(shù)
因為我們這里Scanf是要向內存寫入數(shù)據(jù)的，于是我們利用使用 state.memory.store(addr, val) 接口將數(shù)據(jù)保存到相應參數(shù)內码耐。
優(yōu)化scanf就可以達到和控制返回值類似的效果锅减，對于速度提升效果明顯，時間縮短到4.86s
-
Claripy
angr中通過claripy模塊手動構造輸入伐坏，claripy.BVS可以直接創(chuàng)建符號變量怔匣，第一個參數(shù)為變量名，第二個參數(shù)是位數(shù)桦沉，可以這樣創(chuàng)建用戶輸入每瞒，然后把這些變量保存在內存地址。
class my_scanf(angr.SimProcedure):
def run(self, fmt, ptr):
self.state.mem[ptr].dword = flag_chars[self.state.globals['scanf_count']]
self.state.globals['scanf_count'] += 1
proj.hook_symbol('__isoc99_scanf', my_scanf(), replace=True)
simulation.one_active.globals['scanf_count'] = 0
這樣程序每次調用scanf時纯露，其實就是在執(zhí)行my_scanf就會將flag_chars[i]存儲到self.state.mem[ptr]當中剿骨，這其中ptr參數(shù)，其實就是本身scanf函數(shù)傳遞進來的埠褪。為了控制下標浓利，我們設置了一個全局符號變量scanf_count記錄scanf函數(shù)的數(shù)目挤庇，存儲在state.globals里面，使得第i個scanf函數(shù)的state.mem賦值第i個符號變量贷掖。
這種優(yōu)化方式時間縮短嫡秕，效果不明顯，平均5.02s
綜合上述分析優(yōu)化苹威，完整程序代碼見./angr-doc/examples/defcon2016quals_baby-re/solve.py
參考資料
https://blog.csdn.net/doudoudouzoule/article/details/79977415
https://b0ldfrev.gitbook.io/note/symbolic_execution/angr-jin-jie
https://www.anquanke.com/post/id/214288
https://xz.aliyun.com/t/4137
https://blog.csdn.net/doudoudouzoule/article/details/79394447
https://blog.csdn.net/zhuzhuzhu22/article/details/80350441
https://www.zhihu.com/question/53533149/answer/152262963
https://www.pianshen.com/article/5473288632/
樣例來源：https://github.com/angr/angr-doc/examples/sym_write
