路徑爆炸

之前說過，angr在處理分支時，採取統統收集的策略，因此每當遇見一個分支，angr的路徑數量就會乘2，這是一種指數增長，也就是所說的路徑爆炸。

以下是路徑爆炸的一個例子：

char buffer[17];
for(int i=0;i<16;i++){
        if(buffer[i]!='B'){
            return 0;
        }
}
return 1;

buffer的字元長度為16，當它等於16個連續的'B'時，程式返回1，然而angr在探索這樣的路徑時，會遇上16次if語句，也就相應地產生2的16次方個路徑，但正確的答案只有一條路徑能夠達到（if全為false的那一條），這一條路徑就被淹沒在大量錯誤路徑中，產生了路徑爆炸。

因此當遇見大量分支（尤其是迴圈中巢狀的if語句）時，必須想辦法緩解這種路徑爆炸。

angr常用的緩解路徑爆炸的方式有四種：

• 重寫可能導致路徑爆炸的函式或程式碼片段，可以採用angr提供的hook
• veritesting：結合動態符號執行和靜態符號執行
• Lazy Solve：跳過不必要的函式
• Symbion：結合具體執行和符號執行

在angr_ctf中只涉及到了前兩種方式，因此本篇著重說說第一種方式，以及簡略介紹下第二種方式。angr緩解路徑爆炸的策略，後續新開一篇詳細談談。

重寫程式碼片段

仍然以上一節路徑爆炸中用的程式碼片段為例，字串buffer要按位比較16次從而產生2的16次方條路徑，它的路徑大致如下圖：

angr必須選擇16次F才能達到目標狀態。

然而根據逆向分析得出的結果來看，只要讓buffer='B'*16就可以通過這段程式碼了，因此如果我們之間跳過這段程式碼，然後在跳過了這段程式碼的state中新增一個約束：buffer='B'*16，這樣就不會產生路徑了。

你可能會問，既然我們都通過逆向的手段看出來buffer等於16個B了，那為什麼還要使用angr呢。

然而如果真正的目標狀態在該程式碼片段的後面，這段會產生路徑爆炸的程式碼如果不繞開的話，你很可能無法達到真正的目標狀態。

Hook

Hook可以譯為掛鉤或者鉤子，是逆向工程中改變程式執行流程的技術，可以讓自己的程式碼執行在其他程式當中。通常說Hook函式，則是接收被Hook函式的引數，然後使用這些引數執行自己的程式碼，並將返回值返回（也可以沒有返回值），至於被Hook的函式，可以選擇讓它繼續執行，或者不執行。

聽上去Hook技術很麻煩，讓其他程式執行自己寫的程式碼似乎挺不可思議的。Hook技術值得深入研究，但angr提供了簡便的Hook介面，能夠用於Hook被angr模擬執行的程式，它通常有兩種方式：

• 裝飾器@project.hook
• 函式project.hook_symbol

裝飾器@project.hook

@project.hook(hook_addr, length=ins_length)
def hook_ins(state):
    #your code

請注意，這裡的project.hook來自於你使用angr.Project方法建立的頂層模組（即project=angr.Project('filename')）。

該方法相當於在hook_addr處刪去長度為length的指令，然後用hook_ins中的指令替代。

該裝飾器需要傳入待hook的地址，以及要跳過的指令的長度，然後在hook_ins中實現你的程式碼即可。

使用裝飾器的方法，如果是對函式進行hook而不是對某一程式碼片段進行hook的話，無法接收函式的引數，需要根據情況來使用。

hook_symbol

假設程式中有一個這樣的原始函式：

int my_add(int a, int b){
    return a+b;
}

那麼這樣的函式可以被下面的方式hook掉：

class Replace_my_add(angr.SimProcedure):
    def run(self, a, b):
        return a - b
    
hooked_func_name = 'my_add'
project.hook_symbol(hooked_func_name, Replace_my_add())

該方法相當於替換了原函式，為此你需要建立一個類，繼承自angr.SimProcedure，類名隨意。

然後在類中重寫run方法，run的self後的引數與待hook的函式相同。

最後在主函式中，呼叫project.hook_symbol，並傳入待hook的函式名以及新建的繼承自SimProcedure的類的物件即可。

設立返回值

• 對於裝飾器

該方法相當於程式碼片段的替換，因此如果你選擇跳過了某條函式呼叫語句（例如 call my_add這條彙編指令），那麼就需要去檢視該函式的返回值，或者說程式碼片段的最終計算結果，被儲存在了什麼地方。找到這個地方，然後使用記憶體或者暫存器操作，將返回值填入即可。

一般來說，32位程式函式的返回值會放在eax暫存器中

• 對於hook_symbol

該方式相當於替換了函式的內容，因此直接在重寫的run方法中使用return返回即可

返回值的時候，如果需要根據某個符號變數來決定返回的內容（例如判斷一個符號變數等於某個字串時返回1，否則返回0），此時不能用python的if語句來判斷，然後分別返回1和0，這有兩個問題：

• 符號變數與其他內容進行比較（無論是符號變數、位向量、常數、變數），它的真值永遠是false
• 如果返回值後續參與了其他的路徑選擇，此時若只返回了值而不是帶約束的符號變數，可能會造成約束丟失

這種情況下，需要使用claripy.If來返回值：

state.regs.eax = claripy.If(buffer == target, claripy.BVV(1, 32),claripy.BVV(0, 32))

上面程式碼的意思是，當buffer==target時，將位向量<BVV32 1>傳遞給eax，否則將位向量<BVV32 0>傳遞給eax

而如果不這麼做，你可能會寫出這樣的程式碼：

if buffer==target:
    state.regs.eax = claripy.BVV(1,32)
else:
    state.regs.eax = claripy.BVV(0,32)

這兩種做法的區別在於，如果buffer或target中至少存在一個符號變數，下面的方式將永遠判斷為false。

此外，兩種方式傳遞給eax的內容也不同，下面一種方式傳遞的是一個位向量，而上面的方式傳遞的是帶約束的符號變數（之後實戰中你會看到更多）。

Veritesting

veritesting意為路徑歸併，它在動態符號執行（DSE）和靜態符號執行（SSE）之間切換，結合兩種方式減少了路徑爆炸的影響。

• DSE：為路徑生成公式，生成公式時負載很高，但公式易解
• SSE：為語句生成公式，公式生成容易，也能覆蓋更多路徑，但更難解

詳細可參見這篇論文：Enhancing symbolic execution with veritesting (acm.org)

在angr中，要啟動veritesting，有以下兩種方式：

p = angr.Project('/bin/true')
state = p.factory.entry_state()

#初始化SM時啟動
simgr = p.factory.simgr(state, veritesting=True)

#或者在SM初始化後啟動
simgr = p.factory.simgr(state)
simgr.use_technique(angr.exploration_techniques.Veritesting())

state外掛

之前提到的angr的求解器solver，以及操作記憶體、暫存器、檔案系統的方法：memory、regs、fs等，實際上都是state的外掛，下面說明兩個其他常用的外掛。

全域性外掛global

state.global實現了標準python dict介面，使用它你能夠在模擬執行的state中儲存任意資料，並且很方便的就能訪問到。可以使用如下的語句訪問全域性變數：

state.globals['x'] = a_symbol

全域性變數名x不需要提前宣告，但當你需要使用這個全域性變數之前，需要對它賦值。

history外掛

history記錄了一個狀態的執行路徑，它是一個連結串列，每個節點代表一次執行的狀態。你可以不斷使用.parent來回溯這個連結串列，history的使用方式如下：

• state.history.bbl_addrs：返回當前state執行的基本塊的地址列表
• state.history.parent.bbl_addrs：返回上一個state執行的基本塊的地址列表
• state.history.descriptions：描述state上每輪執行的狀態的字串列表
• state.histroy.guards：到達當前state所走路徑需要滿足的條件的列表（也就是每次分支判斷時為True還是False）
• state.history.events：執行過程中發生的事件列表，比如符號跳轉條件、彈出訊息框等

此外，在每種方法前加上recent_，就可以獲取列表中最近的那個地址，例如state.history.recent_bbl_addrs會返回當前state最近執行的基本塊的地址。

實戰：08_angr_constraints

先逆向檢視邏輯

和之前一樣，先對輸入進行混淆，然後再判斷。

但這裡的問題在於，首先字串的長度為16，此外，在check_equals函式中，採用的是按位比較的方式：

而字串長度為16，那麼就會進行16次比較，從而產生2的16次方條路徑，這樣angr就會陷入路徑爆炸。

但能夠注意到，check函式中實際上是在讓buffer與password進行比較（0x0804a040就是password的地址），而password在main的開頭被初始化為一串已知的字串。

因此可以考慮讓模擬執行在呼叫check函式之前停下來，然後新增一個符號約束（buffer==已知的字串），之後再用求解器求解buffer即可。

angr指令碼如下：

import angr
import claripy
import time


def good(state):
    tag = b'Good' in state.posix.dumps(1)
    return True if tag else False


def bad(state):
    tag = b'Try' in state.posix.dumps(1)
    return True if tag else False


time_start = time.perf_counter()

path_to_binary = './dist/08_angr_constraints'
p = angr.Project(path_to_binary, auto_load_libs=False)
start_addr = 0x08048625
init_state = p.factory.blank_state(addr=start_addr)

buffer = claripy.BVS('buffer', 16*8)
# buffer的地址
buffer_addr = 0x0804a050
init_state.memory.store(buffer_addr, buffer)

simgr = p.factory.simgr(init_state)

# call check指令的地址
check_addr = 0x08048565
# 讓程式模擬執行到call check時就標記為目標狀態
simgr.explore(find=check_addr)

if simgr.found:
    solution_state = simgr.found[0]
    # 由於buffer經過混淆函式混淆發生了變化
    # 因此需要從buffer的記憶體地址中取出buffer目前的值
    buffer_current = solution_state.memory.load(buffer_addr, 16)
    key = 'AUPDNNPROEZRJWKB'

    # 為當前狀態新增約束
    solution_state.solver.add(buffer_current == key)

    # 求解buffer
    solution = solution_state.solver.eval(buffer, cast_to=bytes)
    print('[+]Success:', solution.decode())


else:
    raise Exception("Could not find solution")

print('program last: ', time.perf_counter() - time_start)

你大概有兩個問題：

• 為何要重新從buffer_addr中取出符號變數，不能直接使用buffer嗎？
• 在實戰05中輸入字串的長度為32，然後使用了strncmp進行比較，strncmp的底層實現也是按位比較的，為何之前不用考慮路徑爆炸的問題呢？

首先第一個問題，我們可以先將buffer打印出來，應該能得到一個位向量<BV128 buffer_0_128>。該位向量之後被我們儲存在了buffer的地址當中。

然後列印一下buffer_current：

_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:0]))[63:32] >> 0x3[7:0] + 26 * 0xffffffbf + (buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:0]) >> 0x1f[7:0]>

會得到一個極為龐大的符號變數，或者說一個表示式，這是位向量<BV128 buffer_0_128>經過混淆函式混淆後的結果，因此要求解的應該是這個表示式。

我們建立的符號buffer被儲存在了buffer的地址當中，然後模擬程式執行時，從地址中取出符號進行混淆，混淆的過程也被儲存在buffer的地址中，因此在最後需要從這個地址裡面取出混淆後的符號進行求解。

第二個問題，先說結論：angr在路徑選擇時只進入庫函式一次，而不關心庫函式內部的實現採用了多少次if。

編寫以下兩個c程式並編譯（我這裡使用gcc編譯成64位了，與題目的32位不符，但原理相同）：

#include<stdio.h>

char buffer[9];
char passwd[9] = "abcdefgh";

int main(){
    scanf("%8s", buffer);
    if (strncmp(buffer, passwd ,8)==0){
        printf("good");
    }
    else{
        printf("bad");
    }
}

#include<stdio.h>

char buffer[9];
char passwd[9] = "abcdefgh";

int check(int size){
    int i = 0;
    for(i;i<size;i++){
        if(buffer[i]!=passwd[i]){
            return 0;
        }
    }
    return 1;
}

int main(){
    scanf("%8s", buffer);
    printf("%s\n",buffer);
    if (check(8)){
        printf("good");
    }
    else{
        printf("bad");
    }
}

兩個程式都接收8個字元，然後與abcdefgh進行比較，區別在於第一個程式使用庫函式strncmp進行比較，而後一個程式則自己定義了一個check進行比較，兩者比較的內部原理都是按位迴圈比較（strncmp還進行了一些額外處理，但基本原理仍然是按位迴圈比較，具體可參見strncmp原始碼）

然後，我們使用符號變數填充到buffer對應的地址中，讓模擬執行從scanf後的語句開始執行，並以列印good為目標狀態。

獲取目標狀態後，使用history外掛打印出當前state執行的基本塊，這些步驟的angr程式碼如下：

import angr
import claripy
import time


def good(state):
    tag = b'good' in state.posix.dumps(1)
    return True if tag else False


def bad(state):
    tag = b'bad' in state.posix.dumps(1)
    return True if tag else False


start_time = time.perf_counter()
p = angr.Project('./a', auto_load_libs=False)
init_state = p.factory.blank_state(addr=0x40118b)

buffer_addr = 0x404060
x = claripy.BVS('x', 8 * 9)
init_state.memory.store(buffer_addr, x)

simgr = p.factory.simgr(init_state)
simgr.explore(find=good, avoid=bad)

if simgr.found:
    solution_state = simgr.found[0]
    x_current = solution_state.memory.load(buffer_addr, 8)
　　# 列印路徑
    for address in solution_state.history.bbl_addrs:
        print(hex(address))
    result = solution_state.solver.eval(x_current, cast_to=bytes)
    print(result)
else:
    raise Exception("Could not find solution")

print(time.perf_counter() - start_time)

兩個程式的angr指令碼相同，修改一下地址和檔名即可，此外還需要注意，如果編譯時沒加任何引數，裝載的地址可能會跟你在IDA中看到的不一樣，例如我使用angr時提示如下：

WARNING | 2022-11-29 02:41:46,685 | cle.loader | The main binary is a position-independent executable. It is being loaded with a base address of 0x400000.

它提示我們，程式被裝載到基地址0x400000中了，而我們在IDA中看到的程式的地址main函式以0x1169開頭，這是一個相對地址，因此在編寫angr指令碼時，要將這些相對地址加上0x400000.

此時打印出來兩種判斷方式的路徑如下：

#程式1
0x40118b 0x401040 0x500010 0x40119a 0x401030 0x500008 0x4011b8 0x401050 0x500018 0x4011ce 0x401030 0x500008 0x4011ec 0x4011f0 0x401050 0x500018
#程式2
0x4011c9 0x401030 0x500008 0x4011d8 0x401159 0x401198 0x401169 0x401194 0x401169 0x401194 0x401169 0x401194 0x401169 0x401194 0x401169 0x401194 0x401169 0x401194 0x401169 0x401194 0x401169 0x401194 0x4011a0 0x4011e2 0x4011e6 0x401040 0x500010

程式1中0x40119a所在的基本塊就是呼叫strncmp的基本塊，它只被執行了一次，因此在if語句中只會產生2個路徑。

而程式2中check函式內部的迴圈語句所在的基本塊0x401169和0x401194被執行了8次，從而產生了2的8次方個路徑。

因此可以得到開頭的結論，庫函式內部如何實現，與angr無關，並不會產生額外的路徑。

實戰：09_angr_hooks

仍然先逆向檢視邏輯

程式先接收一個輸入，輸入被混淆後與password進行比較，password被初始化為一個已知的字串。

然後程式混淆password，再接收一個輸入，將輸入與混淆後的password進行比較。（兩個for迴圈中的地址分別是buffer和password的地址）

第一次比較在check函式中按位比較，後一次比較則是使用了strncmp函式，因此路徑爆炸發生在check函式中，對於strncmp則無須處理。

這次使用裝飾器的方法來解決這個問題：

1. 使用裝飾器跳過呼叫check函式的指令，也就是call cehck_equals
2. 在裝飾器內部實現符號==AUPDNNPROEZRJWKB的約束
3. 將符號約束作為返回值返回，檢視彙編程式碼可以知道，check函式的返回值儲存在了eax暫存器中

angr指令碼如下：

import angr
import time
import claripy

time_strat = time.perf_counter()


def good(state):
    tag = b'Good' in state.posix.dumps(1)
    return True if tag else False


def bad(state):
    tag = b'Try' in state.posix.dumps(1)
    return True if tag else False


path_to_binary = './dist/09_angr_hooks'
p = angr.Project(path_to_binary, auto_load_libs=False)
init_state = p.factory.entry_state()
# call check_equal的地址
check_addr = 0x080486b3
# call check_equal的指令長度
ins_size = 5


@p.hook(check_addr, length=ins_size)
def skip_check(state):
    buffer_addr = 0x0804a054
    buffer = state.memory.load(buffer_addr, 16)
    target = 'XYMKBKUHNIQYNQXE'
    # 使用claripy.If返回一個符號約束
    tmp = claripy.If(buffer == target, claripy.BVV(1, 32), claripy.BVV(0, 32))
    print(type(tmp))
    print(tmp)
    state.regs.eax = tmp


simgr = p.factory.simgr(init_state)
simgr.explore(find=good, avoid=bad)

if simgr.found:
    solution_state = simgr.found[0]
    flag = solution_state.posix.dumps(0)
    print(flag)
else:
    raise Exception("Could not find solution")

打印出tmp的內容，其中最後的片段如下：

packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:0]) >> 0x1f[7:0]) == 0x58594d4b424b55484e4951594e515845 then 0x1 else 0x0>

tmp前面的內容即buffer的內容，是經過混淆計算後的符號，而在最後可以看到，claripy.If建立了一個判斷，因此實際上返回了一個約束，這就是為什麼不適用python中的if然後傳遞一個<BVV32 1>的原因。

實戰：10_angr_simprocedures

第十題的路徑爆炸仍然發生在check_equals函式當中，與上一題的區別在於，此時輸入的字串被儲存在區域性變數當中，我們無法提前得知它的地址，因此如果要hook掉check函式，則必須獲取check函式的引數。

因此需要使用hook_symbol的方式來hook掉check函式

使用方式之前說明了，只需要注意使用hook_symbol的方法本質上是建立了新的函式取代了原有函式，因此在返回值的時候使用return返回，而不用將值儲存在eax當中（事實上重寫的run方法中沒有當前的state，你也儲存不到eax裡面）

angr指令碼如下：

import angr
import time
import claripy

time_strat = time.perf_counter()


def good(state):
    tag = b'Good' in state.posix.dumps(1)
    return True if tag else False


def bad(state):
    tag = b'Try' in state.posix.dumps(1)
    return True if tag else False



path_to_binary = './dist/10_angr_simprocedures'
p = angr.Project(path_to_binary, auto_load_libs=False)
init_state = p.factory.entry_state()

class Hook(angr.SimProcedure):

    def run(self, addr, size):
        # 後兩個引數即為check_equals函式的引數
        input_buffer = addr
        input_size = size

        # 從記憶體中讀取輸入
        input_str = self.state.memory.load(input_buffer, input_size)
        right_str = 'ORSDDWXHZURJRBDH'

        # 比較返回符號約束
        result = claripy.If(input_str == right_str, claripy.BVV(1, 32),
                            claripy.BVV(0, 32))

        return result

# funcname一定要相同，可在IDA中檢視
hooked_funcname = 'check_equals_ORSDDWXHZURJRBDH'
p.hook_symbol(hooked_funcname, Hook())

simgr = p.factory.simgr(init_state)
simgr.explore(find=good, avoid=bad)

if simgr.found:
    solution_state = simgr.found[0]
    flag = solution_state.posix.dumps(0)
    print(flag)

實戰：11_angr_sim_scanf

此題與實戰2-7中的題類似，實際上使用萬能指令碼就可以成功。出於練習的目的，跟著angr_ctf作者的思路，我們使用hook_symbol方法來hook掉scanf函式。

angr指令碼如下，使用到了state的全域性變數外掛，用法很簡單，用於進行約束求解。如果不使用全域性變數的話，從buffer的地址中取出符號進行求解也是一樣的（就像在實戰8中做的那樣）

import angr
import claripy

def good(state):
    tag = b'Good' in state.posix.dumps(1)
    return True if tag else False


def bad(state):
    tag = b'Try' in state.posix.dumps(1)
    return True if tag else False


path_to_binary = './dist/11_angr_sim_scanf'
project = angr.Project(path_to_binary, auto_load_libs=False)

initial_state = project.factory.entry_state()


class ReplacementScanf(angr.SimProcedure):
    # 第一個引數是scanf的格式化字串，接著是兩個buffer地址
    def run(self, format_string, scanf0_address, scanf1_address):
        # 在run中完成scanf的功能，即向目標地址寫入符號
        # 定義兩個符號變數，用於寫入buffer
        scanf0 = claripy.BVS('scanf0', 32)
        scanf1 = claripy.BVS('scanf1', 32)

        # 寫入記憶體，最後一個引數指定位元組序
        self.state.memory.store(scanf0_address,
                                scanf0,
                                endness=project.arch.memory_endness)
        self.state.memory.store(scanf1_address,
                                scanf1,
                                endness=project.arch.memory_endness)

        # 儲存變數到全域性，方便後續約束求解
        self.state.globals['solution0'] = scanf0
        self.state.globals['solution1'] = scanf1


# scanf的函式名稱，可在ida中檢視
scanf_symbol = '__isoc99_scanf'
project.hook_symbol(scanf_symbol, ReplacementScanf())

simulation = project.factory.simgr(initial_state)

simulation.explore(find=good, avoid=bad)

if simulation.found:
    solution_state = simulation.found[0]

    # 對符號變數進行約束求解
    stored_solutions0 = solution_state.globals['solution0']
    stored_solutions1 = solution_state.globals['solution1']
    scanf0_solution = solution_state.solver.eval(stored_solutions0)
    scanf1_solution = solution_state.solver.eval(stored_solutions1)

    print(scanf0_solution, scanf1_solution)

else:
    raise Exception('Could not find the solution')

實戰：12_angr_veritesting

先逆向分析

可以看到，此題與之前的題目不同的地方在於，它不僅是按位進行比較的，而且是按位進行混淆後馬上比較。之前的題目都是整體混淆後比較。因此路徑爆炸同時出現在混淆和比較兩個地方。

之前的做法是跳過迴圈比較，直接讓混淆後的字串與正確的字串比較，但這裡不能這樣做，跳過迴圈比較就意味著跳過了混淆。

因此考慮使用路徑歸併的搜尋策略veritesting，此題就是用來體驗一把veritesting的強大功能的。

angr指令碼如下，直接使用萬能指令碼，並且開啟veritesting：

import angr
import claripy
import time

start_time = time.perf_counter()
p = angr.Project('./dist/12_angr_veritesting', auto_load_libs=False)
init_state = p.factory.entry_state()



def good(state):
    tag = b'Good' in state.posix.dumps(1)
    return True if tag else False


def bad(state):
    tag = b'Try' in state.posix.dumps(1)
    return True if tag else False

simgr = p.factory.simgr(init_state, veritesting=True)
simgr.explore(find=good, avoid=bad)

if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.posix.dumps(0).decode())

print(time.perf_counter() - start_time)

（不加veritesting直接能跑宕機，大佬的智慧真是看不懂，但是真好用）