Security Prover

简介

Prover是一个动态扫描引擎，能够运行代码并探索其所有执行过程的状态空间。在探索过程中，Prover根据执行特征（如property变化和执行路径）来检测是否存在漏洞。同时，通过一些充分的约束条件，Prover能够证明代码中不包含某些关键漏洞，如 reentrancy。因此，Prover引擎既具有漏洞检测功能，又能验证代码中是否存在某些关键漏洞。

为实现Prover产品，我们构建了基于语义层的符号执行引擎，支持自动生成代码状态空间，并允许用户用Solidity编写Prover脚本以挖掘状态空间。

Prover的漏洞检测功能包括：编译合约文件生成AST树；动态执行语句，记录执行过程；最后依据状态空间、执行路径和内置规则判断是否存在漏洞。

Prover的安全性证明在获取状态空间后，定义各类漏洞的安全证明条件，如重入漏洞，从而证明代码中不会发生相应漏洞。

Prover的property证明通过用户自定义MAIN函数，验证合约执行过程中合约的property不会违反规则。

相比静态引擎，Prover具有更高的可靠性和更低的误报率，因为其分析的代码状态空间是真实可执行的。