智能合约验证变得更简单

智能合约开发者现在可以使用他们编写代码的语言（Solidity）来表达安全属性，我们的新工具manticore-verifier会自动验证这些不变量。更棒的是，Echidna和Manticore现在共享相同的属性测试规范格式。

这意味着开发者只需编写一次属性测试，就可以同时进行模糊测试和符号执行验证！manticore-verifier从根本上降低了符号化测试任意属性所需的初始投入和成本。

工作原理

智能合约的行为及其潜在漏洞往往具有独特性，并高度依赖于未明示的合约不变量。让我们测试一个简单合约：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32


contract Ownership{
    address owner = msg.sender;
    function Owner() public{
        owner = msg.sender;
    }
    modifier isOwner(){
        require(owner == msg.sender);
        _;
    }
}

contract Pausable is Ownership{
    bool is_paused;
    modifier ifNotPaused(){
        require(!is_paused);
        _;
    }
    function paused() isOwner public{
        is_paused = true;
    }
    function resume() isOwner public{
        is_paused = false;
    }
}

contract Token is Pausable{
    mapping(address => uint) public balances;
    function transfer(address to, uint value) ifNotPaused public{
        balances[msg.sender] -= value;
        balances[to] += value;
    }
}

该合约维护资产负债表并允许简单交易。用户可以发送代币给其他用户，但代币总量必须保持不变——即合约启动后不能再创建新代币。因此在这个不变量下，有效属性可以表述为：“如果只有10,000个代币，那么没有用户可以拥有超过这个数量。”

我们可以将这个属性表示为Solidity方法：“crytic_test_balance”。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10


import "token.sol";
contract TestToken is Token {
    constructor() public{
        balances[msg.sender] = 10000;
    }
    // 属性定义
    function crytic_test_balance() view public returns(bool){
        return balances[msg.sender] <= 10000;
    }   
}

模拟世界

ManticoreEVM编译合约并在完全模拟的符号化区块链中创建合约。同时创建不同的普通账户来模拟真实场景：部署者账户用于部署合约，其他账户用于探索合约并尝试破坏属性，最后可能使用不同账户来测试属性。

ManticoreEVM检测高级源代码中存在的属性类型方法，并在每次符号交易组合后检查它们。如果方法返回false，则普通属性被视为失败。

探索循环

部署者账户最初通过CREATE交易创建目标合约。然后manticore-verifier模拟来自合约测试者的所有可能的交错交易，直到（例如）找不到更多覆盖率。每次符号交易后，都会以属性检查账户的名义检查属性，如果发现任何问题，就会生成可复现的漏洞利用跟踪报告。像crytic_test_balance()这样的普通属性预期返回true；任何其他结果都会被报告为问题。

1

manticore-verifier dapp.sol --contract TestToken

命令行工具

探索的多个方面、停止条件和使用的用户账户都可以通过命令行参数修改。运行$manticore-verifier –help查看完整列表。以下是运行示例：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24


$manticore-verifier dapp.sol --contract TestToken

# Owner account: 0x28e9eb58c2f5be87161a261f412a115eb85946d9
# Contract account: 0x9384027ebe35100de8ef216cb401573502017f7
# Sender_0 account: 0xad5e556d9699e9e35b3190d76f75c9bf9997533b
# PSender account: 0xad5e556d9699e9e35b3190d76f75c9bf9997533b
# Found 1 properties: crytic_test_balance
# Exploration will stop when some of the following happens:
# * 3 human transaction sent
# * Code coverage is greater than 100% measured on target contract
# * No more coverage was gained in the last transaction
# * At least 1 different properties where found to be breakable. (1 for fail fast)
# * 240 seconds pass
# Starting exploration...
Transaction 0. States: 1, RT Coverage: 0.0%, Failing properties: 0/1
Transaction 1. States: 2, RT Coverage: 60.66%, Failing properties: 0/1
Found 1/1 failing properties. Stopping exploration.
60.66% EVM code covered 
+---------------------+------------+
|    Property Named   |   Status   |
+---------------------+------------+
| crytic_test_balance | failed (0) |
+---------------------+------------+
Checkout testcases here:./mcore_kkgtybqb

发现的漏洞

在我们的示例中，manticore-verifier找到了破坏指定属性的方法。当尝试转移极其大量的代币时，内部整数表示超出限制，使得发送者的储蓄可以异常增加，即凭空创造代币。

1

transfer(0,115792089237316195422001709574841237640532965826898585773776019699400460720238) -> STOP (*)

结论：互操作性=101%

manticore-verifier降低了符号化测试任意属性的初始成本。它还使我们的符号执行器能够更紧密地与Solidity、Echidna和slither-prop协同工作。

相同的方法论也可以与我们的以太坊模糊测试器Echidna一起使用。因此，您可以编写一次属性，然后通过符号执行和模糊测试来验证它们，无需额外工作。

manticore-verifier可以检查自动生成的ERC20属性。此外，我们的静态分析器slither-prop详细记录了ERC20合约应该做什么，并可以自动生成manticore-verifier可以检查的ERC20属性。