合约验证变得更简单 - Trail of Bits博客
智能合约开发者现在可以使用编写代码的同一语言（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
11
12
|
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
# 所有者账户：0x28e9eb58c2f5be87161a261f412a115eb85946d9
# 合约账户：0x9384027ebe35100de8ef216cb401573502017f7
# 发送者_0账户：0xad5e556d9699e9e35b3190d76f75c9bf9997533b
# 属性发送者账户：0xad5e556d9699e9e35b3190d76f75c9bf9997533b
# 找到1个属性：crytic_test_balance
# 探索将在以下情况之一发生时停止：
# * 发送3个人工交易
# * 目标合约的代码覆盖率大于100%
# * 上次交易未获得更多覆盖率
# * 发现至少1个不同的属性可被破坏（1个用于快速失败）
# * 经过240秒
# 开始探索...
交易0. 状态：1，实时覆盖率：0.0%，失败属性：0/1
交易1. 状态：2，实时覆盖率：60.66%，失败属性：0/1
找到1/1失败属性。停止探索。
60.66% EVM代码覆盖
+---------------------+------------+
| 属性名称 | 状态 |
+---------------------+------------+
| crytic_test_balance | 失败 (0) |
+---------------------+------------+
查看测试用例：./mcore_kkgtybqb
|
注意每个失败属性都会有一个关联的测试用例编号。更多详细信息可以在指定的测试用例文件中找到：./mcore_kkgtybqb/user_000000.tx
发现漏洞！
在我们的示例中，manticore-verifier找到了破坏指定属性的方法。当尝试转移极其大量的代币时，内部整数表示超出其限制，使得发送者的储蓄可能增加，即凭空创建代币。
1
|
transfer(0,115792089237316195422001709574841237640532965826898585773776019699400460720238) -> STOP (*)
|
结论：互操作性 = 101%
manticore-verifier降低了符号测试任意属性的初始成本。它还使我们的符号执行器能够更紧密地与Solidity、Echidna和slither-prop协同工作。
相同的方法论可以与我们以太坊模糊测试器Echidna一起使用。因此，您可以编写一次属性，并使用符号执行和模糊测试进行测试，无需额外努力。
manticore-verifier可以检查自动生成的ERC20属性。此外，我们的静态分析器slither-prop具有关于ERC20合约应该做什么的详细信息，并且可以自动为manticore-verifier可以检查的ERC20生成属性。
所以获取您的合约，添加属性方法，并随意使用manticore-verifier进行测试。如有任何问题，请加入Empire Hacking Slack。