完整流程

Securify分三个步骤进行：

1. 将合约的EVM字节码反编译成静态的单一赋值形式（ SSA——static-single assignment）；

2. 将SSA形式的代码转为基本事实（base facts）并推断关于合约的其他语义事实（semantic facts）；

3. 匹配由特定领域语言（DSL）编写的各种安全属性，输出对应模式并整合成安全报告。

安全模式匹配结果分为真阳性（violation）、假阳性、真阴性（compliance、no violation）、假阴性。对于真阳性与真阴性Securify都能直接给出准确结果，而对于假阳性与假阴性Securify只能在报告中给出警告标识（warning），之后通过额外人工或其他检测方式继续识别确定。

SSA

先讲讲SSA是什么东西。静态单一赋值形式（SSA）是中间表示（IR）的属性，它要求每个变量只分配一次，并且每个变量在使用之前定义。原始IR中的现有变量被拆分为版本，新变量通常由原始名称用下标表示，以便每次定义都有自己的版本。（注：在本方案中部分操作码如push、dup等会被消除）

base fact

当EVM字节码反编译成SSA形式的中间表示之后，我们需要将其转换成基本事实。

上图即一个基本事实的表示，其中instr是指令名称，L是指令标签（CFG中的基本块），Y是存储指令结果的指令（如果有的话），Xn是参数。

semantic fact

接着我们用基本事实推断出语义事实。

在智能合约的语义分析中，我们通常需要根据两种依赖关系来推断语义事实（流控制依赖+数据控制依赖）。

意思是存在某条路径使得L1基本块流向L2基本块。

意思是对任何路径都是L1基本块流向L2基本块。

意思是数据T修改了，数据Y也可能跟着被修改。

意思是数据Y和数据T是相等的。

意思是数据T不同的取值会导致数据Y的取值不同。

注：

1. 使用通配符(_)来代替在规则中只出现一次的变量

2. isConst、Taint、join是其他谓词表达，与op、mload、mstore、goto同样属于基本事实的表达。

trace、property

结论：

trace：指区块链从一个老状态更新到新状态，状态包括存储和内存状态、堆栈状态、事务信息和块信息。

property：指在trace上的一种关系，用一阶逻辑规则定义。

DSL（领域专用语言domain specific language）

• some+BNF合取范式：一部分路径符合条件

• all+BNF合取范式：全部路径符合条件

security patterns of properties

pattern classification

• instruction patterns：指令模式，即由某条指令导致违反该安全属性（例如上图中后6个安全模式）。

• contract pattern：合约模式，即因为整个合约的整体原因导致违反该安全属性（很难找出一个单一的指令对其违反负责，例如上图中第一个安全模式）。

Securify2.0

文章传送：https://arxiv.org/pdf/1806.01143.pdf