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

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

对合约进行建模,将银行转账合约与重入攻击合并为一个合约并作为 SOL2M 转换器的输入,转换结果如
图 16 所示.

Fig.16 Modeling results of SOL2M converter
图 16 SOL2M 转换器建模结果
使用 PPTL 公式描述银行转账合约应满足的性质,下面从功能一致性、逻辑正确性以及合约完备性 3 个层
面进行详细描述.
(1) 功能一致性.
对于银行转账合约来说,其 deposit 函数用于实现存钱操作.若用户调用了 deposit 函数,但用户余额没有增
加,则说明 deposit 函数没有满足实际要求,即合约不满足功能一致性.将该功能精简为性质 5:在任何状态下,若
用户调用 deposit 函数,则该用户余额在未来某一状态一定增加.从原子命题、命题逻辑、时序逻辑 3 个层面描
述性质 5 见表 9,最终使用 PPTL 公式描述性质 5 为
alw(m->som n).
Table 9 Description of property 5
表 9 性质 5 相关描述
类别 信息描述 操作符
用户调用 deposit 函数 m
原子命题
用户余额增加 n
命题逻辑 若用户调用 deposit 函数,则该用户余额一定增加 m→n
在将来某一状态下 n 一定成立 som n
时序逻辑
在所有状态下(m->som n)都成立 alw(m→som n)
(2) 逻辑正确性.
在银行转账合约中,将以太币发送至地址需要提交外部调用.一旦被攻击者劫持,将会迫使合约执行更多的
代码(即 fallback 回退函数).攻击者在 fallback 函数中回调受攻击合约的任意函数,即为重入合约.在本例中,攻击
者可以多次回调 deposit 函数实现无限取钱操作.无重入攻击的合约应当在执行完外部调用时保证没有调用合
约内所有函数.可能导致恶意情况发生的内部函数有 deposit 函数和 withDraw 函数,因此描述性质 6 为:在所有
状态下都不存在当 withDraw 函数执行完外部调用时,deposit 函数或 withDraw 函数被再次调用.从原子命题、
命题逻辑、时序逻辑这 3 个层面描述性质 6 见表 10,最终使用 PPTL 公式描述性质 6 为