Show simple item record  

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.identifier.urihttps://hdl.handle.net/10289/14688
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.language.isoen
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
dc.identifier.doi10.4230/OASIcs.FMBC.2021.3en_NZ
dc.relation.isPartOfProceedings of 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021), OASICS Vol. 95en_NZ
pubs.elements-id266698
pubs.finish-date2021-07-19en_NZ
pubs.start-date2021-07-18en_NZ


Files in this item

This item appears in the following Collection(s)

Show simple item record