合约验证变得更简单
智能合约开发者现在可以用编写代码的同一语言（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;
}
// the property
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
发现Bug！
在我们的示例中，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