Securify v2.0发布

我们很高兴宣布Securify v2.0，这是流行的以太坊智能合约安全扫描器的新版本。

Securify v2.0通过以下特性超越了最先进的智能合约漏洞扫描器：

• 高精度：得益于全新的Solidity中间表示(IR)和完全声明式的上下文敏感静态分析
• 改进的可扩展性：利用高效的Souffle Datalog引擎驱动的完全声明式静态分析
• 高漏洞覆盖率：涵盖37种不同的安全属性，这些属性来自智能合约弱点分类注册表并按严重程度分类

重要的是，Securify v2.0仍然免费和开源。您可以在GitHub上免费下载Securify v2.0。

Securify v2.0支持什么？

• 用Solidity 0.5.*和0.6.*编写的以太坊智能合约
• 37种按严重程度分类的漏洞（支持的完整漏洞列表在本文底部）

Securify v2.0有什么新功能？

我们现在讨论添加到Securify v2.0的关键技术细节和改进。这些使Securify成为最全面和可扩展的Solidity静态分析器。

1. 使用新中间表示的源代码分析

与工具的第一个版本相比，Securify v2.0分析源代码，而不是EVM字节码。虽然由于语言结构更丰富，分析Solidity源代码更困难，但它捕获了字节码中缺失的重要语义信息。重要的是，Solidity精确捕获了合约的存储模型，允许清晰区分变量和映射，这些信息在字节码中使用的低级基于哈希的存储模型中不存在。

为了处理Solidity语言的复杂性，Securify v2.0将Solidity编译为新的清晰简洁的Solidity中间表示(IR)。新的IR基于MLton编译器用于Standard ML，并具有以下特性：

• 基本块上的控制流图(CFG)
• 基本块类似于延续传递风格中常见的延续，每个块接受参数，并具有以可以传递参数的传输形式指向下一个块的指针
• 变量的静态单赋值(SSA)形式和语句的三地址代码风格

为了说明IR，考虑以下Solidity代码：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

contract ToyExample{
    function inc(uint x) internal returns (uint){
        return x+1;
    }
    function main() external{
        uint res;
        for(uint i = 0; i < 42; i++){
            res = inc(i);
            require(res > 0);
        }
    }
}

Securify v2.0使用Solidity编译器获取合约的AST，然后将其转换为以下中间表示：

[按Enter或点击查看完整尺寸图像]

代码遵循静态单赋值形式(SSA)，将每个操作的结果分配给一个新变量（由语句标签标识）。代码被分成多个基本块。BLOCK00对应于函数inc的定义，BLOCK01对应于main函数的定义。变量以参数的形式在块之间传递（参见带注释的边）。这种表示简洁，节点类型数量有限，仅保留分析所需的信息。IR是完整的，因为任何Solidity智能合约都可以映射到它。

2. 通过调用点敏感度实现更高精度

Securify v2.0通过调用点敏感度实现更高精度。为了更好地理解调用点敏感度是什么以及它如何有益于我们的分析，请考虑以下示例：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

contract CallSitesTest {
    mapping(address => uint) aMapping;
    
    function id(address x) public returns (address){
        return x;
    }
    
    function unrestrictedStorage(address arbitraryAddress) external{
        address a = id(arbitraryAddress);
        aMapping[a] = 1;
    }
    
    function restrictedStorage(address arbitraryAddress) external {
        address b = id(msg.sender);
        aMapping[b] = 1;
    }
}

在上面的示例中，函数unrestrictedStorage和restrictedStorage接受用户提供的任意地址作为参数。注意，函数unrestrictedStorage允许任何人写入存储中的任意位置，而函数restrictedStorage允许用户仅写入存储中的aMapping[msg.sender]（其中msg.sender是用户的地址）。为了识别此漏洞，Securify v2.0将用户提供的值标记为不可信（在此示例中，它污染了arbitraryAddress）并沿程序的依赖图传播标签。精确的分析将识别地址a不可信，报告函数unrestrictedStorage易受攻击，而地址b可信，报告函数restrictedStorage安全。

Securify的第一个版本使用调用点不敏感分析，它将函数id的返回值标记为不可信，因为当函数id被函数unrestrictedStorage调用时，它返回arbitraryAddress的值。特别是，分析不区分函数id是从函数unrestrictedStorage还是函数restrictedStorage调用的。由于这种不精确性，分析也报告restrictedStorage函数易受攻击。

相比之下，Securify v2.0区分函数id是从函数unrestrictedStorage还是restrictedStorage调用的（因此称为调用点敏感）。额外的精度正确识别地址b不可信，进而正确标记函数restrictedStorage安全。

3. 通过完全声明式分析改进可扩展性

Securify的第一个版本在Java和Datalog的组合中实现更深的漏洞检查。这减慢了分析速度，因为它需要将所有中间Datalog结果传递给Java。

相比之下，Securify v2.0的分析是完全声明式的，并在Datalog中实现。这大大提高了分析的性能和可扩展性。此外，完全声明式分析提高了Securify的维护性和可扩展性，因为声明式模式更易于指定。

4. 更高的漏洞覆盖率

Securify v2.0支持37种已知漏洞模式。它将它们分为五个严重级别：严重、高、中、低和信息。与工具的第一个版本类似，Securify v2.0报告违规（保证违反给定安全属性的行为）和警告（可能违反安全属性的行为）。

如何使用Securify v2.0？

使用Securify v2.0的最简单方法是使用其Docker镜像，如下所示：

1

docker run -it -v `pwd`:/share securify /share/myContract.sol

在GitHub上按照说明将Securify v2.0安装为python包的替代方法：

1

securify myContract.sol

除了分析Solidity合约，Securify v2.0可以分析Etherscan.io上的任何合约：

1

securify -b <contractAddress> —key /path/to/api_key.txt

用户可以使用-i参数控制Securify应报告哪些严重级别：

1

securify myContract.sol -i CRITICAL HIGH

此外，用户可以使用-p参数指定要检查的漏洞：

1

securify myContract.sol -p LockedEther

支持的漏洞

Securify v2.0支持以下漏洞：

以下SWC漏洞不适用于pragma >=0.8的Solidity合约，因此Securify v2.0不检查它们：

• SWC-118（不正确的构造函数名称）
• SWC-129（使用+=）

如何贡献？

Securify v2.0可在GitHub上获取：https://github.com/eth-sri/securify2

要贡献，请报告您在使用该工具时遇到的任何问题和错误。

致谢

以下人员为Securify v2.0做出了贡献：

• Ioannis Sachinoglou
• Lavrentios Frobeen
• Frederic Vogel
• Dimitar Dimitrov
• Petar Tsankov

团队还要感谢以太坊基金会，它部分资助了Securify v2.0的开发。