Predicate abstractions for smart contract validation
Authors: 
Javier Godoy, 
Juan Pablo Galeotti, 
Diego Garbervetsky, 
Sebastian UchitelAuthors Info & Claims
Javier Godoy, Juan Pablo Galeotti, Diego Garbervetsky, Sebastian UchitelAuthors Info & ClaimsPages 289 - 299
Abstract
Smart contracts are immutable programs deployed on the blockchain that can manage significant assets. Because of this, verification and validation of smart contracts is of vital importance. Indeed, it is industrial practice to hire independent specialized companies to audit smart contracts before deployment. Auditors typically rely on a combination of tools and experience but still fail to identify problems in smart contracts before deployment, causing significant losses. In this paper, we propose using predicate abstraction to construct models which can be used by auditors to explore and validate smart contact behaviour at the function call level by proposing predicates that expose different aspects of the contract. We propose predicates based on requires clauses and enum-type state variables as a starting point for contract validation and report on an evaluation on two different benchmarks.
References
[1]
2016. Analysis of the dao exploit. http://hackingdistributed.com/2016/06/18/analysis-of-thedao-exploit/
[2]
2016. The dao smart contract. http://etherscan.io/address/0xbb9bc244d798123fde783fcc1c72d3bb8c189413
[3]
2017. Azure Blockchain Workbench. https://github.com/Azure-Samples/blockchain/tree/master/blockchain-workbench/application-and-smart-contract-samples
[4]
2017. OMG Unified Modeling Language, Version 2.5.1. https://www.omg.org/spec/UML/2.5.1/PDF.
[5]
2018. Smart Contract Best Practices Revisited: Block Number vs. Times-tamp. https://medium.com/@phillipgoldberg/smart-contract-best-practices-revisited-block-number-vs-timestamp-648905104323
[6]
2018. Surya's repository. https://github.com/ConsenSys/surya.
[7]
2019. Digital Locker Documentation. https://github.com/Azure-Samples/blockchain/tree/master/blockchain-workbench/application-and-smart-contract-samples/digital-locker
[8]
2020. Azure fixed code. https://github.com/blockhousetech/research/tree/master/Solidifier/evaluation/examples/azure_fixed.
[9]
2020. Openzeppelin: Build secure smart contracts in solidity. https://openzeppelin.com/contracts/
[10]
2020. Smart Contract Weakness Classification and Test Cases. https://swcregistry.io/
[11]
2020. Types in Solidity. https://docs.soliditylang.org/en/v0.8.7/types.html
[12]
2021. Require in Solidity. https://docs.soliditylang.org/en/v0.8.7/control-structures.html.
[13]
2022. Rust for Near. https://docs.rs/near-sdk/latest/near_sdk/macro.require.html.
[14]
Flora Amato, Giovanni Cozzolino, Francesco Moscato, Vincenzo Moscato, and Fatos Xhafa. 2021. A Model for verification and validation of law compliance of smart contracts in IoT environment. IEEE Transactions on Industrial Informatics 17, 11 (2021), 7752--7759.
[15]
Pedro Antonino and A. W. Roscoe. 2021. Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling. In SAC '21: The 36th ACM/SIGAPP Symposium on Applied Computing, Virtual Event, Republic of Korea, March 22--26, 2021, Chih-Cheng Hung, Jiman Hong, Alessio Bechini, and Eunjee Song (Eds.). ACM, 1788--1797.
[16]
Guido de Caso, Victor Braberman, Diego Garbervetsky, and Sebastian Uchitel. 2009. Validation of contracts using enabledness preserving finite state abstractions. In 2009 IEEE 31st International Conference on Software Engineering. 452--462.
[17]
Guido de Caso, Víctor Braberman, Diego Garbervetsky, and Sebastián Uchitel. 2011. Program Abstractions for Behaviour Validation. In Proceedings of the 33rd International Conference on Software Engineering (Waikiki, Honolulu, HI, USA) (ICSE '11). Association for Computing Machinery, New York, NY, USA, 381--390.
[18]
Guido de Caso, Victor Braberman, Diego Garbervetsky, and Sebastian Uchitel. 2012. Automated abstractions for contract validation. IEEE Transactions on Software Engineering 38, 1 (2012), 141--162.
[19]
G. de Caso, V. Braberman, D. Garbervetsky, and S. Uchitel. 2013. Enabledness-based program abstractions for behavior validation. ACM Trans. Softw. Eng. Methodol. 22, 3 (2013).
[20]
Robert DeLine and Manuel Fähndrich. 2001. Enforcing high-level protocols in low-level software. In Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation. 59--69.
[21]
Wang Duo, Huang Xin, and Ma Xiaofeng. 2020. Formal analysis of smart contract based on colored petri nets. IEEE Intelligent Systems 35, 3 (2020), 19--30.
[22]
Joshua Ellul and Gordon J Pace. 2018. Runtime verification of ethereum smart contracts. In 2018 14th European Dependable Computing Conference (EDCC). IEEE, 158--163.
[23]
Josselin Feist, Gustavo Grieco, and Alex Groce. 2019. Slither: A Static Analysis Framework for Smart Contracts. 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB) (May 2019).
[24]
Ikram Garfatta, Kaïs Klai, Mohamed Graïet, and Walid Gaaloul. 2022. Model checking of vulnerabilities in smart contracts: a solidity-to-CPN approach. In Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing. 316--325.
[25]
Carlo Ghezzi, Andrea Mocci, and Mattia Monga. 2009. Synthesizing intensional behavior models by graph transformation. In 2009 IEEE 31st International Conference on Software Engineering. IEEE, 430--440.
[26]
Javier Godoy, Juan Pablo Galeotti, Diego Garbervetsky, and Sebastián Uchitel. 2021. Enabledness-based Testing of Object Protocols. ACM Trans. Softw. Eng. Methodol. 30, 2 (2021), 12:1--12:36.
[27]
Gustavo Grieco, Will Song, Artur Cygan, Josselin Feist, and Alex Groce. 2020. Echidna: Effective, Usable, and Fast Fuzzing for Smart Contracts. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis (Virtual Event, USA) (ISSTA 2020). Association for Computing Machinery, New York, NY, USA, 557--560.
[28]
Alex Groce, Josselin Feist, Gustavo Grieco, and Michael Colburn. 2020. What are the Actual Flaws in Important Smart Contracts (and How Can We Find Them)?. In Financial Cryptography.
[29]
Thomas A Henzinger, Ranjit Jhala, and Rupak Majumdar. 2005. Permissive interfaces. In Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering. 31--40.
[30]
Thomas A Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. 2003. Software verification with BLAST. In International SPIN Workshop on Model Checking of Software. Springer, 235--239.
[31]
Daniel Jackson. 2019. Alloy: A Language and Tool for Exploring Software Designs. Commun. ACM 62, 9 (aug 2019), 66--76.
[32]
Ranjit Jhala, Andreas Podelski, and Andrey Rybalchenko. 2018. Predicate Abstraction for Program Verification. Springer International Publishing, Cham, 447--491.
[33]
Mahtab Kouhizadeh and Joseph Sarkis. 2018. Blockchain practices, potentials, and perspectives in greening supply chains. Sustainability 10, 10 (2018), 3652.
[34]
Anastasia Mavridou, Aron Laszka, Emmanouela Stachtiari, and Abhishek Dubey. 2019. VeriSolid: Correct-by-design smart contracts for Ethereum. arXiv preprint arXiv:1901.01292 (2019).
[35]
Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, and Artem Dinaburg. 2019. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 1186--1189.
[36]
Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, and Martin Vechev. 2020. VerX: Safety Verification of Smart Contracts. In 2020 IEEE Symposium on Security and Privacy (SP). 1661--1677.
[37]
Ilya Sergey, Amrit Kumar, and Aquinas Hobor. 2018. Temporal Properties of Smart Contracts. In Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5--9, 2018, Proceedings, Part IV (Limassol, Cyprus). Springer-Verlag, Berlin, Heidelberg, 323--338.
[38]
Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu K. Lahiri, and Isil Dillig. 2021. SmartPulse: Automated Checking of Temporal Properties in Smart Contracts. In 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24--27 May 2021. IEEE, 555--571.
[39]
Yuepeng Wang, Shuvendu K. Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer, and Kostas Ferles. 2019. Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain. In Verified Software. Theories, Tools, and Experiments - 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13--14, 2019, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 12031), Supratik Chakraborty and Jorge A. Navas (Eds.). Springer, 87--106.
[40]
Gavin Wood et al. 2014. Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper 151, 2014 (2014), 1--32.
Index Terms
- Predicate abstractions for smart contract validation
Recommendations
Smart Contract Locator (SCL) and Smart Contract Description Language (SCDL)
Service-Oriented Computing – ICSOC 2019 WorkshopsAbstractToday’s blockchain technologies focus mostly on isolated, proprietary technologies, yet there are application scenarios that ask for interoperability, e.g., among blockchains themselves or with external applications. This paper proposes the Smart ...
Smart Payment Contract Mechanism Based on Blockchain Smart Contract Mechanism
In recent years, blockchain technology has become a hot topic in various industries. With the development and maturity of blockchain technology, it has been applied to finance, law, etc., with its advantages of decentralization, openness, information ...
Smart Contract and Blockchain Based Contract Management System
ECBS 2021: 7th Conference on the Engineering of Computer Based SystemsThis paper presents theoretical and practical research on the possibilities of applying smart contracts in the field of law and a contract management system which allows users to conclude contracts based on blockchain technology. The transition from ...
Comments
Information & Contributors
Information
Published In
October 2022
412 pages
Copyright © 2022 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 the author(s) 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].
Sponsors
In-Cooperation
- Univ. of Montreal: University of Montreal
- IEEE CS
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 24 October 2022
Check for updates
Qualifiers
- Research-article
Funding Sources
- ANPCYT
- CONICET
- UBACYT
Conference
MODELS '22
Sponsor:
MODELS '22: ACM/IEEE 25th International Conference on Model Driven Engineering Languages and Systems
October 23 - 28, 2022
Quebec, Montreal, Canada
Acceptance Rates
MODELS '22 Paper Acceptance Rate 35 of 125 submissions, 28%;
Overall Acceptance Rate 144 of 506 submissions, 28%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 180Total Downloads
- Downloads (Last 12 months)57
- Downloads (Last 6 weeks)3
Reflects downloads up to 24 Oct 2024
Other Metrics
Citations
Cited By
View allView Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in