淺談angr的緩解狀態爆炸策略 - 網安 - 專業的網絡安全產業、社區、知識平臺

前言

angr是有名的符號執行工具。眾所周知，符號執行最大的問題就是狀態爆炸。因此，angr中也內置了很多緩解符號執行的策略。本文主要介紹angr里的一些內置機制是如何緩解狀態爆炸的。

概述

據我對angr的了解，angr緩解狀態爆炸的策略約有以下幾種：

（1）simProcedure：重寫一些可能導致狀態爆炸的函數。

（2）veritesting：動態符號執行和靜態符號執行的結合

（3）Lazy Solve：跳過不必要的函數

（4）Symbion：具體執行和符號執行的結合

simProcedure

為了使得符號執行實踐性更強，angr用python寫的summary替換了庫函數。這些summary成為Simprocedures。Simprocedures可以緩解路徑爆炸，反過來也可能引入路徑爆炸。比如，strlen的參數是符號字符串。

但是，angr的simprocedure并不完善。如果angr出現了預期以外的行為，可能是由于不完整的simprocedure導致的。為此，官網給出了幾種解決方案：

（1）禁用simprocedure（雖然也有可能引入路徑爆炸，需要限制下函數的輸入）

（2）寫一個hook來代替其中的幾個simprocedure

（3）修復simprocedure

下面介紹一個simprocedure的例子

from angr import Project,SimProcedureproject = Project("example/fauxware/fauxware")class BugFree(SimProcedure):    def run(self,argc,argv):        print("Program running with argc=%s and argv=%s" %(argc,argv))        return 0# 將二進制中的main函數替換為bug free函數project.hook_symbol("main",BugFree())simgr = project.factory.simulation_manager()simgr.run()

當程序執行到main函數時，會去執行BugFree函數，就只會打印一個信息，然后返回。

當進入函數時，參數的值會從哪里進來呢？不管有多少個參數，只要定義個run函數，simprocedure就通過調用約定，自動地提取程序狀態里的參數給你。返回值也是一樣的，run函數的返回值也會通過調用約定放到狀態里的。

事實上，最經常使用simprocedure的地方是用來替換庫函數。

關于數據類型，你可能會發現run函數打印出了SAO BV64 0xSTUFF的類。這個是SimActionObject。這個只是bitvector的wrapper。他會在simprocedure里追蹤。（在靜態分析里很有用）

另外，也許你還會注意到run函數返回的是python的int 0，這個會被自動處理為word大小的bitvector。你可以返回一個普通的數字或者一個SimActionObject。

當你想要去寫一個procedure去處理浮點數時，你需要手動指定調用約定。只需要為hook提供一個cc（調用約定）。

cc = project.factory.cc_from_arg_kinds((True,True),ret_fp=True)project.hook(address, ProcedureClass(cc=mycc))

如何退出SimProcedure呢？我們已經知道了最簡單的方法去做這個，就是從run函數返回。實際上，從run函數返回是調用了self.ret(value)。self.ret()是一個知道如何從一個函數返回的函數。

SimProcedures可使用許多不同的函數：

ret(expr)：從函數返回
jump(addr)：跳到二進制中的地址
exit(code)：終止程序
call(addr,args,continue_at)：在二進制中調用
inline_call(procedure,*args):調用SimProcedure（inline）并返回結果

如果要在SimProcedure加個條件分支的話，需要直接在SimSuccessors那邊的節點上添加。

self.successors.add_successor(state,addr,guard,jumpkind)

如果我們調用二進制中的一個函數，并且在SimProcedure后重新執行呢？有個叫SimProcedure Continuation的框架可以實現這個。當你使用self.call(addr,args,continue_at) ，其中addr是你需要call的地址，args是需要調用的函數的參數的元組，continue_at是另外一個simProcedure的方法。

下面來看看一個例子，這個例子是將所有共享庫初始化的例子，來實現一個full_init_state。initializers是一個初始化隊列。每次從里頭去一個共享庫的地址，然后執行self.call。如果初始化隊列為空，則跳轉到程序的entry執行。

class LinuxLoader(angr.SimProcedure):    NO_RET = True    IS_FUNCTION = True    local_vars = ('initializers',)
    def run(self):        self.initializers = self.project.loader.initializers        self.run_initializer()
    def run_initializer(self):        if len(self.initializers) == 0:            self.project._simos.set_entry_register_values(self.state)            self.jump(self.project.entry)        else:            addr = self.initializers[0]            self.initializers = self.initializers[1:]            self.call(addr, (self.state.posix.argc, self.state.posix.argv, self.state.posix.environ), 'run_initializer')

hook symbols，可以使用符號表直接來進行hook。比如，要替換rand函數為一個具體的列表值，可以用以下代碼實現。

>>> class NotVeryRand(SimProcedure):...     def run(self, return_values=None):...         rand_idx = self.state.globals.get('rand_idx', 0) % len(return_values)...         out = return_values[rand_idx]...         self.state.globals['rand_idx'] = rand_idx + 1...         return out
>>> project.hook_symbol('rand', NotVeryRand(return_values=[413, 612, 1025, 1111]))

user hooks，除了hook 庫函數以外，也可以hook二進制中的普通函數。例子如下，0x1234是函數的地址。length參數控制程序的控制流。在函數執行完這個例子后，下一步就是從hooked的地址的5個字節后面開始執行。

>>> @project.hook(0x1234, length=5)... def set_rax(state):...     state.regs.rax = 1

Veritesting

Veritesting方法來源于論文Enhancing Symbolic Execution with veritesting，論文作者是mayhem的團隊。

論文鏈接見此：https://dl.acm.org/doi/pdf/10.1145/2927924

AngrCTF的第12個挑戰，就是關于如何使用angr的veritesting模式來緩解路徑爆炸。只需要在新建simulation_manager對象時，加上veritesting的參數就可以了。

simulation = project.factory.simgr(initial_state, veritesting=True)

簡單說下這個veritesting的原理。

從高層面來說，有兩種符號執行，一種是動態符號執行（Dynamic Symbolic Execution，簡稱DSE），另一種是靜態符號執行（Static Symbolic Execution，簡稱SSE）。動態符號執行會去執行程序然后為每一條路徑生成一個表達式。而靜態符號執行將程序轉換為表達式，每個表達式都表示任意條路徑的屬性。基于路徑的DSE在生成表達式上引入了很多的開銷，然而生成的表達式很容易求解。而SSE雖然生成表達式容易，但是表達式難求解。veritesting就是在這二者中做權衡，使得能夠在引入低開銷的同時，生成較易求解的表達式。

先來看個簡單的例子，下面的7行代碼中，有著2^100次條可能的執行路徑。每條路徑都要DSE單獨地去分析，從而使得實現100%的覆蓋率是不太現實的。實際上，只要兩個測試樣例，就可以達到100%的路徑覆蓋率。一個包含75個B的字符串和一個沒有B的字符串。然而，在2的100次方狀態空間里找到這兩個測試樣例是很難的。

veritest只要47s就能到達bug函數，而其他的符號執行工具比如klee，S2E，Mayhem使用狀態合并的策略跑1個小時，都沒跑完。Veritest從DSE開始，一旦遇到一些簡單的代碼，就切換到SSE的模式。簡單的代碼指的是不含系統調用，間接跳轉或者其他很難精確推斷的語句。在SSE模式下，首先動態恢復控制流圖，找到SSE容易分析的語句和難以分析的語句。然后SSE算法推斷出從易分析的節點到難分析節點路徑的影響。最后，Veritesting切換回DSE模式去處理靜態不好解決的情況。

lazy

這個思路有點像chopped symbolic execution論文里提到的。論文地址：https://dl.acm.org/doi/abs/10.1145/3180155.3180251

論文里是在klee實現的，開源于：https://github.com/davidtr1037/chopper

在angr里也有類似的操作，只需要設置狀態為LAZY_SOLVES就可以了。

s = proj.factory.entry_state(add_options={angr.options.LAZY_SOLVES})

依然簡單說下原理。拿論文中的例子，下面的程序是libtasn1庫里的代碼片段。第8行的get_length()函數會導致堆溢出。整體是一個while循環。這個函數會去用get_length去獲取當前數據的長度。get_length函數會去掃描輸入字符串，并且轉為ASN.1 域。然后注意14行，會去遞歸地迭代執行。或者觸發第11行的append_value函數。這個函數會在AST上創建節點。然后還會去多次掃描輸入的字符串，檢查多次元素，并分配內存給節點。這里會產生狀態爆炸主要是由于多次的嵌套調用，只符號執行函數get_length(get_length的參數為長度為n的字符串)，會導致4*n條不同路徑。函數append_value會調用多次求解器，同樣也會影響符號執行引擎的效率。最后導致無法發現第8行的堆溢出漏洞。

lazy solves就是應對這種情況而誕生的。它的核心思想是執行過程中的大部分函數和漏洞實際上并不相關。就好比這個程序里，漏洞是由于21行的剩下字節的錯誤更新導致當調用get_length時會有內存越界讀。也就是說這個bug很構造ASN.1表示的那些函數沒啥關系（比如append_value）。因此，我們可以快速的跳過這些不相關的函數。

Lazy Solves策略實際上是在符號執行過程中先跳過函數調用。如果遇到的漏洞點和前面的函數有依賴關系，再會去求解相關的函數的依賴。由于漏洞只和一小部分函數有關聯，所以這種策略在一定程度上緩解了狀態爆炸。

Symbion

Symbion來自論文：SYMBION: Interleaving Symbolic with Concrete Execution

他的核心思想主要是在具體執行和符號執行相互切換的一個過程。他的應用場景特別適合：假設只需要符號執行一個程序的特定函數，但是到這個函數前有很多初始化的步驟想要跳過。因為這些步驟和分析無關或者angr不能很合適地模擬。比如，程序是運行在一個嵌入式系統上，而你有訪問debug接口的權限，但不太容易復現硬件的環境。

這里的例子是angr博客里的，下面的代碼有四個惡意行為。所有這些行為依賴于硬編碼的配置。我們可以在地址0x400cd6看到配置的使用方法：二進制里第一個做決定的點。

我們的目標是要去分析二進制的惡意行為以及如何觸發它們。我們可以看到第二個payload在基本塊400d6a處，我們如何到達它？還有基本塊0x400d99呢？這就是符號執行要做的事情。

思路是讓binary自動unpack，并且具體執行到0x400cd6的地方，然后同步狀態到angr，然后定義一個符號變量，去符號化探索后面的程序。

然而，這個二進制是packed的，并且內存會被unpacking 進程覆蓋。軟件的斷點都會被覆蓋。所以我們手動逆向二進制，并且確定了我們可以從程序的開始運行到0x85b853，to have a new stub available at 0x45b97f。最終就等待4個斷點在那個地址命中，我們就可以獲取在400cd6的unpacked code了。

下面的代碼是官方給出的示例。我也試著跑了一下，但由于avatar2和某些angr的庫不兼容，最后跑出來的結果和github里的某個issue一樣。

import subprocessimport osimport noseimport avatar2 as avatar2
import angrimport claripyfrom angr_targets import AvatarGDBConcreteTarget
# First set everything upbinary_x64 = os.path.join(os.path.dirname(os.path.realpath(__file__)),                                          os.path.join('..', '..', 'binaries',                                          'tests','x86_64',                                          'packed_elf64'))
# Spawning of the gdbserver analysis environment(這里GDB_SERVER_IP和PORT應該要自己設置)print("gdbserver %s:%s %s" % (GDB_SERVER_IP,GDB_SERVER_PORT,binary_x64))subprocess.Popen("gdbserver %s:%s %s" % (GDB_SERVER_IP,GDB_SERVER_PORT,binary_x64),                  stdout=subprocess.PIPE,                  stderr=subprocess.PIPE,                  shell=True)
# Instantiation of the AvatarGDBConcreteTargetavatar_gdb = AvatarGDBConcreteTarget(avatar2.archs.x86.X86_64,                                     GDB_SERVER_IP, GDB_SERVER_PORT)
# Creation of the project with the new attributes 'concrete_target'p = angr.Project(binary_x64, concrete_target=avatar_gdb,                             use_sim_procedures=True)# 從entry開始使用具體執行entry_state = p.factory.entry_state()entry_state.options.add(angr.options.SYMBION_SYNC_CLE)entry_state.options.add(angr.options.SYMBION_KEEP_STUBS_ON_SYNC)
simgr = p.factory.simgr(state)
## Now, let's the binary unpack itself（concrete execution）simgr.use_technique(angr.exploration_techniques.Symbion(find=[0x85b853]))exploration = simgr.run()new_concrete_state = exploration.stashes['found'][0]
# 為啥這樣可以找到unpack code ？confusing# Hit the new stub 4 times before having our unpacked code at 0x400cd6for i in xrange(0,4):    simgr = p.factory.simgr(new_concrete_state)    simgr.use_technique(angr.exploration_techniques.Symbion(find=[0x85b853]))    exploration = simgr.run()    new_concrete_state = exploration.stashes['found'][0]
## Reaching the first decision point#獲取了unpack code后，開始去找符號執行開始的地方simgr = p.factory.simgr(new_concrete_state)simgr.use_technique(angr.exploration_techniques.Symbion(find=[0x400cd6])exploration = simgr.run()new_concrete_state = exploration.stashes['found'][0]# 定義符號化的參數，并把符號化的變量存到相應的內存區域# Declaring a symbolic bufferarg0 = claripy.BVS('arg0', 8*32)
# The address of the symbolic buffer would be the one of the# hardcoded malware configurationsymbolic_buffer_address = new_concrete_state.regs.rbp-0xc0
# Setting the symbolic buffer in memory!new_concrete_state.memory.store(symbolic_buffer_address, arg0) simgr = p.factory.simgr(new_concrete_state)
print("[2]Symbolically executing binary to find dropping of second stage" +       "[ address:  " + hex(DROP_STAGE2_V2) + " ]")# 符號執行# Symbolically explore the malware to find a specific behavior by avoiding# evasive behaviorsexploration = simgr.explore(find=DROP_STAGE2_V2, avoid=[DROP_STAGE2_V1,                                                       VENV_DETECTED, FAKE_CC ])# Get our synchronized state back!new_symbolic_state = exploration.stashes['found'][0] print("[3]Executing binary concretely with solution found until the end " +hex(BINARY_EXECUTION_END))
simgr = p.factory.simgr(new_symbolic_state)# 具體執行到結尾# Concretizing the solution to reach the interesting behavior in the memory# of the concrete process and resume until the end of the execution.simgr.use_technique(angr.exploration_techniques.Symbion(find=[BINARY_EXECUTION_END],                              memory_concretize = [(symbolic_buffer_address,arg0)],                               register_concretize=[]))
exploration = simgr.run()# 求解的結果new_concrete_state = exploration.stashes['found'][0]

總的來說，代碼可以劃分為以下幾個步驟：

（1）從entry開始具體執行到0x85b853。（困惑這里的0x85b853是啥？）

（2）連續具體執行四次，終點依然是0x85b853（獲取unpacked code？）

（3）具體執行到0x400dc6（決策點的位置）

（4）從0x400dc6開始符號執行到DROP_STAGE2_V2

（5）再具體執行到結尾，同時把符號化的地址具體化。

總結

angr里可能還有其他緩解狀態爆炸的思路，比如driller，這里我就沒有展開來講。也可以發現，在緩解狀態爆炸的路上，通常都是結合了多種方法來實現的。在各種程序分析技術中切換，或許是未來符號執行發展的路線。