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

1860 Journal of Software 软件学报 Vol.32, No.6, June 2021

Table 6 Description of property 1
表 6 性质 1 相关描述
类别 信息描述 操作符
原子命题 有其他候选者的票数比 winner 函数得到的赢家票数高 m
命题逻辑 不存在 m 成立的情况 !m
时序逻辑 投票结束后,不存在 m 成立的情况 fin(!m)

(2) 逻辑正确性.
关乎智能合约的安全问题,是指保证合约内函数的逻辑正确,即不存在逻辑漏洞.对于投票智能合约来说,
vote 函数是整个合约的逻辑核心部分,其逻辑为:当投票者调用 vote 函数发起投票时,其手中拥有的票数至少为
1,且当投票者手中有票时,一定会投票成功.将该逻辑精简为性质 2 与性质 3.
• 性质 2:当投票者投票成功时,则其手中一定有票.从原子命题、命题逻辑与时序逻辑这 3 个方面对性质
2 进行描述见表 7,最终使用 PPTL 公式描述性质 2 为 alw(q->r);
Table 7 Description of property 2
表 7 性质 2 相关描述
类别 信息描述 操作符
投票成功 q
原子命题
手中有票 r
命题逻辑 若投票成功,则手中一定有票 q->r
时序逻辑 在所有状态下,(q->p)都成立 alw(q->r)
• 性质 3:当投票者调用 vote 函数且手中有票时,在将来某一状态下一定投票成功.从原子命题、命题逻
辑与时序逻辑这 3 个方面对性质 3 进行描述见表 8,最终使用 PPTL 公式描述性质 3 为
alw((p and r) ->som q).

Table 8 Description of property 3
表 8 性质 3 相关描述
类别 信息描述 操作符
调用 vote 函数 p
原子命题 手中有票 r
投票成功 q
调用 vote 函数且手中有票 p and r
命题逻辑
若调用 vote 函数且手中有票,则投票成功 (p and r)->q
将来某一状态下投票成功 som q
时序逻辑 若调用 vote 函数且手中有票,则将来一定投票成功 (p and r)->som q
在所有状态下,((p and r)->som q)都成立 alw((p and r)->som q)
(3) 合约完备性.
功能一致性与逻辑正确性的综合表达,只有满足功能一致性与逻辑正确性,才能认为合约满足完备性.对于
投票智能合约来说,其合约完备被描述为性质 4:性质 1~性质 3 同时满足.使用 PPTL 公式描述性质 4 为
fin(!m) and (alw(q->r)) and (alw((p and r) ->som q)).
最后,将 MSVL 模型与 PPTL 公式输入到 UMC4M 中进行验证.在验证之前,需要在 MSVL 建模程序中加入
对性质的定义,类似于代码插桩技术.
投票智能合约应满足的 PPTL 公式 fin(!m) and (alw(q->r)) and (alw((p and r)->som q))等价于 fin(!m) and
alw(!(q) or r) and alw(!(p and r) or (som q)).将上述性质输入到 p 文件中,具体如下所示:
〈/
define m: m_flag=1; //定义命题 m
define p: p_flag=1; //定义命题 p
define q: q_flag=1; //定义命题 q