Page 289 - 《软件学报》2021年第6期

王小兵 等:面向 MSVL 的智能合约形式化验证 1863

alw(!(f and (h or r))).
Table 10 Description of property 6
表 10 性质 6 相关描述
类别 信息描述 操作符
执行完外部调用 f
原子命题 执行过 deposit 函数 h
执行过 withDraw 函数 r
命题逻辑 执行完外部调用时 deposit 或 withDraw 函数被调用 f and (h or r)
时序逻辑 在所有状态下(g and !f)都不成立 alw(!(f and (h or r)))

除此之外,当用户要求银行转账时,若该用户余额大于转账金额,则一定能够转账成功;并且当转账成功时,
该用户余额一定大于转账金额.从原子命题、命题逻辑与时序逻辑这 3 个方面对性质 7 进行描述见表 11,最终
使用 PPTL 公式描述性质 7 为
alw((p and q)->g) and alw(g->q).
Table 11 Description of property 7
表 11 性质 7 相关描述
类别 信息描述 操作符
用户请求转账 p
原子命题 用户余额大于转账金额 q
转账成功 g
当用户请求转账且其余额大于转账金额时,则转账一定成功 (p and q)->g
命题逻辑
当转账成功时,用户余额一定大于转账金额 g->q
时序逻辑 在所有状态下((p and q)->g)与(g->q)都成立 alw((p and q)->g) and alw(g->q)
(3) 合约完备性.
合约完备性是功能一致性与逻辑正确性的综合表达,只有满足功能一致性与逻辑正确性,才能认为合约满
足完备性.对于银行转账合约来说,其合约完备被描述为性质 8:性质 5~性质 7 同时满足.使用 PPTL 公式描述性
质 8 为
alw(m->n) and alw(!(f and (h or r))) and alw((p and q)->g) and alw(g->q).
将 MSVL 模型与 PPTL 公式输入到 UMC4M 中进行验证:首先,将性质的定义加入到 MSVL 程序中,并把
MSVL 程序放在 m 文件中,PPTL 公式 alw(m->som n) and alw(!(f and (h or r))) and alw((p and q)->g) and
alw(g->q)等价于 alw(!m or (som n)) and alw(!(f and (h or r))) and alw(!(p and q) or g) and alw(!g or q),在 p 文件中
输入待验证的 PPTL 公式,具体如下所示:
〈/
define m: m_flag=1; //定义命题 m
define n: n_flag=1; //定义命题 n
define f: f_flag=1; //定义命题 f
define h: h_flag=1; //定义命题 h
define r: r_flag=1; //定义命题 r
define g: g_flag=1; //定义命题 g
define p: p_flag=1; //定义命题 p
define q: q_flag=1; //定义命题 q
alw(!m or (som n)) and alw(!(f and (h or r))) and alw(!(p and q) or g) and alw(!g or q)
/〉
运行 UMC4M 检测器,验证结果为性质不满足.经过对性质 5~性质 7 的分别验证,发现性质 5 与性质 7 满足
而性质 6 不满足,表明存在重入攻击漏洞,攻击者劫持了外部调用,并在 fallback 回退函数中再次调用本合约中