Page 287 - 《软件学报》2021年第6期
P. 287
王小兵 等:面向 MSVL 的智能合约形式化验证 1861
define r: r_flag=1; //定义命题 r
fin(!m) and alw(!(q) or r) and alw(!(p and r) or (som q))
/〉
运行 UMC4M 检测器的结果如图 14 所示,验证结果为模型满足性质,总用时 653ms.
MC vote.p vote.m
$$$$$$$$$$$$$$$$$
ThreadPool init success!!!
Verification Result: Val id!!!
Release ThreadPoo1 success!!!
The run time is: 653ms
Fig.14 Verification results of the vote smart contract
图 14 投票智能合约验证结果
4.2 银行转账合约的建模与验证
本小节以具体的银行转账智能合约与常见的重入攻击漏洞为例,给出 SOL2M 对转账合约与重入攻击进行
建模的详细流程以及验证过程.建模时,在银行转账合约中抽象加入了重入攻击操作,即将转账合约与重入攻击
代码抽象为合约.如图 15 所示,其中,deposit 函数的功能是用户把钱存入银行,withDraw 函数实现了转账功能,
用户通过 withDraw 函数与 send 函数从银行取钱.Attack 函数实现了重入攻击的功能,其具体步骤为:首先,攻击
者调用 Attack 函数,通过 deposit 函数向银行转账合约中存入一些以太币;之后调用 withDraw 函数,从银行转账
合约中取钱,使用 require 语句判断用户余额以及银行总余额是否足够;最后,调用 send 函数给用户地址转账.问
题出现在第 10 行与第 11 行:合约执行 send 操作后修改用户余额,当合约发送以太币给攻击合约时会执行回退
函数,建模过程中使用 fallback 模拟,其中会再次调用 withDraw 函数取钱.当执行 require 语句时,由于第 11 行还
未执行,用户余额未改变,require 语句顺利通过,银行转账合约继续向攻击合约转账.不断重复这些操作,攻击者
可以从合约中提取所有以太币.
1 pragma solidity>=0.4.22<0.6.0;
2 contract ReTry {
3 mapping(address>=uint) public userBalance;
4 uint public Limit=1;
5 uint public bankbalance=0;
6 function withDraw(address sender,uint toWithdraw) public {
7 uint amount=userBalance[sender];
8 require(amount>=toWithdraw);
9 if (amount>0) {
10 send(sender,toWithdraw);
11 userBalance[sender]−=toWithdraw;
12 }
13 }
14 function deposit(address sender,uint value) public {
15 userBalance[sender]+=value;
16 bankbalance+=value;
17 }
18 function send(address sende r,uint toWithdraw) public {
19 msg.value+=toWithdraw;
20 fallback(sender);
21 }
22 function Attack(address sender) public {
23 deposit(sender,1);
24 withDraw(sender,1);
25 }
26 function fallback(address sender) public {
27 require(bankbalance>0);
28 withDraw(sender,1);
29 }
30 }
Fig.15 Bank transfer smart contract
图 15 银行转账智能合约
