SpringerLink
Log in

Comparison of Ethereum Smart Contract Analysis and Verification Methods

  • Conference paper
  • First Online:
Computer Security. ESORICS 2023 International Workshops (ESORICS 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14398))

Included in the following conference series:

  • 231 Accesses

Abstract

Ethereum allows to publish and use applications known as smart contracts on its public network.

Smart contracts can be costly for users if erroneous. Various security vulnerabilities have occurred in the past and have been exploited causing the loss of billions of dollars. Therefore, it is in the developer’s interest to publish smart contracts that serve their intended purpose only.

In this work, we study different approaches to verify if Ethereum smart contracts behave as intended and how to detect possible vulnerabilities. To this end, we compare and evaluate, different formal verification tools and tools to automatically detect vulnerabilities. Our empirical comparison of 140 smart contracts with known vulnerabilities shows that different tools vary in their success to identify issues with smart contracts. In general, we find that automated analysis tools often miss vulnerabilities, while formal verifiers based on model checking with Hoare-style source code annotations require high effort and knowledge to discover possible weaknesses. Specifically, some vulnerabilities (e.g., related to bad randomness) are not detected by any of the tools. Formal verifiers perform better than automated analysis tools as they detect more vulnerabilities and are more reliable. One of the automated analysis tools was able to find only three out of 16 Access Control vulnerabilities. On the contrary, formal verifiers have a hundred percent detection rate for selected tests.

As a case study with a smart contract without previously known vulnerabilities and for a more in-depth evaluation, we examine a smart contract using a two-phase commit protocol mechanism which is key in many smart contract applications. We use the presented tools to analyze and verify the contract. Thereby we come across different important patterns to detect vulnerabilities e.g. with respect to re-entrancy, and how to annotate a contract to prove that intended the restriction and requirements hold at any time.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 79.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Since Solidity version 0.8.0 uint cannot overflow/underflow anymore [4].

References

  1. Awosika, E., Richards, S., et al.: Formal verification of smart contracts (2022). https://github.com/ethereum/ethereum-org-website/blob/dev/src/content/developers/docs/smart-contracts/formal-verification/index.md

  2. InterFi Network: Smart-Contract-Audits (2023). https://github.com/interfinetwork/smart-contract-audits

  3. Hajdu, A., et al.: Solc-verify-readme.md (2021). https://github.com/SRI-CSL/solidity/blob/boogie/SOLC-VERIFY-README.md

  4. chriseth et al.: Version 0.8.0 (2020). https://github.com/ethereum/solidity/releases/tag/v0.8.0

  5. agaperste et al.: Smart Contracts Created (Granular) (2023). https://dune.com/queries/688911

  6. J.F.F., et al.: Smartbugs-Curated (2022). https://github.com/smartbugs/smartbugs-curated/tree/main/dataset

  7. Almakhour, M., Sliman, L., Samhat, A.E., Mellouk, A.: Verification of smart contracts: a survey. Pervas. Mob. Comput. 67, 101227 (2020)

    Article  Google Scholar 

  8. Antonino, P., Roscoe, A.: Formalising and verifying smart contracts with solidifier: a bounded model checker for solidity. ar**v preprint ar**v:2002.02710 (2020)

  9. Antonopoulos, A.M., Wood, G.: Mastering Ethereum: Building Smart Contracts and Dapps. O’reilly Media (2018)

    Google Scholar 

  10. Behan, S.: Solidity Smart Contract Testing with Static Analysis Tools. Master’s thesis, Dublin, National College of Ireland (2022). https://norma.ncirl.ie/5932/. Submitted

  11. Bernardi, T., et al.: Wip: finding bugs automatically in smart contracts with parameterized invariants (2020)

    Google Scholar 

  12. Bernhard Mueller, F.I.E.A.: Mythril (2017). https://github.com/ConsenSys/mythril

  13. Bertot, Y., Castéran, P.: Interactive theorem proving and program development. In: Coq’Art: The Calculus of Inductive Constructions. Springer (2013)

    Google Scholar 

  14. CertiK: Certik - Securing the web3 World (2022). https://www.certik.com/

  15. Chriseth, Liu, D., et al.: Solidity (2016). https://github.com/ethereum/solidity/blob/develop/docs/security-considerations.rst

  16. Di Angelo, M., Salzer, G.: A survey of tools for analyzing ethereum smart contracts. In: 2019 IEEE International Conference on Decentralized Applications and Infrastructures (DAPPCON), pp. 69–78. IEEE (2019)

    Google Scholar 

  17. Dika, A., Nowostawski, M.: Security vulnerabilities in ethereum smart contracts. In: 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData), pp. 955–962. IEEE (2018)

    Google Scholar 

  18. Durieux, T., Ferreira, J.F., Abreu, R., Cruz, P.: Empirical review of automated analysis tools on 47,587 ethereum smart contracts. In: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, pp. 530–541 (2020)

    Google Scholar 

  19. Ethereum. Goerli Testnet Explorer (2015). https://goerli.etherscan.io/

  20. Ethereum. The Native IDE for Web3 Development (2018). https://remix.ethereum.org/

  21. Feist, J., Grieco, G., Groce, A.: Slither: a static analysis framework for smart contracts. In: 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), pp. 8–15 (2019). https://doi.org/10.1109/WETSEB.2019.00008

  22. Ferreira, J.F., Cruz, P., Durieux, T., Abreu, R.: Smartbugs: a framework to analyze solidity smart contracts. In: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, pp. 1349–1352 (2020)

    Google Scholar 

  23. Hajdu, A.: Solidity Summit Demo (2022). https://github.com/hajduakos/solidity-summit-demo

  24. Hajdu, Á., Jovanović, D.: solc-verify: a modular verifier for Solidity smart contracts. In: Chakraborty, S., Navas, J.A. (eds.) Verified Software. Theories, Tools, and Experiments. LNCS, vol. 12301, pp. 161–179. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-41600-3_11

  25. Hajdu, Á., Jovanović, D., Ciocarlie, G.: Formal specification and verification of solidity contracts with events. ar**v preprint ar**v:2005.10382 (2020)

  26. Happersberger, V.: Contract of the two-phase commit smart contract (2023). https://goerli.etherscan.io/address/0x6e972a23da401321820ff121c2e41e43140b3dd1/#code

  27. Harz, D., Knottenbelt, W.: Towards safer smart contracts: a survey of languages and verification methods. ar**v preprint ar**v:1809.09805 (2018)

  28. He, D., Deng, Z., Zhang, Y., Chan, S., Cheng, Y., Guizani, N.: Smart contract vulnerability analysis and security audit. IEEE Network 34(5), 276–282 (2020). https://doi.org/10.1109/MNET.001.1900656

    Article  Google Scholar 

  29. Ivančić, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Efficient sat-based bounded model checking for software verification. Theoret. Comput. Sci. 404(3), 256–274 (2008)

    Article  MathSciNet  Google Scholar 

  30. Nikolic, I.: Maian (2018). https://github.com/ivicanikolicsg/MAIAN

  31. Kaleem, M., Mavridou, A., Laszka, A.: Vyper: a security comparison with solidity based on common vulnerabilities. In: 2020 2nd Conference on Blockchain Research and Applications for Innovative Networks and Services (BRAINS), pp. 107–111 (2020). https://doi.org/10.1109/BRAINS49436.2020.9223278

  32. Kalra, S., Goel, S., Dhawan, M., Sharma, S.: Zeus: analyzing safety of smart contracts. In: NDSS, pp. 1–12 (2018)

    Google Scholar 

  33. Kongmanee, J., Kijsanayothin, P., Hewett, R.: Securing smart contracts in blockchain. In: 2019 34th IEEE/ACM International Conference on Automated Software Engineering Workshop (ASEW), pp. 69–76 (2019). https://doi.org/10.1109/ASEW.2019.00032

  34. Lee, W.M.: Using the metamask chrome extension. In: Beginning Ethereum Smart Contracts Programming, pp. 93–126. Springer (2019)

    Google Scholar 

  35. Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 254–269 (2016)

    Google Scholar 

  36. Marks, B., Yang, H., Na, Y.: Two-phase commit using blockchain (2022). https://www.scs.stanford.edu/22spcs244b/projects/TwoPhase%20Commit%20Using%20Blockchain.pdf

  37. Mohanta, B.K., Panda, S.S., Jena, D.: An overview of smart contract and use cases in blockchain technology. In: 2018 9th International Conference on Computing, Communication and Networking Technologies (ICCCNT), pp. 1–4 (2018). https://doi.org/10.1109/ICCCNT.2018.8494045

  38. Murray, Y., Anisi, D.A.: Survey of formal verification methods for smart contracts on blockchain. In: 2019 10th IFIP International Conference on New Technologies, Mobility and Security (NTMS), pp. 1–6. IEEE (2019)

    Google Scholar 

  39. NCC Group + Contributors: Dasp - Top 10. https://dasp.co/

  40. Nehaï, Z., Piriou, P.Y., Daumas, F.: Model-checking of smart contracts. In: 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData), pp. 980–987 (2018). https://doi.org/10.1109/Cybermatics_2018.2018.00185

  41. Nehaï, Z., Bobot, F.: Deductive proof of industrial smart contracts using why3. In: Sekerinski, E., et al. (eds.) Formal Methods. FM 2019 International Workshops: Porto, Portugal, 7–11 October 2019, Revised Selected Papers, Part I, pp. 299–311. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-54994-7_22

  42. Perez, D., Livshits, B.: Smart contract vulnerabilities: does anyone care? ar**v preprint ar**v:1902.06710, pp. 1–15 (2019)

  43. Perez, D., Livshits, B.: Smart contract vulnerabilities: vulnerable does not imply exploited. In: USENIX Security Symposium, pp. 1325–1341 (2021)

    Google Scholar 

  44. Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: Verx: safety verification of smart contracts. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 1661–1677 (2020). https://doi.org/10.1109/SP40000.2020.00024

  45. Petrović, N., Tošić, M.: Semantic approach to smart contract verification. Facta Univ. Ser. Automat. Control Robot. 19(1), 021–037 (2020)

    Google Scholar 

  46. Ribeiro, M., Adão, P., Mateus, P.: Formal verification of ethereum smart contracts using Isabelle/HOL. In: Nigam, V., et al. (eds.) Logic, Language, and Security: Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday, pp. 71–97. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-62077-6_7

  47. Roşu, G., Ştefănescu, A.: From hoare logic to matching logic reachability. In: Proceedings of the Formal Methods: 18th International Symposium (FM 2012), Paris, 27–31 August 2012, pp. 387–402. Springer, Cham (2012)

    Google Scholar 

  48. Runtime Verification. Smart Contract Analysis and Verification (2023). https://runtimeverification.com/smartcontract

  49. Seres, I.A.: Implementing 2 phase commit (2pc) with solidity (2018). https://ethereum.stackexchange.com/questions/54950/implementing-2-phase-commit-2pc-with-solidity

  50. Lahiri, S.: Verisolcontracts.sol (2019). https://github.com/microsoft/verisol/blob/master/Test/regressions/Libraries/VeriSolContracts.sol

  51. Lahiri, S., ellab123, et al.: verisol. https://github.com/microsoft/verisol

  52. SmartContractSecurity + Contributers. SWC registry smart contract weakness classification and test cases (2020). https://swcregistry.io/

  53. Tolmach, P., Li, Y., Lin, S.-W., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. ACM Comput. Surv. 54(7), 1–38 (2022). https://doi.org/10.1145/3464421

  54. Torres, C.F., Schütte, J., State, R.: Osiris: hunting for integer bugs in ethereum smart contracts. In: Proceedings of the 34th Annual Computer Security Applications Conference, pp. 664–676 (2018)

    Google Scholar 

  55. Wang, Y., et al.: Formal verification of workflow policies for smart contracts in azure blockchain. In: Chakraborty, S., Navas, J.A. (eds.) Verified Software. Theories, Tools, and Experiments: 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13–14, 2019, Revised Selected Papers, pp. 87–106. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-41600-3_7

  56. Yang, Z., Lei, H., Qian, W.: A hybrid formal verification system in coq for ensuring the reliability and security of ethereum-based service smart contracts. IEEE Access 8, 21411–21436 (2020). https://doi.org/10.1109/ACCESS.2020.2969437

    Article  Google Scholar 

  57. Hirai, Y.: Ethereum-Formal-Verification-Overview (2018). https://github.com/pirapira/ethereum-formal-verification-overview

  58. Zou, W., et al.: Smart contract development: challenges and opportunities. IEEE Trans. Softw. Eng. 47(10), 2084–2106 (2021). https://doi.org/10.1109/TSE.2019.2942301

Download references

Author information

Authors and Affiliations

  1. Fraunhofer Institute for Production Systems and Design Technology IPK, Berlin, Germany

    Vincent Happersberger, Frank-Walter Jäkel & Thomas Knothe

  2. DFINITY Foundation, Zurich, Switzerland

    Yvonne-Anne Pignolet

  3. Technical University of Berlin, Berlin, Germany

    Stefan Schmid

Authors
  1. Vincent Happersberger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frank-Walter Jäkel
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Thomas Knothe
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yvonne-Anne Pignolet
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Stefan Schmid
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vincent Happersberger .

Editor information

Editors and Affiliations

  1. Norwegian University of Science and Technology, Gjøvik, Norway

    Sokratis Katsikas

  2. Polytechnique Montréal, Montreal, QC, Canada

    Frédéric Cuppens

  3. Polytechnique Montréal, Montreal, QC, Canada

    Nora Cuppens-Boulahia

  4. University of Piraeus, Piraeus, Greece

    Costas Lambrinoudakis

  5. Télécom SudParis, Palaiseau, France

    Joaquin Garcia-Alfaro

  6. Universitat Autonoma de Barcelona, Bellaterra, Spain

    Guillermo Navarro-Arribas

  7. University of Murcia, Murcia, Spain

    Pantaleone Nespoli

  8. University of the Aegean, Mytilene, Greece

    Christos Kalloniatis

  9. University of Toronto, Toronto, ON, Canada

    John Mylopoulos

  10. Georgia Institute of Technology, Atlanta, GA, USA

    Annie Antón

  11. University of Piraeus, Piraeus, Greece

    Stefanos Gritzalis

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Happersberger, V., Jäkel, FW., Knothe, T., Pignolet, YA., Schmid, S. (2024). Comparison of Ethereum Smart Contract Analysis and Verification Methods. In: Katsikas, S., et al. Computer Security. ESORICS 2023 International Workshops. ESORICS 2023. Lecture Notes in Computer Science, vol 14398. Springer, Cham. https://doi.org/10.1007/978-3-031-54204-6_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-54204-6_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-54203-9

  • Online ISBN: 978-3-031-54204-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation