符号执行和检测部分

oyente.symExec:run

前面讲到 oyente.oyente:analyze_bytecode 中为 symExec.run 传入反汇编文件，进行后续操作。

在不是 is_testing_evm 测试 evm 的情况下，关键函数有以下三个： analyze()、 detect_vulnerabilities()、closing_message()

oyente.symExec:analyze

好多函数中都有一个函数内的嵌套函数定义： timeout_cb() , 其内容为 DEBUG mode 时的 traceback1，作用：便于调试时，一层层显示信息。 Ps： 这里还使用的是嵌套函数，

Python 嵌套函数 在 Python 函数中定义嵌套函数

analyze() 函数的作用时，生成 CFG 控制流图，并分析 run_build_cfg_and_analyze ，如有异常，则抛出。而 run_build_cfg_and_analyze 函数中

  1. initGlobalVars()

    1. 初始化约束求解器，设置超时2

      1. 如果是并行的话，设置 simplify（简化）、solve-eqs（高斯消元）、smt（提供一个基于 SMT 的 solver）策略，还会把 goal 分解成子 goal

        ParThen：Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel. The tactic split-clause will select a clause (or f_1 ... f_n) in the input goal, and split it n subgoals.

      2. 如果反汇编文件中有 MSIZE，则将对应标志设置为 True

        MSIZE 为操作码之一，含义为：size of memory, i.e. largest accessed memory index。 0.4.24 的 opcode 列表

    2. 初始化 explorer 相关

      大致有一下（没写全）： | 变量 | 含义| |----|---| | visited_pcs | 访问过的路径的集合| | vertices |顶点字典| | edges |边字典| | visited_edges |访问过的边的字典| | calls_affect_state | call 影响的状态？不太清楚| | money_flow_all_paths | 金钱流列表| | reentrancy_all_paths | 重入流列表| | path_conditions | 路径条件列表| | global_problematic_pcs | 检测的漏洞的列表组成的字典|

      符号变量的名字生成器 还有 USE_GLOBAL_BLOCKCHAIN: 是否使用区块链全局状态 和 REPORT_MODE：是否生成报告

      instructions: capturing all the instructions, keys are corresponding addresses

  2. build_cfg_and_analyze()

    1. timeout to run symbolic execution

      在 global_params.py 中定义的 GLOBAL_TIMEOUT = 50 , 如果超时，则标记超时，且抛出超时异常

    2. change_format() 整理、简化反汇编文件的格式

      1. 替换一些 evm 未实现的反汇编为指令
      2. 简化每一行 00002: PUSH1 0x80 变成 2 PUSH1 => 0x80
      3. 然后写回反汇编源文件

    3. 读取上一步处理好的反汇编文件，并去除首行 runtimecode

    4. tokenize 模块提供语法、语义扫描解析3

      it breaks a stream of bytes into Python tokens. It decodes the bytes according to PEP-0263 fordetermining source file encoding

    5. collect_vertices 貌似看不太懂？

      1. Parse the disassembled file
      2. Then identify each basic block (i.e. one-in, one-out)
      3. Store them in vertices

    6. construct_bb 构建基本块

    7. construct_static_edges 构建静态边

    8. full_sym_exec 符号执行检测

      1. get_init_global_state 初始化当前状态

        global_state 有调用与被调用者余额， global_state["balance"]["Is"或"Ia"] ，pc（程序计数器)，接受和发送者地址，时间戳等

      2. init_analysis 初始化分析相关参数

      3. 创建 params 对象，而且把上两步的全局状态和 analysis 对象增加为该对象的属性。

    9. sym_exec_block 符号执行块， 是个递归

      1. 计数和检查最大边界

        1. 对 current_edge 的访问次数计数
        2. 判断 current_edge 访问次数是否超过 LOOP_LIMIT，如果超过，则返回 stack - [ ] 这里为什么要返回 stack
        3. 判断使用的 gas 是否超过 GAS_LIMIT，如果超过，则返回 stack

      2. 执行块中的指令

        循环遍历块的指令列表，每次执行一条，执行指令调用： sym_exec_ins()

      3. 将当前块标记为已访问

      4. 漏洞路径更新

        将路径加入重入漏洞路径？（怎么就直接加入了，哪里检测了？） 如果当前 money_flow 路径在全部 money 漏洞中不存在，则更新相关路径。

      5. Go to next Basic Block(s)

        根据跳转类型，选择块，然后更新相关条件，然后递归。 跳转类型： terminal、unconditional、falls_to、conditional

        1. 终止类型或者深度超过 DEPTH_LIMIT，则终止该路径，并 display_analysis money flow相关？ - [ ] 为什么
2. 无条件，则更新相关参数，然后直接跳转
3. follow to 的同上
4. 有条件跳转

    采用 DFS 深度优先搜索递归遍历
    先检查左节点，如果约束有解，则向左递归，直到叶子节点，然后回退一个节点，走右边节点，若约束有解，则进入右边节点。

    10. sym_exec_ins 符号执行指令

      模拟执行指令 opcode

  3. detect_vulnerabilities instruction 是一个以 {指令地址:指令}的字典

    1. 计算代码覆盖率，evm_code_coverage
    2. 分别检测漏洞，将结果放如 result 二维列表
    3. vulnerability_found 没有看懂

  4. closing_message 分析结束，根据全局变量 STORE_RESULT 觉得那个是否存储分析结果。

参考资料