Palina Tolmach
Yi Li
Yang Liu
Skip Abstract Section
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.
- 2016. King of the Ether Throne — Post-Mortem Investigation. Retrieved from https://www.kingoftheether.com/postmortem.html.Google Scholar
- 2018. Bamboo: A Morphing Smart Contract Language. Retrieved from https://github.com/cornellblockchain/bamboo.Google Scholar
- 2020. Common Patterns — Solidity 0.6.11 documentation. Retrieved from https://solidity.readthedocs.io/en/v0.6.11/common-patterns.html.Google Scholar
- 2020. EOS.IO Technical White Paper v2. Retrieved from https://github.com/EOSIO/Documentation/blob/master/TechnicalWhitePaper.md.Google Scholar
- Etherscan. 2020. Ethereum Charts and Statistics | Etherscan. Retrieved February 13, 2020 from https://etherscan.io/charts.Google Scholar
- 2020. Solidity — Solidity 0.6.11 documentation. Retrieved from https://solidity.readthedocs.io/en/v0.6.11/.Google Scholar
- 2020. Solidity by Example — Solidity 0.6.11 documentation. Retrieved from https://solidity.readthedocs.io/en/v0.6.11/solidity-by-example.html.Google Scholar
- 2021. Daml Programming Language. Retrieved from https://daml.com.Google Scholar
- 2021. Transaction execution approval language (TEAL) specification. Retrieved from https://developer.algorand.org/docs/reference/teal/specification.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- S. Akca, A. Rajan, and C. Peng. 2019. SolAnalyser: A framework for analysing and testing smart contracts. In Proceedings of the APSEC. 482–489.Google Scholar
- 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.Google Scholar
- 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).Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google ScholarCross Ref
- 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.Google Scholar
- P. Antonino and A. W. Roscoe. 2020. Formalising and verifying smart contracts with Solidifier: A bounded model checker for Solidity. arxiv:2002.02710.Google Scholar
- 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.Google Scholar
- A. Arusoaie. 2020. Certifying Findel Derivatives for Blockchain. arxiv:2005.13602.Google Scholar
- N. Atzei, M. Bartoletti, and T. Cimoli. 2017. A survey of attacks on ethereum smart contracts. In Proceedings of the POST. Springer, 164–186.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- J. C. M. Baeten. 2005. A brief history of process algebra. Theor. Comput. Sci. 335, 2 (2005), 131–146.Google ScholarDigital Library
- 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.Google Scholar
- R. Banach. 2020. Verification-led smart contracts. In Proceedings of the FC. Springer International Publishing, 106–121.Google ScholarCross Ref
- 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.Google Scholar
- 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.Google ScholarCross Ref
- M. Bartoletti and R. Zunino. 2019. Verifying liquidity of bitcoin contracts. In Proceedings of the POST. Springer International Publishing, 222–247.Google Scholar
- B. Beckert, M. Herda, M. Kirsten, and J. Schiffl. 2018. Formal specification and verification of hyperledger fabric chaincode. In Proceedings of the SDLT.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- B. Bernardo, R. Cauderlier, B. Pesin, and J. Tesson. 2020. Albert, an Intermediate Smart-Contract Language for the Tezos Blockchain. arxiv:2001.02630.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- S. Bragagnolo, H. Rocha, M. Denker, and S. Ducasse. 2018. SmartInspect: Solidity smart contract inspector. In Proceedings of the IEEE IWBOSE. 9–18.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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).Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- S. E. S. Crawford and E. Ostrom. 1995. A grammar of institutions. Am. Polit. Sci. Rev. 89, 3 (1995), 582–600.Google ScholarCross Ref
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google ScholarDigital Library
- 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.Google Scholar
- J. Ellul and G. J. Pace. 2018. Runtime verification of ethereum smart contracts. In Proceedings of the EDCC. IEEE, 158–163.Google Scholar
- 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.Google Scholar
- Y. Feng, E. Torlak, and R. Bodík. 2019. Precise attack synthesis for smart contracts. arxiv:1902.06067.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- F. Fournier and I. Skarbovsky. 2019. Enriching smart contracts with temporal aspects. In Proceedings of the ICBC, Vol. 11521 LNCS. Springer Verlag, 126–141.Google Scholar
- J. Frank, C. Aschermann, and T. Holz. 2020. ETHBMC: A bounded model checker for smart contracts. In Proceedings of the USENIX Security. USENIX Association.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- L. M. Goodman. 2014. Tezos — A Self-Amending Crypto-Ledger. White Paper. Retrieved from https://tezos.com/static/white_paper-2dc8c02267a8fb86bd67a108199441bf.pdf.Google Scholar
- G. Governatori. 2014. Thou shalt is not you will. CoRR abs/1404.1685 (2014).Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- NCC Group. 2018. TOP 10 — Arithmetic Issues. Retrieved from https://www.dasp.co/.Google Scholar
- S. Haber and W. S. Stornetta. 1991. How to time-stamp a digital document. J. Cryptol. 3, 2 (Jan. 1991), 99–111.Google ScholarDigital Library
- Á. Hajdu and D. Jovanović. 2019. solc-verify: A modular verifier for solidity smart contracts. arxiv:1907.04262.Google Scholar
- Á. Hajdu, D. Jovanović, and G. Ciocarlie. 2020. Formal Specification and Verification of Solidity Contracts with Events. arxiv:2005.10382.Google Scholar
- D. Harz and W. Knottenbelt. 2018. Towards safer smart contracts: A survey of languages and verification methods. arxiv:1809.09805.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Y. Hirai. 2016. Formal Verification of Deed Contract in Ethereum Name Service. Retrieved from https://yoichihirai.com/deed.pdf.Google Scholar
- Y. Hirai. 2017. Defining the ethereum virtual machine for interactive theorem provers. In Proceedings of the FC. Springer, Cham, 520–535.Google Scholar
- Y. Hirai. 2018. Blockchains as Kripke models: An analysis of atomic cross-chain swap. In Proceedings of the ISoLA. Springer International Publishing, 389–404.Google ScholarDigital Library
- G. J. Holzmann. 1997. The model checker SPIN. IEEE Trans. Softw. Eng. 23, 5 (1997), 279–295. DOI: https://doi.org/10.1109/32.588521Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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.Google Scholar
- A. Imeri, N. Agoulmine, and D. Khadraoui. 2020. Smart contract modeling and verification techniques: A survey. In Proceedings of the ADVANCE. 1–8.Google Scholar
- Runtime Verification Inc.2018. ERC20-K: Formal Executable Specification of ERC20. Retrieved from https://github.com/runtimeverification/erc20-semantics.Google Scholar
- 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.Google Scholar
- S. Kalra, S. Goel, M. Dhawan, and S. Sharma. 2018. ZEUS: Analyzing safety of smart contracts. In Proceedings of the NDSS.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- J. Kongmanee, P. Kijsanayothin, and R. Hewett. 2019. Securing smart contracts in blockchain. In Proceedings of the ACM/IEEE ASEW. 69–76.Google Scholar
- 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.Google Scholar
- J. Krupp and C. Rossow. 2018. teEther: Gnawing at ethereum to automatically exploit smart contracts. In Proceedings of the USENIX Security. ACM, 1317–1333.Google Scholar
- 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/.Google Scholar
- J. Ladleif and M. Weske. 2019. A unifying model of legal smart contracts. In Proceedings of the ER. 323–337.Google Scholar
- 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/.Google Scholar
- C. Laneve, C. S. Coen, and A. Veschetti. 2019. On the Prediction of Smart Contracts’ Behaviours. Springer International Publishing, 397–415.Google Scholar
- A. Li, J. A. Choi, and F. Long. 2020. Securing smart contract with runtime validation. In Proceedings of the ACM PLDI. ACM, 438–453.Google Scholar
- A. Li and F. Long. 2018. Detecting standard violation errors in smart contracts. arxiv:1812.07702.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- D. Magazzeni, P. Mcburney, and W. Nash. 2017. Validation and verification of smart contracts: A research agenda. Computer 50, 9 (2017), 50–57.Google ScholarDigital Library
- 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.Google Scholar
- A. Mavridou, A. Laszka, E. Stachtiari, and A. Dubey. 2019. VeriSolid: Correct-by-design smart contracts for ethereum. arxiv:1901.01292.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- B. Mueller. 2018. Smashing Ethereum Smart Contracts for Fun and Real Profit. Technical Report.Google Scholar
- S. Nakamoto. 2008. Bitcoin: A Peer-to-Peer Electronic Cash System. Retrieved July 14, (2020) from https://bitcoin.org/bitcoin.pdf/. (2008).Google Scholar
- Z. Nehai and F. Bobot. 2019. Deductive proof of ethereum smart contracts using why3. arxiv:1904.11281.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- J. B. Nielsen and B. Spitters. 2019. Smart Contract Interactions in Coq. arxiv:1911.04732.Google Scholar
- 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.Google Scholar
- R. O’Connor. 2017. Simplicity: A new language for blockchains. In Proceedings of the ACM PLAS. ACM, 107–120.Google ScholarDigital Library
- OpenZeppelin. 2020. SafeMath Library. Retrieved from https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/math/SafeMath.sol.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- D. Perez and B. Livshits. 2019. Smart contract vulnerabilities: Does anyone care?arxiv:1902.06710.Google Scholar
- 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.Google Scholar
- S. Popejoy. 2017. The Pact Smart-Contract Language. Retrieved from https://www.kadena.io/whitepapers.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- RChain. 2018. Contract Design — RChain Architecture 0.9.0 documentation. Retrieved from https://architecture-docs.readthedocs.io/contracts/contract-design.html.Google Scholar
- 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.Google Scholar
- J. Rushby. 2001. Theorem Proving for Verification. Springer Berlin, 39–57.Google Scholar
- N. F. Samreen and M. H. Alalfi. 2020. Reentrancy vulnerability identification in ethereum smart contracts. In Proceedings of the IEEE IWBOSE. 22–29.Google Scholar
- D. C. Sánchez. 2018. Raziel: Private and verifiable smart contracts on blockchains. CoRR abs/1807.09484 (2018).Google Scholar
- 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.Google Scholar
- S. Sayeed, H. Marco-Gisbert, and T. Caira. 2020. Smart contract: Attacks and protections. IEEE Access 8 (2020), 24416–24427.Google ScholarCross Ref
- C. Schneidewind, I. Grishchenko, M. Scherer, and M. Maffei. 2020. eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. arxiv:2005.06227.Google Scholar
- F. Schrans, S. Eisenbach, and S. Drossopoulou. 2018. Writing safe smart contracts in Flint. In Proceedings of the ACM Programming Companion. ACM, 218–219.Google Scholar
- I. Sergey and A. Hobor. 2017. A concurrent perspective on smart contracts. In Proceedings of the FC, Vol. 10323 LNCS. Springer Verlag, 478–493.Google Scholar
- I. Sergey, A. Kumar, and A. Hobor. 2018. Temporal properties of smart contracts. In Proceedings of the ISoLA. Springer, Cham, 323–338.Google Scholar
- 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.Google ScholarDigital Library
- E. Shishkin. 2018. Debugging smart contract’s business logic using symbolic model-checking. arxiv:1812.00619.Google Scholar
- D. Siegel. 2016. Understanding The DAO Attack — CoinDesk. Retrieved from https://www.coindesk.com/understanding-dao-hack-journalists.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- T. Sun and W. Yu. 2020. A formal verification framework for security issues of blockchain smart contracts. Electronics 9, 2 (Feb. 2020), 255.Google ScholarCross Ref
- D. Suvorov and V. Ulyantsev. 2019. Smart contract design meets state machine synthesis: Case studies. arxiv:1906.02906.Google Scholar
- Nick Szabo. 1997. Formalizing and securing relationships on public networks. First Mond. 2, 9 (Sep. 1997).Google ScholarCross Ref
- 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/.Google Scholar
- 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.Google Scholar
- P. Tolmach, Y. Li, S.-W. Lin, and Y. Liu. 2021. Formal Analysis of Composable DeFi Protocols. arxiv:2103.00540.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google ScholarCross Ref
- E. Viglianisi, M. Ceccato, and P. Tonella. 2020. A federated society of bots for smart contract testing. J. Syst. Softw. 168 (2020), 110647.Google ScholarCross Ref
- F. Vogelsteller and V. Buterin. 2015. ERC-20 Token Standard. Retrieved from https://eips.ethereum.org/EIPS/eip-20.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google ScholarCross Ref
- S. Wang, C. Zhang, and Z. Su. 2019. Detecting nondeterministic payment bugs in ethereum smart contracts. Proceedings of the ACM OOPSLA.Google Scholar
- 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/.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- G. Wood. 2014. Ethereum: A secure decentralised generalised transaction ledger. Ether. Proj. Yell. Paper 151 (2014), 1–32.Google Scholar
- W. Xu and G. A. Fink. 2019. Building Executable Secure Design Models for Smart Contracts with Formal Methods. arxiv:1912.04051.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Z. Yang and H. Lei. 2018. Lolisa: Formal syntax and semantics for a subset of the solidity programming language. CoRR abs/1803.09885 (2018).Google Scholar
- 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).Google Scholar
- X. L. Yu, O. Al-Bataineh, D. Lo, and A. Roychoudhury. 2019. Smart Contract Repair. arxiv:1912.05823.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- 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.Google ScholarCross Ref
- N. Zupan, P. Kasinathan, J. Cuellar, and M. Sauer. 2020. Secure Smart Contract Generation Based on Petri Nets. Springer Singapore, 73–98.Google Scholar
Index Terms
- A Survey of Smart Contract Formal Specification and Verification
Recommendations
Formal Modeling and Verification of Smart Contracts
ICSCA '18: Proceedings of the 2018 7th International Conference on Software and Computer ApplicationsSmart 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 engineeringIn 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