Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/3437378.3437879acmotherconferencesArticle/Chapter ViewAbstractPublication PagesacswConference Proceedingsconference-collections
research-article

A Survey on Formal Verification for Solidity Smart Contracts

Published: 01 February 2021 Publication History

Abstract

One of the 21st century’s hottest topics in the world of IT has been the emergence of what some predict to be the foundation stone for a new era of internet (web 3.0): Blockchain technology. Besides being the backbone of what we come to know as cryptocurrencies, Blockchain’s features make for a bottomless list of possible applications, especially thanks to the concept of smart contracts. This, however, caused Blockchain to be in the limelight of not only interested investors but also malicious users who started hunting for this technology’s vulnerabilities, which resulted in numerous attacks on different Blockchain platforms. In an attempt to mend such loopholes, researchers took an interest in the verification of smart contracts, which are at the heart of Blockchain’s applications. In this survey, we aim to present a general overview of the different axes investigated by researchers towards the verification of smart contracts, while taking a special interest in studies that focus on formal verification, the different approaches they apply and vulnerabilities they target.

References

[1]
[n.d.]. Formal Verification for Solidity Contracts — Ethereum Community Forum. https://forum.ethereum.org/discussion/3779/formal-verification-for-solidity-contracts.
[2]
[n.d.]. Ropsten. https://ropsten.etherscan.io/.
[3]
Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples. 2018. Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. New York, NY, USA, 66–77.
[4]
Saswat Anand, Corina S. Pasareanu, and Willem Visser. [n.d.]. Symbolic execution with abstraction. Int. J. Softw. Tools Technol. Transf. 11, 1 ([n. d.]).
[5]
Monika Di Angelo and Gernot Salzer. 2019. A Survey of Tools for Analyzing Ethereum Smart Contracts. 2019 IEEE International Conference on Decentralized Applications and Infrastructures (DAPPCON)(2019), 69–78.
[6]
Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. [n.d.]. A Survey of Attacks on Ethereum Smart Contracts (SoK). In Principles of Security and Trust - 6th International Conference, POST 2017, Uppsala, Sweden, April 22-29, Proceedings.
[7]
Ananda Basu, Saddek Bensalem, Marius Bozga, Jacques Combaz, Mohamad Jaber, Thanh-Hung Nguyen, and Joseph Sifakis. 2011. Rigorous Component-Based System Design Using the BIP Framework. IEEE Software 28, 3 (2011), 41–48.
[8]
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, and Santiago Zanella Béguelin. 2016. Formal Verification of Smart Contracts: Short Paper. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS@CCS 2016, Vienna, Austria, October 24, 2016. 91–96.
[9]
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic Model Checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS ’99, Held as Part of ETAPS’99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings. 193–207.
[10]
Lexi Brent, Anton Jurisevic, Michael Kong, Eric Liu, François Gauthier, Vincent Gramoli, Ralph Holz, and Bernhard Scholz. 2018. Vandal: A Scalable Security Analysis Framework for Smart Contracts. CoRR abs/1809.03981(2018).
[11]
Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. [n.d.]. The nuXmv Symbolic Model Checker. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of VSL 2014, Austria.
[12]
Ting Chen, Xiaoqi Li, Xiapu Luo, and Xiaosong Zhang. 2017. Under-optimized smart contracts devour your money. In IEEE 24th International Conference on Software Analysis, Evolution and Reengineering, SANER 2017, Klagenfurt, Austria, February 20-24, 2017. 442–446.
[13]
Leonardo Mendonça de Moura and Nikolaj Bjørner. [n.d.]. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Budapest, Hungary, March 29-April 6, 2008.
[14]
Wesley Dingman, Aviel Cohen, Nick Ferrara, Adam Lynch, Patrick Jasinski, Paul E. Black, and Lin Deng. 2019. Defects and Vulnerabilities in Smart Contracts, a Classification using the NIST Bugs Framework. IJNDC 7, 3 (2019), 121–132.
[15]
Nick Dodson. 2016. Solint: A linting utility for Ethereum solidity smart-contracts. https://github.com/SilentCicero/solint.
[16]
Vimal Dwivedi, Vipin Deval, Abhishek Dixit, and Alex Norta. 2019. Formal-Verification of Smart-Contract Languages: A Survey. In Advances in Computing and Data Sciences. Singapore, 738–747.
[17]
Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. 343–361.
[18]
Yoichi Hirai. 2017. Ethereum VM for Coq (v0.0.2). https://medium.com/@pirapira/ethereum-virtual-machine-for-coq-v0-0-2-d2568e068b18.
[19]
Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018. ZEUS: Analyzing Safety of Smart Contracts. In 25th Annual Network and Distributed System Security Symposium, NDSS 2018, San Diego, California, USA, February 18-21, 2018.
[20]
Sarfraz Khurshid, Corina S. Pasareanu, and Willem Visser. 2003. Generalized Symbolic Execution for Model Checking and Testing. In Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings. 553–568.
[21]
Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making Smart Contracts Smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Austria, October 24-28.
[22]
Anastasia Mavridou and Aron Laszka. [n.d.]. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. In Financial Cryptography and Data Security - 22nd International Conference, FC 2018, Nieuwpoort, Curaçao, February 26 - March 2, 2018.
[23]
Anastasia Mavridou, Aron Laszka, Emmanouela Stachtiari, and Abhishek Dubey. [n.d.]. VeriSolid: Correct-by-Design Smart Contracts for Ethereum. In Financial Cryptography and Data Security - 23rd International Conference, FC 2019, Frigate Bay, St. Kitts and Nevis, February 18-22, 2019.
[24]
Kenneth L. McMillan. 1993. Symbolic model checking. Kluwer.
[25]
David Molnar, Xue Cong Li, and David A. Wagner. 2009. Dynamic Test Generation to Find Integer Bugs in x86 Binary Linux Programs. In 18th USENIX Security Symposium, Montreal, Canada, August 10-14, 2009, Proceedings. 67–82.
[26]
Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. 2018. Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. In Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC 2018, San Juan, PR, USA, December 03-07, 2018. 653–663.
[27]
Zvonimir Rakamaric and Michael Emmi. [n.d.]. SMACK: Decoupling Source Language Details from Verifier Implementations. In Computer Aided Verification - 26th International Conference, CAV 2014, Vienna, Austria, July 18-22, 2014.
[28]
Alex Rea. 2016-2020. SolCover: Code coverage for Solidity smart-contracts. https://github.com/sc-forks/solidity-coverage.
[29]
Cesare Tinelli. 2012. SMT-Based Model Checking. In NASA Formal Methods - 4th International Symposium, NFM 2012, USA, April 3-5, 2012. Proceedings.
[30]
Christof Ferreira Torres, Julian Schütte, and Radu State. 2018. Osiris: Hunting for Integer Bugs in Ethereum Smart Contracts. In Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC 2018, USA, December 03-07.
[31]
Petar Tsankov, Andrei Marian Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin T. Vechev. 2018. Securify: Practical Security Analysis of Smart Contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, Canada, October 15-19.
[32]
Ence Zhou, Song Hua, Bingfeng Pi, Jun Sun, Yashihide Nomura, Kazuhiro Yamashita, and Hidetoshi Kurihara. 2018. Security Assurance for Smart Contract. In 9th IFIP International Conference on New Technologies, Mobility and Security, NTMS 2018, Paris, France, February 26-28, 2018. 1–5.

Cited By

View all
  • (2024)Automated Repair of Smart Contract Vulnerabilities: A Systematic Literature ReviewElectronics10.3390/electronics1319394213:19(3942)Online publication date: 6-Oct-2024
  • (2024)SCVHunter: Smart Contract Vulnerability Detection Based on Heterogeneous Graph Attention NetworkProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639213(1-13)Online publication date: 20-May-2024
  • (2024)Classification Method of Ethereum Smart Contracts Based on Statistical Model Checking2024 IEEE 24th International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS62785.2024.00078(733-744)Online publication date: 1-Jul-2024
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences
ACSW '21: Proceedings of the 2021 Australasian Computer Science Week Multiconference
February 2021
211 pages
ISBN:9781450389563
DOI:10.1145/3437378
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: 01 February 2021

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Blockchain
  2. Ethereum
  3. Formal Verification
  4. Smart Contract
  5. Solidity

Qualifiers

  • Research-article
  • Research
  • Refereed limited

Conference

ACSW '21

Acceptance Rates

Overall Acceptance Rate 61 of 141 submissions, 43%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)185
  • Downloads (Last 6 weeks)16
Reflects downloads up to 14 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Automated Repair of Smart Contract Vulnerabilities: A Systematic Literature ReviewElectronics10.3390/electronics1319394213:19(3942)Online publication date: 6-Oct-2024
  • (2024)SCVHunter: Smart Contract Vulnerability Detection Based on Heterogeneous Graph Attention NetworkProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639213(1-13)Online publication date: 20-May-2024
  • (2024)Classification Method of Ethereum Smart Contracts Based on Statistical Model Checking2024 IEEE 24th International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS62785.2024.00078(733-744)Online publication date: 1-Jul-2024
  • (2024)A Coverage-Oriented Fuzzing Test Method for Embedded Firmware2024 10th International Symposium on System Security, Safety, and Reliability (ISSSR)10.1109/ISSSR61934.2024.00036(244-250)Online publication date: 16-Mar-2024
  • (2024)(In)Correct Smart Contract Specifications2024 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)10.1109/ICBC59979.2024.10634444(567-575)Online publication date: 27-May-2024
  • (2024)Bi-thresholds-based unknown vulnerability detection in smart contracts using multi-classification modelComputers and Electrical Engineering10.1016/j.compeleceng.2024.109682120(109682)Online publication date: Dec-2024
  • (2024)A smart contract vulnerability detection method based on deep learning with opcode sequencesPeer-to-Peer Networking and Applications10.1007/s12083-024-01750-717:5(3222-3238)Online publication date: 27-Jun-2024
  • (2024)FVF-BIoT: a formal verification framework for blockchain-based IoT authenticationSoftware Quality Journal10.1007/s11219-024-09691-332:4(1457-1480)Online publication date: 20-Jul-2024
  • (2024)A systematic mapping on software testing for blockchainsCluster Computing10.1007/s10586-024-04421-727:6(7111-7126)Online publication date: 1-Sep-2024
  • (2024)Vulnerabilities in Smart Contracts of Decentralized BlockchainCyber Security and Digital Forensics10.1007/978-981-99-9811-1_44(551-566)Online publication date: 11-Mar-2024
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

HTML Format

View this article in HTML Format.

HTML Format

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media