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

韩宁 等:以太坊中间语言的可执行语义 1731

[6] Tolmach P, Li Y, Lin SW, Liu Y, Li ZX. A survey of smart contract formal specification and verification. arXiv:2008.02712, 2020.
[7] Yul-Solidity documentation (v0.6.1). https://solidity.readthedocs.io/en/v0.6.1/yul.html
[8] Bartoletti M, Galletta L, Murgia M. A minimal core calculus for solidity contracts. In: Pérez-Solà C, Navarro-Arribas G, Biryukov
A, García-Alfaro J, eds. Proc. of the Cryptocurrencies and Blockchain Technology on Data Privacy Management. Springer-Verlag,
2019. 233−243. [doi: 10.1007/978-3-030-31500-9_15]
[9] Nielson HR, Nielson F. Semantics with applications: An appetizer. In: Proc. of the Undergraduate Topics in Computer Science.
Springer-Verlag, 2007. 19−41. [doi: 10.1007/978-1-84628-692-6]
[10] Bhargavan K, Delignat-Lavaud A, Fournet C, Gollamudi A, Gonthier G, Kobeissi N, Kulatova N, Rastogi A, Sibut-Pinote T,
Swamy N, Zanella-Béguelin S. Formal verification of smart contracts: Short paper. In: Murray TC, Stefan D, eds. Proc. of the 2016
ACM Workshop on Programming Languages and Analysis for Security. 2016. 91−96. [doi: 10.1145/2993600.29 93611]
[11] Zakrzewski J. Towards verification of Ethereum smart contracts: A formalization of core of solidity. In: Piskac R, Rümmer P, eds.
Proc. of the Working Conf. on Verified Software: Theories, Tools and Experiments. Springer-Verlag, 2018. 229−247. [doi: 10.
1007/978-3-030-0 3592-1_ 13]
[12] Yang Z, Lei H. Lolisa: Formal syntax and semantics for a subset of the solidity programming language in mathematical tool coq. In:
Proc. of the Mathematical Problems in Engineering. 2020. [doi: 10.1155/2020/6191537]
[13] Yang Z, Lei H, Qian WZ. A hybrid formal verification system in coq for ensuring the reliability and security of ethereum-based
service smart contracts. IEEE Acess, 2020,8:21411−21436. [doi: 10.1109/ACCESS.2020.2969437]
[14] Jiao J, Lin SW, Sun J. A generalized formal semantic framework for smart contracts. In: Wehrheim H, Cabot J, eds. Proc. of the
Fundamental Approaches to Software Engineering. Springer-Verlag, 2020. 75−96. [doi: 10.1007/978-3-030-45234-6_4]
[15] Jiao J, Kan S, Lin SW, Sanan D, Liu Y, Sun J. Semantic understanding of smart contracts: Executable operational semantics of
solidity. In: Proc. of the 2020 IEEE Symp. on Security and Privacy. IEEE, 2020. 1695−1712. [doi: 10.1109/SP40000.2020. 00066]
[16] Ahrendt W, Pace GJ, Schneider G. Smart contracts: A killer application for deductive source code verification. In: Müller P,
Schaefer I, eds. Proc. of the Principled Software Development. Springer-Verlag, 2018. 1−18. [doi: 10.1007/978-3-319-98047-8_1]
[17] Sergey I, Kumar A, Hobor A. Scilla: A smart contract intermediate-level language. arXiv:1801.00687, 2018.
[18] Bernardo B, Cauderlier R, Pesin B, Tesson J. Albert, an intermediate smart-contract language for the tezos blockchain. arXiv:2001.
02630, 2020.
[19] Eth-isabelle. 2018. https://github.com/pirapira/eth-isabelle
[20] Li XM, Shi ZP, Zhang QY, Wang GH, Guan Y, Han N. Towards verifying Ethereum smart contracts at intermediate language level.
In: Ameur YA, Qin SC, eds. Proc. of the Int’l Conf. on Formal Engineering Methods. Springer-Verlag, 2019. 121−137. [doi: 10.
1007/978-3-030-32409-4_8]
[21] Hirai Y. Defining the Ethereum virtual machine for interactive theorem provers. In: Brenner M, Rohloff K, Bonneau J, Miller A,
Ryan PYA, Teague V, Bracciali A, Sala M, Pintore F, Jakobsson M, eds. Proc. of the Int’l Conf. on Financial Cryptography and
Data Security. Springer-Verlag, 2017.520−535. [doi: 10.1007/978-3-319-70278-0_33]
[22] Amani S, Bégel M, Bortin M, Staples M. Towards verifying Ethereum smart contract bytecode in Isabelle/HOL. In: Andronick J,
Felty AP, eds. Proc. of the 7th ACM SIGPLAN Int’l Conf. on Certified Programs and Proofs. ACM, 2018. 66−77. [doi:
10.1145/3167084]
[23] Grishchenko I, Maffei M, Schneidewind C. A semantic framework for the security analysis of Ethereum smart contracts. In: Bauer
L, Küsters R, eds. Proc. of the 7th Int’l Conf. on Principles of Security and Trust. Springer-Verlag, 2018. 243−269. [doi: 10.1007/
978-3-319-89722-6_10]
[24] Hildenbrandt E, Saxena M, Rodrigues N, Zhu XR, Daian P, Guth D, Moore B, Park D, Zhang Y, Ștefănescu A, Roşu G. KEVM: A
complete formal semantics of the Ethereum virtual machine. In: Proc. of the 31st Computer Security Foundations Symp. IEEE
Computer Society, 2018. 204−217. [doi: 10.1109/CSF.2018.00022]
[25] Kasampalis T, Guth D, Moore B, Șerbănuță TF, Zhang Y, Filaretti D, Serbanuta V, Johnson R, Roşu G. IELE: A rigorously
designed language and tool ecosystem for the blockchain. In: Beek MH, McIver A, Oliveira JN, eds. Proc. of the Int’l Symp. on
Formal Methods. Spinger-Verlag, 2019. 593−610. [doi: 10.1007/978-3-030-30942-8_35]
[26] Luu L, Chu DH, Olickel H, Saxena P, Hobor A. Making smart contracts smarter. In: Weippl ER, Katzenbeisser S, Kruegel C,
Myers AC, Halevi S, eds. Proc. of the 2016 ACM SIGSAC Conf. on Computer and Communications Security. ACM, 2016.
254−269. [doi: 10.1145/2976749.2978309]
[27] Permenev A, Dimitrov D, Tsankov P, Drachsler-Cohen D, Vechev M. VerX: Safety verification of smart contracts. In: Proc. of the
2020 IEEE Symp. on Security and Privacy. 2020. 1661−1677. [doi: 10.1109/SP40000.2020.00024]
[28] Li XY, Su C, Xiong Y, Huang WC, Wang WS. Formal verification of BNB smart contract. In: Proc. of the Int’l Conf. on Big Data.
IEEE, 2019. 74−78. [doi: 10.1109/BIGCOM.2019.00021]