research-article

A Survey of Smart Contract Formal Specification and Verification

Authors:

Palina Tolmach,

Zengxiang LiAuthors Info & Claims

ACM Computing Surveys (CSUR), Volume 54, Issue 7

Article No.: 148, Pages 1 - 38

https://doi.org/10.1145/3464421

Published: 18 July 2021 Publication History

Abstract

A smart contract is a computer program that allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal, and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work.

References

[1]

2016. King of the Ether Throne — Post-Mortem Investigation. Retrieved from https://www.kingoftheether.com/postmortem.html.

[2]

2018. Bamboo: A Morphing Smart Contract Language. Retrieved from https://github.com/cornellblockchain/bamboo.

[3]

2020. Common Patterns — Solidity 0.6.11 documentation. Retrieved from https://solidity.readthedocs.io/en/v0.6.11/common-patterns.html.

[4]

2020. EOS.IO Technical White Paper v2. Retrieved from https://github.com/EOSIO/Documentation/blob/master/TechnicalWhitePaper.md.

[5]

Etherscan. 2020. Ethereum Charts and Statistics | Etherscan. Retrieved February 13, 2020 from https://etherscan.io/charts.

[6]

2020. Solidity — Solidity 0.6.11 documentation. Retrieved from https://solidity.readthedocs.io/en/v0.6.11/.

[7]

2020. Solidity by Example — Solidity 0.6.11 documentation. Retrieved from https://solidity.readthedocs.io/en/v0.6.11/solidity-by-example.html.

[8]

2021. Daml Programming Language. Retrieved from https://daml.com.

[9]

2021. Transaction execution approval language (TEAL) specification. Retrieved from https://developer.algorand.org/docs/reference/teal/specification.

[10]

T. Abdellatif and K. L. Brousmiche. 2018. Formal verification of smart contracts based on users and blockchain behaviors models. In Proceedings of the IFIP NTMS. IEEE, 1–5.

[11]

W. Ahrendt, R. Bubel, J. Ellul, G. J. Pace, R. Pardo, V. Rebiscoul, and G. Schneider. 2019. Verification of smart contract business logic. In Proceedings of the FSEN. Springer International Publishing, Cham, 228–243.

[12]

S. Akca, A. Rajan, and C. Peng. 2019. SolAnalyser: A framework for analysing and testing smart contracts. In Proceedings of the APSEC. 482–489.

[13]

E. Albert, J. Correas, P. Gordillo, G. Román-Díez, and A. Rubio. 2019. GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. arxiv:1912.11929.

[14]

E. Albert, J. Correas, P. Gordillo, G. Román-Díez, and A. Rubio. 2019. SAFEVM: A safety verifier for ethereum smart contracts. CoRR abs/1906.04984 (2019).

[15]

S. Alqahtani, X. He, R. Gamble, and P. Mauricio. 2020. Formal verification of functional requirements for smart contract compositions in supply chain management systems. In Proceedings of the HICSS.

[16]

S. Amani, M. Bégel, M. Bortin, and M. Staples. 2018. Towards verifying ethereum smart contract bytecode in Isabelle/HOL. In Proceedings of the ACM CPP. ACM Press, 66–77.

[17]

E. Androulaki, A. Barger, V. Bortnikov, C. Cachin, K. Christidis, A. De Caro, D. Enyeart, C. Ferris, G. Laventman, and Y. Manevich. 2018. Hyperledger fabric: A distributed operating system for permissioned blockchains. In Proceedings of the EuroSys. ACM.

[18]

M. Andrychowicz, S. Dziembowski, D. Malinowski, and Ł. Mazurek. 2014. Modeling bitcoin contracts by timed automata. In Proceedings of the FORMATS. Springer International Publishing, 7–22.

[19]

D. Annenkov, J. B. Nielsen, and B. Spitters. 2020. ConCert: A smart contract certification framework in coq. In Proceedings of the ACM CCP. ACM, 215—228.

[20]

P. Antonino and A. W. Roscoe. 2020. Formalising and verifying smart contracts with Solidifier: A bounded model checker for Solidity. arxiv:2002.02710.

[21]

A. W. Appel, R. Dockins, A. Hobor, L. Beringer, J. Dodds, G. Stewart, S. Blazy, and X. Leroy. 2014. Program Logics for Certified Compilers. Cambridge University Press.

[22]

A. Arusoaie. 2020. Certifying Findel Derivatives for Blockchain. arxiv:2005.13602.

[23]

N. Atzei, M. Bartoletti, and T. Cimoli. 2017. A survey of attacks on ethereum smart contracts. In Proceedings of the POST. Springer, 164–186.

[24]

N. Atzei, M. Bartoletti, T. Cimoli, S. Lande, and R. Zunino. 2018. SoK: Unraveling bitcoin smart contracts. In Proceedings of the POST. Springer International Publishing, 217–242.

[25]

N. Atzei, M. Bartoletti, S. Lande, N. Yoshida, and R. Zunino. 2019. Developing secure bitcoin contracts with BitML. In Proceedings of the ACM ESEC/FSE. ACM, 1124–1128.

[26]

S. Azzopardi, J. Ellul, and G. J. Pace. 2019. Monitoring smart contracts: ContractLarva and open challenges beyond. In Proceedings of the RV, Vol. 11237. Springer Verlag, 113–137.

[27]

S. Azzopardi, G. J. Pace, and F. Schapachnik. 2018. On observing contracts: Deontic contracts meet smart contracts. In Proceedings of the JURIX, Vol. 313. IOS Press, 21–30.

[28]

J. C. M. Baeten. 2005. A brief history of process algebra. Theor. Comput. Sci. 335, 2 (2005), 131–146.

Digital Library

[29]

X. Bai, Z. Cheng, Z. Duan, and K. Hu. 2018. Formal modeling and verification of smart contracts. In Proceedings of the ACM ICSCA. ACM Press, 322–326.

[30]

R. Banach. 2020. Verification-led smart contracts. In Proceedings of the FC. Springer International Publishing, 106–121.

[31]

M. Bartoletti and L. Pompianu. 2017. An empirical analysis of smart contracts: Platforms, applications, and design patterns. In Proceedings of the FC, Vol. 10323 LNCS. Springer Verlag, 494–509. arxiv:1703.06322.

[32]

M. Bartoletti and R. Zunino. 2019. Formal models of bitcoin contracts: A survey. Front. Blockch. 2 (2019), 8. Retrieved from https://www.frontiersin.org/article/10.3389/fbloc.2019.00008.

[33]

M. Bartoletti and R. Zunino. 2019. Verifying liquidity of bitcoin contracts. In Proceedings of the POST. Springer International Publishing, 222–247.

[34]

B. Beckert, M. Herda, M. Kirsten, and J. Schiffl. 2018. Formal specification and verification of hyperledger fabric chaincode. In Proceedings of the SDLT.

[35]

B. Beckert, J. Schiffl, and M. Ulbrich. 2019. Smart Contracts: Application Scenarios for Program Verification. Retrieved from https://www.key-project.org/wp-content/uploads/2019/11/sc-verification.pdf.

[36]

T. Bernardi, N. Dor, A. Fedotov, S. Grossman, N. Immerman, D. Jackson, A. Nutz, L. Oppenheim, O. Pistiner, N. Rinetzky, M. Sagiv, M. Taube, J. A. Toman, and J. R. Wilcox. 2020. WIP: Finding bugs automatically in smart contracts with parameterized invariants. Retrieved from https://www.certora.com/pubs/sbc2020.pdf.

[37]

B. Bernardo, R. Cauderlier, Z. Hu, B. Pesin, and J. Tesson. 2019. Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts. arxiv:1909.08671.

[38]

B. Bernardo, R. Cauderlier, B. Pesin, and J. Tesson. 2020. Albert, an Intermediate Smart-Contract Language for the Tezos Blockchain. arxiv:2001.02630.

[39]

K. Bhargavan, N. Swamy, S. Zanella-Béguelin, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, and T. Sibut-Pinote. 2016. Formal verification of smart contracts. In Proceedings of the ACM PLAS. ACM Press, 91–96.

[40]

G. Bigi, A. Bracciali, G. Meacci, and E. Tuosto. 2015. Validation of Decentralised Smart Contracts Through Game Theory and Formal Methods. Springer International Publishing, 142–161.

[41]

S. Blackshear, D. L. Dill, S. Qadeer, C. W. Barrett, J. C. Mitchell, O. Padon, and Y. Zohar. 2020. Resources: A Safe Language Abstraction for Money. arxiv:2004.05106.

[42]

S. Bragagnolo, H. Rocha, M. Denker, and S. Ducasse. 2018. SmartInspect: Solidity smart contract inspector. In Proceedings of the IEEE IWBOSE. 9–18.

[43]

L. Brent, N. Grech, S. Lagouvardos, B. Scholz, and Y. Smaragdakis. 2020. Ethainter: A smart contract security analyzer for composite vulnerabilities. In Proceedings of the ACM PLDI. ACM, 454–469.

[44]

Lexi Brent, Anton Jurisevic, Michael Kong, Eric Liu, Francois Gauthier, Vincent Gramoli, Ralph Holz, and Bernhard Scholz. 2018. Vandal: A Scalable Security Analysis Framework for Smart Contracts. arxiv:1809.03981.

[45]

J. Chang, B. Gao, H. Xiao, J. Sun, Y. Cai, and Z. Yang. 2019. sCompile: Critical path identification and analysis for smart contracts. In Proceedings of the ICFEM. Springer International Publishing, 286–304.

[46]

J. Chapman, R. Kireev, C. Nester, and P. Wadler. 2019. System F in Agda, for fun and profit. In Proceedings of the MPC. Springer International Publishing, 255–297.

[47]

K. Chatterjee, A. K. Goharshady, and Y. Velner. 2018. Quantitative analysis of smart contracts. In Proceedings of the ESOP, Vol. 10801 LNCS. Springer Verlag, 739–767. arxiv:1801.03367.

[48]

H. Chen, M. Pendleton, L. Njilla, and S. Xu. 2020. A survey on ethereum systems security: Vulnerabilities, attacks, and defenses. ACM Comput. Surv. 53, 3 (June 2020).

Digital Library

[49]

J. Chen, X. Xia, D. Lo, and J. Grundy. 2020. Why Do Smart Contracts Self-Destruct? Investigating the Selfdestruct Function on Ethereum. arxiv:2005.07908.

[50]

T. Chen, R. Cao, T. Li, X. Luo, G. Gu, Y. Zhang, Z. Liao, H. Zhu, G. Chen, Z. He, Y. Tang, X. Lin, and X. Zhang. 2020. SODA: A generic online detection framework for smart contracts. In Proceedings of the NDSS.

[51]

T. Chen, X. Li, X. Luo, and X. Zhang. 2017. Under-optimized smart contracts devour your money. In Proceedings of the IEEE SANER. 442–446.

[52]

T. Chen, Y. Zhang, Z. Li, X. Luo, T. Wang, R. Cao, X. Xiao, and X. Zhang. 2019. TokenScope: Automatically detecting inconsistent behaviors of cryptocurrency tokens in ethereum. In Proceedings of the ACM CCS. ACM, 1503–1520.

[53]

W. Chen, T. Zhang, Z. Chen, Z. Zheng, and Y. Lu. 2020. Traveling the token world: A graph analysis of ethereum ERC20 token ecosystem. In Proceedings of the WWW. ACM, 1411–1421.

[54]

C. D. Clack and G. Vanca. 2018. Temporal aspects of smart contracts for financial derivatives. In Proceedings of the ISoLA, Vol. 11247 LNCS. Springer Verlag, 339–355. arxiv:1805.11677.

[55]

M. Coblenz, R. Oei, T. Etzel, P. Koronkevich, M. Baker, Y. Bloem, B. A. Myers, J. Sunshine, and J. Aldrich. 2019. Obsidian: Typestate and Assets for Safer Blockchain Programming. arxiv:1909.03523.

[56]

C. Colombo, J. Ellul, and G. J. Pace. 2018. Contracts over smart contracts: Recovering from violations dynamically. In Proceedings of the ISoLA, Vol. 11247 LNCS. Springer Verlag, 300–315.

[57]

S. E. S. Crawford and E. Ostrom. 1995. A grammar of institutions. Am. Polit. Sci. Rev. 89, 3 (1995), 582–600.

[58]

L. P. A. da Horta, J. S. Reis, M. Pereira, and S. M. de Sousa. 2020. WhylSon: Proving your Michelson Smart Contracts in Why3. arxiv:2005.14650.

[59]

M. di Angelo and G. Salzer. 2019. A survey of tools for analyzing ethereum smart contracts. In Proceedings of the IEEE DAPPCON. IEEE, 69–78.

[60]

T. Dickerson, P. Gazzillo, M. Herlihy, V. Saraph, and E. Koskinen. 2019. Proof-carrying smart contracts. In Proceedings of the FC. Springer Berlin, 325–338.

[61]

W. Duo, H. Xin, and M. Xiaofeng. 2020. Formal analysis of smart contract based on colored petri nets. IEEE Intell. Syst. 35, 3 (2020), 19–30.

Digital Library

[62]

T. Durieux, J. F. Ferreira, R. Abreu, and P. Cruz. 2020. Empirical review of automated analysis tools on 47,587 ethereum smart contracts. In Proceedings of the IEEE/ACM ICSE. arxiv:1910.10601.

[63]

J. Ellul and G. J. Pace. 2018. Runtime verification of ethereum smart contracts. In Proceedings of the EDCC. IEEE, 158–163.

[64]

J. Feist, G. Greico, and A. Groce. 2019. Slither: A static analysis framework for smart contracts. In Proceedings of the IEEE/ACM WETSEB. IEEE Press, 8–15.

[65]

Y. Feng, E. Torlak, and R. Bodík. 2019. Precise attack synthesis for smart contracts. arxiv:1902.06067.

[66]

C. Ferreira Torres, M. Baden, R. Norvill, and H. Jonker. 2019. ÆGIS: Smart shielding of smart contracts. In Proceedings of the ACM CCS. ACM, 2589–2591.

[67]

C. Ferreira Torres, J. Schütte, and R. State. 2018. Osiris: Hunting for integer bugs in ethereum smart contracts. In Proceedings of the ACSAC. ACM, 664–676.

[68]

F. Fournier and I. Skarbovsky. 2019. Enriching smart contracts with temporal aspects. In Proceedings of the ICBC, Vol. 11521 LNCS. Springer Verlag, 126–141.

[69]

J. Frank, C. Aschermann, and T. Holz. 2020. ETHBMC: A bounded model checker for smart contracts. In Proceedings of the USENIX Security. USENIX Association.

[70]

C. K. Frantz and M. Nowostawski. 2016. From institutions to code: Towards automated generation of smart contracts. In Proceedings of the IEEE FAS-W. IEEE, 210–215.

[71]

J. Gao, H. Liu, C. Liu, Q. Li, Z. Guan, and Z. Chen. 2019. EASYFLOW: Keep ethereum away from overflow. In Proceedings of the the IEEE/ACM ICSE-Companion. 23–26.

[72]

T. Genet, T. Jensen, and J. Sauvage. 2020. Termination of Ethereum’s Smart Contracts. Research Report. Univ Rennes, Inria, CNRS, IRISA. Retrieved from https://hal.inria.fr/hal-02555738.

[73]

L. M. Goodman. 2014. Tezos — A Self-Amending Crypto-Ledger. White Paper. Retrieved from https://tezos.com/static/white_paper-2dc8c02267a8fb86bd67a108199441bf.pdf.

[74]

G. Governatori. 2014. Thou shalt is not you will. CoRR abs/1404.1685 (2014).

[75]

G. Governatori, F. Idelberger, Z. Milosevic, R. Riveret, G. Sartor, and X. Xu. 2018. On legal contracts, imperative and declarative smart contracts, and blockchain systems. Artif. Intell. Law 26, 4 (01 Dec. 2018), 377–409.

[76]

N. Grech, L. Brent, B. Scholz, and Y. Smaragdakis. 2019. Gigahorse: Thorough, declarative decompilation of smart contracts. In Proceedings of the IEEE/ACM ICSE. 1176–1186.

[77]

N. Grech, M. Kong, A. Jurisevic, L. Brent, B. Scholz, and Y. Smaragdakis. 2018. MadMax: Surviving out-of-gas conditions in ethereum smart contracts. In Proceedings of the ACM OOPSLA.

[78]

I. Grishchenko, M. Maffei, and C. Schneidewind. 2018. A semantic framework for the security analysis of ethereum smart contracts. In Proceedings of the POST. Springer, Cham, 243–269.

[79]

A. Groce, J. Feist, G. Grieco, and M. Colburn. 2019. What are the Actual Flaws in Important Smart Contracts (and How Can We Find Them)?arxiv:1911.07567.

[80]

S. Grossman, I. Abraham, G. Golan-Gueta, Y. Michalevsky, N. Rinetzky, M. Sagiv, and Y. Zohar. 2017. Online detection of effectively callback free objects with applications to smart contracts. Proceedings of the ACM POPL.

[81]

NCC Group. 2018. TOP 10 — Arithmetic Issues. Retrieved from https://www.dasp.co/.

[82]

S. Haber and W. S. Stornetta. 1991. How to time-stamp a digital document. J. Cryptol. 3, 2 (Jan. 1991), 99–111.

Digital Library

[83]

Á. Hajdu and D. Jovanović. 2019. solc-verify: A modular verifier for solidity smart contracts. arxiv:1907.04262.

[84]

Á. Hajdu, D. Jovanović, and G. Ciocarlie. 2020. Formal Specification and Verification of Solidity Contracts with Events. arxiv:2005.10382.

[85]

D. Harz and W. Knottenbelt. 2018. Towards safer smart contracts: A survey of languages and verification methods. arxiv:1809.09805.

[86]

J. He, M. Balunovic̀, N. Ambroladze, P. Tsankov, and M. Vechev. 2019. Learning to fuzz from symbolic execution with application to smart contracts. In Proceedings of the ACM CCS. ACM, 531–548.

[87]

N. He, R. Zhang, L. Wu, H. Wang, X. Luo, Y. Guo, T. Yu, and X. Jiang. 2020. Security Analysis of EOSIO Smart Contracts. arxiv:2003.06568.

[88]

Y. Hirai. 2016. Formal Verification of Deed Contract in Ethereum Name Service. Retrieved from https://yoichihirai.com/deed.pdf.

[89]

Y. Hirai. 2017. Defining the ethereum virtual machine for interactive theorem provers. In Proceedings of the FC. Springer, Cham, 520–535.

[90]

Y. Hirai. 2018. Blockchains as Kripke models: An analysis of atomic cross-chain swap. In Proceedings of the ISoLA. Springer International Publishing, 389–404.

Digital Library

[91]

G. J. Holzmann. 1997. The model checker SPIN. IEEE Trans. Softw. Eng. 23, 5 (1997), 279–295.

Digital Library

[92]

Y. Huang, Y. Bian, R. Li, J. L. Zhao, and P. Shi. 2019. Smart contract security: A software lifecycle perspective. IEEE Access 7 (2019), 150184–150202.

[93]

Y. Huang, Q. Kong, N. Jia, X. Chen, and Z. Zheng. 2019. Recommending differentiated code to support smart contract update. In Proceedings of the IEEE/ACM ICPC. 260–270.

[94]

A. Imeri, N. Agoulmine, and D. Khadraoui. 2020. Smart contract modeling and verification techniques: A survey. In Proceedings of the ADVANCE. 1–8.

[95]

Runtime Verification Inc.2018. ERC20-K: Formal Executable Specification of ERC20. Retrieved from https://github.com/runtimeverification/erc20-semantics.

[96]

J. Jiao, S. Kan, S.-W. Lin, D. Sanán, Y. Liu, and J. Sun. 2020. Semantic understanding of smart contracts: Executable operational semantics of solidity. In Proceedings of the IEEE S&P. IEEE Computer Society, 1265–1282.

[97]

S. Kalra, S. Goel, M. Dhawan, and S. Sharma. 2018. ZEUS: Analyzing safety of smart contracts. In Proceedings of the NDSS.

[98]

T. Kasampalis, D. Guth, B. Moore, T. F. Serbanuta, Y. Zhang, D. Filaretti, V. Serbanuta, R. Johnson, and G. Roşu. 2019. IELE: A rigorously designed language and tool ecosystem for the blockchain. In Proceedings of the FM.

[99]

A. Kolluri, I. Nikolic, I. Sergey, A. Hobor, and P. Saxena. 2019. Exploiting the laws of order in smart contracts. In Proceedings of the ACM ISSTA. ACM, 363–373.

[100]

J. Kongmanee, P. Kijsanayothin, and R. Hewett. 2019. Securing smart contracts in blockchain. In Proceedings of the ACM/IEEE ASEW. 69–76.

[101]

A. Kosba, A. Miller, E. Shi, Z. Wen, and C. Papamanthou. 2016. Hawk: The blockchain model of cryptography and privacy-preserving smart contracts. In Proceedings of the IEEE S&P. 839–858.

[102]

J. Krupp and C. Rossow. 2018. teEther: Gnawing at ethereum to automatically exploit smart contracts. In Proceedings of the USENIX Security. ACM, 1317–1333.

[103]

A. Juels L. Breidenbach, P. Daian and E. G. Sirer. 2017. An In-Depth Look at the Parity Multisig Bug. Retrieved from https://hackingdistributed.com/2017/07/22/deep-dive-parity-bug/.

[104]

J. Ladleif and M. Weske. 2019. A unifying model of legal smart contracts. In Proceedings of the ER. 323–337.

[105]

P. Lamela Seijas, A. Nemish, D. Smith, and S. Thompson. 2020. Marlowe: Implementing and analysing financial contracts on blockchain. Retrieved from https://iohk.io/en/research/library/papers/marloweimplementing-and-analysing-financial-contracts-on-blockchain/.

[106]

C. Laneve, C. S. Coen, and A. Veschetti. 2019. On the Prediction of Smart Contracts’ Behaviours. Springer International Publishing, 397–415.

[107]

A. Li, J. A. Choi, and F. Long. 2020. Securing smart contract with runtime validation. In Proceedings of the ACM PLDI. ACM, 438–453.

[108]

A. Li and F. Long. 2018. Detecting standard violation errors in smart contracts. arxiv:1812.07702.

[109]

X. Li, Z. Shi, Q. Zhang, G. Wang, Y. Guan, and N. Han. 2019. Towards verifying ethereum smart contracts at intermediate language level. In Proceedings of the ICFEM. Springer International Publishing, 121–137.

[110]

X. Li, C. Su, Y. Xiong, W. Huang, and W. Wang. 2019. Formal verification of BNB smart contract. In Proceedings of the the BIGCOM. 74–78.

[111]

C. Liu, H. Liu, Z. Cao, Z. Chen, B. Chen, and B. Roscoe. 2018. ReGuard: Finding reentrancy bugs in smart contracts. In Proceedings of the IEEE/ACM ICSE. ACM, 65–68.

[112]

H. Liu, C. Liu, W. Zhao, Y. Jiang, and J. Sun. 2018. S-gram: Towards semantic-aware security auditing for ethereum smart contracts. In Proceedings of the ACM/IEEE ASE. ACM, 814–819.

[113]

Y. Liu, Y. Li, S.-W. Lin, and R. Zhao. 2020. Towards automated verification of smart contract fairness. In Proceedings of the ACM ESEC/FSE.

[114]

Y. Liu, J. Sun, and J. S. Dong. 2011. PAT 3: An extensible architecture for building multi-domain model checkers. In Proceedings of the IEEE ISSRE.

[115]

Z. Liu and J. Liu. 2019. Formal verification of blockchain smart contract based on colored petri net models. In Proceedings of the IEEE COMPSAC. IEEE, 555–560.

[116]

L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor. 2016. Making smart contracts smarter. In Proceedings of the ACM CCS. ACM, 254–269.

[117]

F. Ma, Y. Fu, M. Ren, M. Wang, Y. Jiang, K. Zhang, H. Li, and X. Shi. 2019. EVM*: From offline detection to online reinforcement for ethereum virtual machine. In Proceedings of the IEEE SANER. 554–558.

[118]

G. Madl, L. Bathen, G. Flores, and D. Jadav. 2019. Formal verification of smart contracts using interface automata. In Proceedings of the IEEE Blockchain. 556–563.

[119]

D. Magazzeni, P. Mcburney, and W. Nash. 2017. Validation and verification of smart contracts: A research agenda. Computer 50, 9 (2017), 50–57.

Digital Library

[120]

D. B. Maksimov, I. A. Yakimov, and A. S. Kuznetsov. 2020. Statistical model checking for blockchain-based applications. IOP Conf. Ser. Mater. Sci. Eng. 734 (Jan. 2020), 012152.

[121]

A. Mavridou, A. Laszka, E. Stachtiari, and A. Dubey. 2019. VeriSolid: Correct-by-design smart contracts for ethereum. arxiv:1901.01292.

[122]

A. Miller, Z. Cai, and S. Jha. 2018. Smart contracts and opportunities for formal methods. In Proceedings of the ISoLA, Vol. 11247 LNCS. Springer Verlag, 280–299.

[123]

C. Molina-Jimenez, I. Sfyrakis, E. Solaiman, I. Ng, M. Weng Wong, A. Chun, and J. Crowcroft. 2018. Implementation of smart contracts using hybrid architectures with on and off-blockchain components. In Proceedings of the IEEE SC2. 83–90.

[124]

M. Mossberg, F. Manzano, E. Hennenfent, A. Groce, G. Grieco, J. Feist, T. Brunson, and A. Dinaburg. 2019. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In Proceedings of the ACM/IEEE ASE. 1186–1189.

[125]

B. Mueller. 2018. Smashing Ethereum Smart Contracts for Fun and Real Profit. Technical Report.

[126]

S. Nakamoto. 2008. Bitcoin: A Peer-to-Peer Electronic Cash System. Retrieved July 14, (2020) from https://bitcoin.org/bitcoin.pdf/. (2008).

[127]

Z. Nehai and F. Bobot. 2019. Deductive proof of ethereum smart contracts using why3. arxiv:1904.11281.

[128]

Z. Nehai, P. Piriou, and F. Daumas. 2018. Model-checking of smart contracts. In Proceedings of the IEEE iThings/GreenCom/CPSCom/SmartData. IEEE, 980–987.

[129]

K. Nelaturu, A. Mavridou, A. Veneris, and A. Laszka. 2020. Verified development and deployment of multiple interacting smart contracts with verisolid. Retrieved from http://www.eecg.utoronto.ca/ veneris/20ICBC.pdf.

[130]

J. B. Nielsen and B. Spitters. 2019. Smart Contract Interactions in Coq. arxiv:1911.04732.

[131]

I. Nikolić, A. Kolluri, I. Sergey, P. Saxena, and A. Hobor. 2018. Finding the greedy, prodigal, and suicidal contracts at scale. Proceedings of the ACSAC.

[132]

R. O’Connor. 2017. Simplicity: A new language for blockchains. In Proceedings of the ACM PLAS. ACM, 107–120.

Digital Library

[133]

OpenZeppelin. 2020. SafeMath Library. Retrieved from https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/math/SafeMath.sol.

[134]

R. M. Parizi, A. Singh, and A. Dehghantanha. 2018. Smart contract programming languages on blockchains: An empirical evaluation of usability and security. In Proceedings of the ICBC, Vol. 10974 LNCS. Springer Verlag, 75–91.

[135]

D. Park, Y. Zhang, M. Saxena, P. Daian, and G. Roşu. 2018. A formal verification tool for ethereum VM bytecode. In Proceedings of the ACM ESEC/FSE. ACM, 912–915.

[136]

D. Perez and B. Livshits. 2019. Smart contract vulnerabilities: Does anyone care?arxiv:1902.06710.

[137]

A. Permenev, D. Dimitrov, P. Tsankov, D. Drachsler-Cohen, and M. Vechev. 2020. VerX: Safety verification of smart contracts. In Proceedings of the IEEE S&P. IEEE Computer Society, 414–430.

[138]

S. Popejoy. 2017. The Pact Smart-Contract Language. Retrieved from https://www.kadena.io/whitepapers.

[139]

P. Praitheeshan, L. Pan, J. Yu, J. Liu, and R. Doss. 2019. Security analysis methods on ethereum smart contract vulnerabilities: A survey. arxiv:1908.08605.

[140]

D. Prechtel, T. Groß, and T. Müller. 2019. Evaluating spread of “gasless send” in ethereum smart contracts. In Proceedings of the IFIP NTMS. 1–6.

[141]

M. Qu, X. Huang, X. Chen, Y. Wang, X. Ma, and D. Liu. 2018. Formal verification of smart contracts from the perspective of concurrency. In Proceedings of the SmartBlock, Vol. 11373 LNCS. Springer Verlag, 32–43.

[142]

RChain. 2018. Contract Design — RChain Architecture 0.9.0 documentation. Retrieved from https://architecture-docs.readthedocs.io/contracts/contract-design.html.

[143]

J. S. Reis, P. Crocker, and S. M. de Sousa. 2020. Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts. arxiv:2005.11839.

[144]

J. Rushby. 2001. Theorem Proving for Verification. Springer Berlin, 39–57.

[145]

N. F. Samreen and M. H. Alalfi. 2020. Reentrancy vulnerability identification in ethereum smart contracts. In Proceedings of the IEEE IWBOSE. 22–29.

[146]

D. C. Sánchez. 2018. Raziel: Private and verifiable smart contracts on blockchains. CoRR abs/1807.09484 (2018).

[147]

N. Sato, T. Tateishi, and S. Amano. 2018. Formal requirement enforcement on smart contracts based on linear dynamic logic. In Proceedings of the IEEE iThings/GreenCom/CPSCom/SmartData. 945–954.

[148]

S. Sayeed, H. Marco-Gisbert, and T. Caira. 2020. Smart contract: Attacks and protections. IEEE Access 8 (2020), 24416–24427.

[149]

C. Schneidewind, I. Grishchenko, M. Scherer, and M. Maffei. 2020. eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. arxiv:2005.06227.

[150]

F. Schrans, S. Eisenbach, and S. Drossopoulou. 2018. Writing safe smart contracts in Flint. In Proceedings of the ACM Programming Companion. ACM, 218–219.

[151]

I. Sergey and A. Hobor. 2017. A concurrent perspective on smart contracts. In Proceedings of the FC, Vol. 10323 LNCS. Springer Verlag, 478–493.

[152]

I. Sergey, A. Kumar, and A. Hobor. 2018. Temporal properties of smart contracts. In Proceedings of the ISoLA. Springer, Cham, 323–338.

[153]

I. Sergey, V. Nagaraj, J. Johannsen, A. Kumar, A. Trunov, and K. C. G. Hao. 2019. Safer smart contract programming with Scilla. Proceedings of the ACM OOPSLA.

Digital Library

[154]

E. Shishkin. 2018. Debugging smart contract’s business logic using symbolic model-checking. arxiv:1812.00619.

[155]

D. Siegel. 2016. Understanding The DAO Attack — CoinDesk. Retrieved from https://www.coindesk.com/understanding-dao-hack-journalists.

[156]

A. Singh, R. Parizi, Q. Zhang, K.-K. R. Choo, and A. Dehghantanha. 2019. Blockchain smart contracts formalization: Approaches and challenges to address vulnerabilities. Comput. Secur. 88 (10 2019), 101654.

[157]

S. So, M. Lee, J. Park, H. Lee, and H. Oh. 2020. VeriSmart: A highly precise safety verifier for ethereum smart contracts. In Proceedings of the IEEE S&P. IEEE Computer Society, 825–841.

[158]

F. Spoto. 2020. Enforcing determinism of Java smart contracts. In Proceedings of the FC, Matthew Bernhard, Andrea Bracciali, L. Jean Camp, Shin’ichiro Matsuo, Alana Maurushat, Peter B. Rønne, and Massimiliano Sala (Eds.). Springer International Publishing, Cham, 568–583.

[159]

S. Steffen, B. Bichsel, M. Gersbach, N. Melchior, P. Tsankov, and M. Vechev. 2019. zkay: Specifying and enforcing data privacy in smart contracts. In Proceedings of the ACM CCS. ACM, 1759–1776.

[160]

J. Sun, Y. Liu, and J. S. Dong. 2008. Model checking CSP revisited: Introducing a process analysis toolkit. In Proceedings of the ISoLA. Springer Berlin.

[161]

T. Sun and W. Yu. 2020. A formal verification framework for security issues of blockchain smart contracts. Electronics 9, 2 (Feb. 2020), 255.

[162]

D. Suvorov and V. Ulyantsev. 2019. Smart contract design meets state machine synthesis: Case studies. arxiv:1906.02906.

[163]

Nick Szabo. 1997. Formalizing and securing relationships on public networks. First Mond. 2, 9 (Sep. 1997).

[164]

Parity Technologies. 2017. A Postmortem on the Parity Multi-Sig Library Self-Destruct — Parity Technologies. Retrieved from https://www.parity.io/a-postmortem-on-the-parity-multi-sig-library-self-destruct/.

[165]

S. Tikhomirov, E. Voskresenskaya, I. Ivanitskiy, R. Takhaviev, E. Marchenko, and Y. Alexandrov. 2018. SmartCheck: Static analysis of ethereum smart contracts. In Proceedings of the IEEE/ACM WETSEB. 9–16.

[166]

P. Tolmach, Y. Li, S.-W. Lin, and Y. Liu. 2021. Formal Analysis of Composable DeFi Protocols. arxiv:2103.00540.

[167]

C. Ferreira Torres, M. Steichen, and R. State. 2019. The art of the scam: Demystifying honeypots in ethereum smart contracts. In Proceedings of the USENIX Security. USENIX Association, 1591–1607.

[168]

P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. Bünzli, and M. Vechev. 2018. Securify: Practical security analysis of smart contracts. In Proceedings of the ACM CCS. ACM, 67–82.

[169]

R. v. d. Meyden. 2019. On the specification and verification of atomic swap smart contracts (extended abstract). In Proceedings of the IEEE ICBC. 176–179.

[170]

E. Viglianisi, M. Ceccato, and P. Tonella. 2020. A federated society of bots for smart contract testing. J. Syst. Softw. 168 (2020), 110647.

[171]

F. Vogelsteller and V. Buterin. 2015. ERC-20 Token Standard. Retrieved from https://eips.ethereum.org/EIPS/eip-20.

[172]

H. Wang, Y. Li, S.-W. Lin, C. Artho, L. Ma, and Y. Liu. 2019. Oracle-Supported Dynamic Exploit Generation for Smart Contracts. arxiv:1909.06605.

[173]

H. Wang, Y. Li, S.-W. Lin, L. Ma, and Y. Liu. 2019. VULTRON: Catching vulnerable smart contracts once and for all. In Proceedings of the IEEE/ACM ICSE. IEEE Press, 1–4.

[174]

S. Wang, L. Ouyang, Y. Yuan, X. Ni, X. Han, and F.-Y. Wang. 2019. Blockchain-enabled smart contracts: Architecture, applications, and future trends. IEEE Trans. Syst., Man, Cybern. Syst. (Feb. 2019), 1–12.

[175]

S. Wang, C. Zhang, and Z. Su. 2019. Detecting nondeterministic payment bugs in ethereum smart contracts. Proceedings of the ACM OOPSLA.

[176]

Y. Wang, S. Lahiri, S. Chen, R. Pan, I. Dillig, C. Born, and I. Naseer. 2019. Formal Specification and Verification of Smart Contracts for Azure Blockchain. Retrieved from https://www.microsoft.com/en-us/research/publication/formal-specification-and-verification-of-smart-contracts-for-azure-blockchain/.

[177]

K. Weiss and J. Schütte. 2019. Annotary: A concolic execution system for developing secure smart contracts. In Proceedings of the ESORICS. Springer International Publishing, 747–766.

[178]

M. Wohrer and U. Zdun. 2018. Design patterns for smart contracts in the ethereum ecosystem. In Proceedings of the IEEE iThings/GreenCom/CPSCom/SmartData. IEEE, 1513–1520.

[179]

G. Wood. 2014. Ethereum: A secure decentralised generalised transaction ledger. Ether. Proj. Yell. Paper 151 (2014), 1–32.

[180]

W. Xu and G. A. Fink. 2019. Building Executable Secure Design Models for Smart Contracts with Formal Methods. arxiv:1912.04051.

[181]

X. Xu, C. Pautasso, L. Zhu, Q. Lu, and I. Weber. 2018. A pattern collection for blockchain-based applications. In Proceedings of the ACM EuroPLoP. ACM, ACM.

[182]

K. Yamashita, Y. Nomura, E. Zhou, B. Pi, and S. Jun. 2019. Potential risks of hyperledger fabric smart contracts. In Proceedings of the IEEE IWBOSE. 1–10.

[183]

Z. Yang and H. Lei. 2018. Lolisa: Formal syntax and semantics for a subset of the solidity programming language. CoRR abs/1803.09885 (2018).

[184]

Z. Yang, H. Lei, and W. Qian. 2019. A hybrid formal verification system in Coq for ensuring the reliability and security of ethereum-based service smart contracts. CoRR abs/1902.08726 (2019).

[185]

X. L. Yu, O. Al-Bataineh, D. Lo, and A. Roychoudhury. 2019. Smart Contract Repair. arxiv:1912.05823.

[186]

F. Zhang, E. Cecchetti, K. Croman, A. Juels, and E. Shi. 2016. Town Crier: An authenticated data feed for smart contracts. In Proceedings of the ACM CCS. ACM, 270–282.

[187]

X. Zhang, Y. Li, and M. Sun. 2020. Towards a formally verified EVM in production environment. In Proceedings of the COORDINATION. Springer International Publishing, 341–349.

[188]

Z. Zheng, S. Xie, H.-N. Dai, W. Chen, X. Chen, J. Weng, and M. Imran. 2020. An overview on smart contracts: Challenges, advances and platforms. Fut. Gen. Comput. Syst. 105 (2020), 475–491.

Digital Library

[189]

E. Zhou, S. Hua, B. Pi, J. Sun, Y. Nomura, K. Yamashita, and H. Kurihara. 2018. Security assurance for smart contract. In Proceedings of the IFIP NTMS. 1–5.

[190]

J. Zhu, K. Hu, M. Filali, J.-P. Bodeveix, and J.-P. Talpin. 2020. Formal Verification of Solidity contracts in Event-B. arxiv:2005.01261.

[191]

W. Zou, D. Lo, P. S. Kochhar, X.-B. D. Le, X. Xia, Y. Feng, Z. Chen, and B. Xu. 2019. Smart contract development: Challenges and opportunities. IEEE Trans. Softw. Eng. (Sep. 2019), 1–1.

[192]

N. Zupan, P. Kasinathan, J. Cuellar, and M. Sauer. 2020. Secure Smart Contract Generation Based on Petri Nets. Springer Singapore, 73–98.

Cited By

Lahami MJmal Maalej AKrichen M(2025)A systematic literature review on dynamic testing of blockchain oriented softwareScience of Computer Programming10.1016/j.scico.2024.103211240(103211)Online publication date: Feb-2025
https://doi.org/10.1016/j.scico.2024.103211
Sankar JDavid A(2024)Transforming the Travel LandscapeDecentralizing the Online Experience With Web3 Technologies10.4018/979-8-3693-1532-3.ch012(246-266)Online publication date: 15-Mar-2024
https://doi.org/10.4018/979-8-3693-1532-3.ch012
Adda M(2024)Formal Language for Objects’ TransactionsStandards10.3390/standards40300084:3(133-153)Online publication date: 15-Aug-2024
https://doi.org/10.3390/standards4030008
Show More Cited By

Index Terms

A Survey of Smart Contract Formal Specification and Verification
1. General and reference
  1. Document types
    1. Surveys and overviews
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software notations and tools
    1. System description languages
      1. Specification languages

Recommendations

Formal Modeling and Verification of Smart Contracts
ICSCA '18: Proceedings of the 2018 7th International Conference on Software and Computer Applications

Smart contracts can automatically perform the contract terms according to the received information, and it is one of the most important research fields in digital society. The core of smart contracts is algorithm contract, that is, the parties reach an ...
Formal specification at model-level of model-driven engineering using modelling techniques

Nowadays Model-Driven Engineering (MDE) is gaining more popularity due to high-level development leading to a faster generation of executable code, which reduces manual intervention. Verification is crucial at different levels of model-based development. ...
The echo approach to formal verification
ICSE '06: Proceedings of the 28th international conference on Software engineering

In this research abstract, we propose Echo: a general formal verification approach that combines theorem proving, model checking, and code-level tools to show an implementation's compliance with its formal specification. We believe that this approach is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Computing Surveys

ACM Computing Surveys Volume 54, Issue 7

September 2022

778 pages

ISSN:0360-0300

EISSN:1557-7341

DOI:10.1145/3476825

Editor:
Albert Zomaya
University of Sydney, Australia

Issue’s Table of Contents

Copyright © 2021 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 July 2021

Accepted: 01 April 2021

Revised: 01 April 2021

Received: 01 July 2020

Published in CSUR Volume 54, Issue 7

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

92
Total Citations
View Citations
2,641
Total Downloads

Downloads (Last 12 months)551
Downloads (Last 6 weeks)54

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lahami MJmal Maalej AKrichen M(2025)A systematic literature review on dynamic testing of blockchain oriented softwareScience of Computer Programming10.1016/j.scico.2024.103211240(103211)Online publication date: Feb-2025
https://doi.org/10.1016/j.scico.2024.103211
Sankar JDavid A(2024)Transforming the Travel LandscapeDecentralizing the Online Experience With Web3 Technologies10.4018/979-8-3693-1532-3.ch012(246-266)Online publication date: 15-Mar-2024
https://doi.org/10.4018/979-8-3693-1532-3.ch012
Adda M(2024)Formal Language for Objects’ TransactionsStandards10.3390/standards40300084:3(133-153)Online publication date: 15-Aug-2024
https://doi.org/10.3390/standards4030008
Yan Q(2024)A Study of the Impact of Smart Contract Technology on the Understanding and Application of Contract Law from the Perspective of the Legal ProfessionApplied Mathematics and Nonlinear Sciences10.2478/amns-2024-22389:1Online publication date: 5-Aug-2024
https://doi.org/10.2478/amns-2024-2238
Wei ZSun JZhang ZZhang XYang XZhu L(2024)Survey on Quality Assurance of Smart ContractsACM Computing Surveys10.1145/3695864Online publication date: 14-Sep-2024
https://doi.org/10.1145/3695864
Song SChen JChen TLuo XLi TYang WWang LZhang WLuo FHe ZLu YLi PChristakis MPradel M(2024)Empirical Study of Move Smart Contract Security: Introducing MoveScan for Enhanced AnalysisProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3680391(1682-1694)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3680391
Jiao TXu ZQi MWen SXiang YNan G(2024)A Survey of Ethereum Smart Contract Security: Attacks and DetectionDistributed Ledger Technologies: Research and Practice10.1145/36438953:3(1-28)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3643895
Ali IAbdallah M(2024)On Off-Chaining Smart Contract Runtime Protection: A Queuing Model ApproachIEEE Transactions on Parallel and Distributed Systems10.1109/TPDS.2024.338915335:8(1345-1359)Online publication date: 16-Apr-2024
https://dl.acm.org/doi/10.1109/TPDS.2024.3389153
Augusto ABelchior RCorreia MVasconcelos AZhang LHardjono T(2024)SoK: Security and Privacy of Blockchain Interoperability2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00255(3840-3865)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00255
Kumar Avon Hippel MManolios PNita-Rotaru C(2024)Formal Model-Driven Analysis of Resilience of GossipSub to Attacks from Misbehaving Peers2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00017(2142-2160)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00017
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Media

Figures

Other

Tables

View Issue’s Table of Contents