符号执行

原理

符号执行的关键思想就是，把输入变为符号值，那么程序计算的输出值就是一个符号输入值的函数。

流程

反汇编字节码为汇编代码 对 evm 没有实现

  1. 对待分析的单个过程代码对象构建控制流图构建控制流图（Control Flow Graph，CFG）

    在遇到分支节点时，使用约束求解器判定哪条分支可行，并根据预先设计的路径调度策略实现对该过程所有路径的遍历分析

  2. 构建虚拟执行机模型,对每条语句解释执行 laser-evm

动态符号执行

动态符号执行是以具体数值作为输入来模拟执行程序代码

问题

路径爆炸问题

由于在每一个条件分支都会产生两个不同约束，符号执行要探索的执行路径依分支数指数增长。在时间和资源有限的情况下，应该对最相关的路径进行探索，这就涉及到了路径选择的问题。通过路径选择的方法缓解指数爆炸问题，主要有两种方法：

污点分析

污点分析就是分析程序中由污点源引入的数据是否能够不经无害处理,而直接传播到污点汇聚点.如果不能,说明系统是信息流安全的;否则,说明系统产生了隐私数据泄露或危险数据操作等安全问题.