Verifying Declarative Smart Contracts
Article No.: 179, Pages 1 - 12
Abstract
Smart contracts manage a large number of digital assets nowadays. Bugs in these contracts have led to significant financial loss. Verifying the correctness of smart contracts is, therefore, an important task. This paper presents an automated safety verification tool, DCV, that targets declarative smart contracts written in De-Con, a logic-based domain-specific language for smart contract implementation and specification. DCV proves safety properties by mathematical induction and can automatically infer inductive invariants using heuristic patterns, without annotations from the developer. Our evaluation on 23 benchmark contracts shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools. Furthermore, DCV significantly outperforms baseline tools in verification time.
References
[1]
King of the ether throne --- post-mortem investigation. https://www.kingoftheether.com/postmortem.html, 2016.
[2]
Understanding the dao attack. https://www.coindesk.com/learn/2016/06/25/understanding-the-dao-attack/, 2016.
[3]
Not a fair game - fairness analysis of dice2win. https://blogs.360.net/post/Fairness_Analysis_of_Dice2win_EN.html, 2018.
[4]
Cannot replicate smtchecker example output. https://github.com/ethereum/solidity/issues/13073, 2022.
[5]
Openzeppelin. https://github.com/OpenZeppelin/openzeppelin-contracts, 2022.
[6]
Smtchecker and formal verification. https://docs.soliditylang.org/en/v0.8.17/smtchecker.html, 2022.
[7]
Solidity by example. https://docs.soliditylang.org/en/v0.8.17/solidity-by-example.html, 2022.
[8]
The solidity contract-oriented programming language. https://github.com/ethereum/solidity, 2022.
[9]
Verx smart contract verification benchmarks. https://github.com/eth-sri/verx-benchmarks, 2022.
[10]
Z3. https://github.com/Z3Prover/z3, 2022.
[11]
Act. https://github.com/ethereum/act, 2023.
[12]
Erc-20 top tokens. https://etherscan.io/tokens, 2023.
[13]
Non-fungible tokens (nft). https://etherscan.io/tokens-nft, 2023.
[14]
Scribble. https://github.com/ConsenSys/Scribble, 2023.
[15]
Verismart commit on may 31, 2020. https://github.com/kupl/VeriSmart-public/commit/858af814fbdab0c9d85b758e4c4575402ebf2bdf, 2023.
[16]
Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples. Towards verifying ethereum smart contract bytecode in isabelle/hol. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 66--77, 2018.
[17]
Franck Cassez, Joanne Fuller, and Horacio Mijail Antón Quiles. Deductive verification of smart contracts with dafny. In International Conference on Formal Methods for Industrial Critical Systems, pages 50--66. Springer, 2022.
[18]
Haoxian Chen, Gerald Whitters, Mohammad Javad Amiri, Yuepeng Wang, and Boon Thau Loo. Declarative smart contracts. In ESEC/FSE '22, 2022.
[19]
Ting Chen, Rong Cao, Ting Li, Xiapu Luo, Guofei Gu, Yufei Zhang, Zhou Liao, Hang Zhu, Gang Chen, Zheyuan He, et al. Soda: A generic online detection framework for smart contracts. In NDSS, 2020.
[20]
Xiaohong Chen, Daejun Park, and Grigore Roşu. A language-independent approach to smart contract verification. In International Symposium on Leveraging Applications of Formal Methods, pages 405--413. Springer, 2018.
[21]
Jaeseung Choi, Doyeon Kim, Soomin Kim, Gustavo Grieco, Alex Groce, and Sang Kil Cha. Smartian: Enhancing smart contract fuzzing with static and dynamic data-flow analyses. In 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 227--239. IEEE, 2021.
[22]
Yue Duan, Xin Zhao, Yu Pan, Shucheng Li, Minghao Li, Fengyuan Xu, and Mu Zhang. Towards automated safety vetting of smart contracts in decentralized applications. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, pages 921--935, 2022.
[23]
Joel Frank, Cornelius Aschermann, and Thorsten Holz. ETHBMC: A bounded model checker for smart contracts. In 29th USENIX Security Symposium (USENIX Security 20), pages 2757--2774. USENIX Association, August 2020.
[24]
Gustavo Grieco, Will Song, Artur Cygan, Josselin Feist, and Alex Groce. Echidna: effective, usable, and fast fuzzing for smart contracts. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 557--560, 2020.
[25]
Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. A semantic framework for the security analysis of ethereum smart contracts. In International Conference on Principles of Security and Trust, pages 243--269. Springer, 2018.
[26]
Ákos Hajdu and Dejan Jovanović. solc-verify: A modular verifier for solidity smart contracts. In Working conference on verified software: theories, tools, and experiments, pages 161--179. Springer, 2019.
[27]
Bo Jiang, Ye Liu, and Wing Kwong Chan. Contractfuzzer: Fuzzing smart contracts for vulnerability detection. In 2018 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 259--269. IEEE, 2018.
[28]
Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. Zeus: analyzing safety of smart contracts. In Ndss, pages 1--12, 2018.
[29]
Shuvendu K Lahiri and Shaz Qadeer. Complexity and algorithms for monomial and clausal predicate abstraction. In International Conference on Automated Deduction, pages 214--229. Springer, 2009.
[30]
Ao Li, Jemin Andrew Choi, and Fan Long. Securing smart contract with runtime validation. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 438--453, 2020.
[31]
Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. Making smart contracts smarter. In Proceedings of the 2016 ACM SIGSAC conference on computer and communications security, pages 254--269, 2016.
[32]
Matteo Marescotti, Rodrigo Otoni, Leonardo Alt, Patrick Eugster, Antti EJ Hyvärinen, and Natasha Sharygina. Accurate smart contract verification through direct modelling. In International Symposium on Leveraging Applications of Formal Methods, pages 178--194. Springer, 2020.
[33]
Zeinab Nehai, Pierre-Yves Piriou, and Frederic Daumas. 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), pages 980--987. IEEE, 2018.
[34]
Ivica Nikolić, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. Finding the greedy, prodigal, and suicidal contracts at scale. In Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC '18, page 653--663, New York, NY, USA, 2018. Association for Computing Machinery.
[35]
Benedikt Notheisen, Magnus Gödde, and Christof Weinhardt. Trading stocks on blocks-engineering decentralized markets. In International Conference on Design Science Research in Information System and Technology, pages 474--478. Springer, 2017.
[36]
Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, and Martin Vechev. Verx: Safety verification of smart contracts. In 2020 IEEE symposium on security and privacy (SP), pages 1661--1677. IEEE, 2020.
[37]
Michael Rodler, Wenting Li, Ghassan O Karame, and Lucas Davi. Sereum: Protecting existing smart contracts against re-entrancy attacks. arXiv preprint arXiv:1812.05934, 2018.
[38]
Clara Schneidewind, Ilya Grishchenko, Markus Scherer, and Matteo Maffei. ethor: Practical and provably sound static analysis of ethereum smart contracts. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, pages 621--640, 2020.
[39]
Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan Guan Hao. Safer smart contract programming with scilla. Proceedings of the ACM on Programming Languages, 3(OOPSLA):1--30, 2019.
[40]
Sunbeom So, Seongjoon Hong, and Hakjoo Oh. {SmarTest}: Effectively hunting vulnerable transaction sequences in smart contracts through language {Model-Guided} symbolic execution. In 30th USENIX Security Symposium (USENIX Security 21), pages 1361--1378, 2021.
[41]
Sunbeom So, Myungho Lee, Jisu Park, Heejo Lee, and Hakjoo Oh. Verismart: A highly precise safety verifier for ethereum smart contracts. In 2020 IEEE Symposium on Security and Privacy (SP), pages 1678--1694. IEEE, 2020.
[42]
Kunjian Song, Nedas Matulevicius, Eddie B de Lima Filho, and Lucas C Cordeiro. Esbmc-solidity: an smt-based model checker for solidity smart contracts. In Proceedings of the ACM/IEEE 44th International Conference on Software Engineering: Companion Proceedings, pages 65--69, 2022.
[43]
Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu Lahiri, and Isil Dillig. Smartpulse: automated checking of temporal properties in smart contracts. In 2021 IEEE Symposium on Security and Privacy (SP), pages 555--571. IEEE, 2021.
[44]
Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Buenzli, and Martin Vechev. Securify: Practical security analysis of smart contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pages 67--82, 2018.
[45]
Shuai Wang, Yong Yuan, Xiao Wang, Juanjuan Li, Rui Qin, and Fei-Yue Wang. An overview of smart contract: architecture, applications, and future trends. In 2018 IEEE Intelligent Vehicles Symposium (IV), pages 108--113. IEEE, 2018.
[46]
Yuepeng Wang, Shuvendu K Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer, and Kostas Ferles. Formal verification of workflow policies for smart contracts in azure blockchain. In Working Conference on Verified Software: Theories, Tools, and Experiments, pages 87--106. Springer, 2019.
[47]
Scott Wesley, Maria Christakis, Jorge A Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel. Verifying solidity smart contracts via communication abstraction in smartace. In International Conference on Verification, Model Checking, and Abstract Interpretation, pages 425--449. Springer, 2022.
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 ...
An overview on smart contracts: Challenges, advances and platforms
AbstractSmart contract technology is reshaping conventional industry and business processes. Being embedded in blockchains, smart contracts enable the contractual terms of an agreement to be enforced automatically without the intervention of a trusted ...
Highlights- Opportunities of smart contracts for industrial internet of things.
- Lifecycle and platforms of smart contracts.
- Applications of smart contracts.
- Challenges and advances of smart contracts.
Towards Verifying Ethereum Smart Contracts at Intermediate Language Level
Formal Methods and Software EngineeringAbstractSmart contracts have exhibited great potential in a spectrum of applications, ranging from digital currency to online gaming. Yet smart contracts are known to be prone to errors and vulnerable to attacks. The validation of smart contracts before ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
May 2024
2942 pages
ISBN:9798400702174
DOI:10.1145/3597503
- Co-chairs:
- Ana Paiva,
- Rui Abreu,
- Program Co-chairs:
- Abhik Roychoudhury,
- Margaret Storey
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
In-Cooperation
- Faculty of Engineering of University of Porto
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 12 April 2024
Check for updates
Badges
Qualifiers
- Research-article
Funding Sources
Conference
ICSE '24
Sponsor:
ICSE '24: IEEE/ACM 46th International Conference on Software Engineering
April 14 - 20, 2024
Lisbon, Portugal
Acceptance Rates
Overall Acceptance Rate 276 of 1,856 submissions, 15%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 236Total Downloads
- Downloads (Last 12 months)236
- Downloads (Last 6 weeks)63
Reflects downloads up to 18 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in