OASIcs.FMBC.2021.3.pdf
- Filesize: 0.64 MB
- 8 pages
Document
Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts (Short Paper)
Authors
Daniel Britten 
,
Steve Reeves
-
Part of:
Volume:
3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
Series: Open Access Series in Informatics (OASIcs)
Conference: Workshop on Formal Methods for Blockchains (FMBC) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-11-30
File
Document Identifiers
Author Details
Acknowledgements
I (Daniel Britten) want to thank the University of Auckland and Associate Professor Jing Sun for kindly hosting me during this research.
Cite AsGet BibTex
Daniel Britten, Vilhelm Sjöberg, and Steve Reeves. Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 3:1-3:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/OASIcs.FMBC.2021.3
https://doi.org/10.4230/OASIcs.FMBC.2021.3
Abstract
Using the DeepSEA system for smart contract proofs, this paper investigates how to use the Coq theorem prover to enforce that smart contracts follow the Checks-Effects-Interactions Pattern. This pattern is widely understood to mitigate the risks associated with reentrancy. The infamous "The DAO" exploit is an example of the risks of not following the Checks-Effects-Interactions Pattern. It resulted in the loss of over 50 million USD and involved reentrancy - the exploit used would not have been possible if the Checks-Effects-Interactions Pattern had been followed.
Remix IDE, for example, already has a tool to check that the Checks-Effects-Interactions Pattern has been followed as part of the Solidity Static Analysis module which is available as a plugin. However, aside from simply replicating the Remix IDE feature, implementing a Checks-Effects-Interactions Pattern checker in the proof assistant Coq also allows us to use the proofs, which are generated in the process, in other proofs related to the smart contract.
As an example of this, we will demonstrate an idea for how the modelling of Ether transfer can be simplified by using automatically generated proofs of the property that each smart contract function will call the Ether transfer method at most once (excluding any calls related to invoking other smart contracts). This property is a consequence of following a strict version of the Checks-Effects-Interactions Pattern as given in this paper.
Subject Classification
ACM Subject Classification
- Security and privacy → Logic and verification
- Computer systems organization → Distributed architectures
Keywords
- smart contracts
- formal methods
- blockchain
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Lucas Campbell. DeFi platform dForce hacked for $25m - ERC777 reentrancy attack. https://defirate.com/dforce-hack/. (Accessed on 23 May 2021).
- CertiK Foundation. DeepSEA. https://github.com/certikfoundation/deepsea. (Accessed on 23 May 2021).
- The Coq Development Team. The Coq proof assistant. https://coq.inria.fr/. (Accessed on 23 May 2021).
-
Josselin Feist, Gustavo Grieco, and Alex Groce. Slither: a static analysis framework for smart contracts. In 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), pages 8-15. IEEE, 2019.
- Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. CompCert - a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, 2016. URL: https://hal.inria.fr/hal-01238879.
-
Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. Making smart contracts smarter. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016.
- Alex Manuskin. Living in a lego house: The imBTC DeFi hack explained. https://www.zengo.com/imbtc-defi-hack-explained/. (Accessed on 23 May 2021).
-
Muhammad Izhar Mehar, Charles Louis Shier, Alana Giambattista, Elgar Gong, Gabrielle Fletcher, Ryan Sanayhie, Henry M. Kim, and Marek Laskowski. Understanding a Revolutionary and Flawed Grand Experiment in Blockchain: The DAO Attack. Journal of Cases on Information Technology, 21(1):19-32, 2019.
- David Oz Kashi. The reentrancy strikes again - The case of Lendf.Me. https://valid.network/post/the-reentrancy-strikes-again-the-case-of-lendf-me. (Accessed on 23 May 2021).
- Remix. Remix - Ethereum IDE. https://remix.ethereum.org/. (Accessed on 23 May 2021).
-
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.
-
Maximilian Wohrer and Uwe Zdun. Smart contracts: security patterns in the Ethereum ecosystem and solidity. In 2018 International Workshop on Blockchain Oriented Software Engineering (IWBOSE), pages 2-8. IEEE, 2018.