Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts

Simple item page
dc.contributor.authorBritten, Danielen_NZ
dc.contributor.authorSjöberg, Vilhelmen_NZ
dc.contributor.authorReeves, Steveen_NZ
dc.contributor.editorBernardo, B.en_NZ
dc.contributor.editorMarmsoler, D.en_NZ
dc.date.accessioned2021-12-12T23:41:22Z
dc.date.available2021-12-12T23:41:22Z
dc.date.issued2021en_NZ
dc.description.abstractUsing 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.en_NZ
dc.format.mimetypeapplication/pdf
dc.identifier.doi10.4230/OASIcs.FMBC.2021.3en_NZ
dc.identifier.urihttps://hdl.handle.net/10289/14688
dc.language.isoen
dc.relation.isPartOfProceedings of 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021), OASICS Vol. 95en_NZ
dc.rights© Daniel Britten, Vilhelm Sjöberg, and Steve Reeves; licensed under Creative Commons License CC-BY 4.0 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
dc.sourceFMBC 2021en_NZ
dc.subjectsoftware engineeringen_NZ
dc.subjectsmart contractsen_NZ
dc.subjectformal methodsen_NZ
dc.subjectblockchainen_NZ
dc.titleUsing Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contractsen_NZ
dc.typeConference Contribution
pubs.elements-id266698
pubs.finish-date2021-07-19en_NZ
pubs.organisational-group/Waikato
pubs.organisational-group/Waikato/2025 PBRF
pubs.organisational-group/Waikato/DHECS
pubs.organisational-group/Waikato/DHECS/2025 PBRF - DHEC
pubs.organisational-group/Waikato/DHECS/SCMS
pubs.organisational-group/Waikato/DHECS/SCMS/2025 PBRF - SCMS
pubs.owner.emailstever@waikato.ac.nz
pubs.owner.nameReeves, Stephen
pubs.start-date2021-07-18en_NZ
pubs.user.infoReeves, Stephen (stever@waikato.ac.nz)
uow.verification.statusunverified
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
OASIcs-FMBC-2021-3.pdf
Size:
663.06 KB
Format:
Adobe Portable Document Format
Description:
Published version
Thumbnail Image
Name: OASIcs-FMBC-2021-3.pdf
Size: 663.06 KB
Kind: Adobe PDF
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
Research Commons Deposit Agreement 2017.pdf
Size:
188.11 KB
Format:
Adobe Portable Document Format
Description:
Name: Research Commons Deposit Agreement 2017.pdf
Size: 188.11 KB
Kind: Adobe PDF
Collections
Computing and Mathematical Sciences Papers