合约验证变得更简单
智能合约开发者现在可以用编写代码的同一语言（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
|
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
|
注意，每个失败的属性都会有一个相关的测试用例编号。更多详细信息可以在指定的测试用例文件中找到：./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 合约应该做什么的详细信息，并且可以自动为 ERC20 生成 manticore-verifier 可以检查的属性。
所以，获取您的合约，添加属性方法，并随意使用 manticore-verifier 进行测试。如果您有任何问题，请加入 Empire Hacking Slack。
如果您喜欢这篇文章，请分享：
Twitter
LinkedIn
GitHub
Mastodon
Hacker News