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

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

definition gstk_token_contract where
“gstk_token_contract=〈([(mytoken_code,ls_init,(get_func_values mytoken_code),None) B ]),gs_init,
CKDummy〉 N #[ ]”
全局状态 gs_init 中,交易发送方地址(saddr gs_init)为 0xCA35b7d915458EF540aDe6068dFe2F44E8fa733c;
交易输入数据(input gs_init)的前 4 字节分别为 0xa9,0x05,0x9c 和 0xbb,使得派遣程序能够将对合约的调用转向
其中的 transfer_func.由第 5 字节到第 36 字节均为 0x0,表示 transfer_func 的第 1 个实参为 0x0,向该地址转账,
而由第 36 字节到第 68 字节为 0x0 … 0x0 0x1 0x0 0x0 0x0 0x0(即只有第 64 字节为 0x1,其余字节为 0x0),表示
32
transfer_func 的第 2 个实参为 2 =4294967296,亦即转移代币的数量.此外,全局状态 gs_init 中当前账户地址指
向合约账户 mytoken_account.
该账户的存储中,对应于代币发送方账户地址 addr 0 =0xCA35b7d915458EF540aDe6068dFe2F44E8fa733c 的
代币余额为 99 999 999 999,对应于代币接收方账户地址 0x0 的代币余额为 10 000 000 000.
定义两个辅助函数帮助观察合约执行后发生的代币余额变化,其中,函数 get_val_from_storage 实现从全局
栈顶取出指定存储地址所存放的值的功能,函数 get_balance_offset 获取指定账户的代币余额在 mytoken_
account 账户存储中的偏移量.初始时,代币发送和接收账户的代币余额如下所示.
value “get_val_from_storage (multi_step tre0_ex1 结果:(“Some 99999999999”::
gstk_token_contract 0) (get_balance_offset addr 0)” “256 word option”)
value “get_val_from_storage (multi_step tre0_ex1 结果:(“Some 10000000000”::
gstk_token_contract 0) (get_balance_offset 0x0)” “256 word option”)
函数 transfer_func 执行后,发送和接收账户的代币余额如下所示:
value “get_val_from_storage (multi_step tre0_ex1 结果:(“Some 95705032703”::
gstk_token_contract 270) (get_balance_offset addr 0)” “256 word option”)
value “get_val_from_storage (multi_step tre0_ex1 结果:(“Some 14294967296”::
gstk_token_contract 270) (get_balance_offset 0x0)” “256 word option”)
发送 方代币余额为 99999999999−4294967296=95705032703, 而接收方代 币余额为 10000000000+
4294967296=14294967296.这印证了 transfer_func 函数的代币转移功能.

7 结论与展望

为支撑面向中间语言层、基于定理证明的智能合约形式化验证,本工作在 Isabelle/HOL 中给出了以太坊中
间语言 Yul 的形式化,包括该语言类型系统和小步语义的首个已知的形式化,从而形成了 Yul 语言的形式化规
范.通过创建由 120 个 Yul 语言程序所组成的测试集对形式化语义进行了系统测试,印证了形式化语义对 Yul
语言文档的直观规范以及实际观察的合约执行行为的如实反映.在本文中,通过一个 ERC20 代币合约的案例演
示了类型系统和语义在 Isabelle/HOL 中的执行.除去测试与案例,本工作包含约 2 800 行形式化代码.
本项目当前尚未完成的工作主要为 Yul 语言类型系统保型性(type preservation)的形式化证明,即,在
Isabelle/HOL 中证明表达式和代码块的良类型被小步执行所保持.目前已给出保型性所涉及的关于执行状态的
不变式,并基本完成了保型性的纸笔验证.后续工作中,我们将首先在 Isabelle/HOL 中完成保型性证明,而后,基于
Yul 语言形式化规范开展中间语言层以太坊智能合约的形式化证明工作——重点为安全属性的验证.

References:
[1] Yaga D, Mell P, Roby N, Scarfone K. Blockchain technology overview. U.S., National Institute of Standards and Technology, 2018:
1−6. [doi: 10.6028/NIST.IR.8202]
[2] Wood G. Ethereum: A secure decentralized generalized transaction ledger. Ethereum Project Yellow Paper, 2014,151(2014):1−32.
[3] Li XQ, Jiang P, Chen T, Luo XP, Wen QY. A survey on the security of blockchain systems. Future Generation Computer Systems,
2020,107:841−853. [doi: 10.1016/j.future.2017.08.020]
[4] CNVD blockchain vulnerability sub-library. 2020. https://bc.cnvd.org.cn/statistics
[5] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):33−61 (in
Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm [doi: 10.13328/j.cnki.jos.005652]