Document Open Access Logo

Formal Specification and Verification of Solidity Contracts with Events (Short Paper)

Authors Ákos Hajdu , Dejan Jovanović , Gabriela Ciocarlie

PDF
Thumbnail PDF

File

OASIcs.FMBC.2020.2.pdf
  • Filesize: 454 kB
  • 9 pages

Document Identifiers

Author Details

Ákos Hajdu
  • Budapest University of Technology and Economics, Hungary
Dejan Jovanović
  • SRI International, New York City, NY, USA
Gabriela Ciocarlie
  • SRI International, New York City, NY, USA

Cite As Get BibTex

Ákos Hajdu, Dejan Jovanović, and Gabriela Ciocarlie. Formal Specification and Verification of Solidity Contracts with Events (Short Paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 2:1-2:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/OASIcs.FMBC.2020.2

Abstract

Events in the Solidity language provide a means of communication between the on-chain services of decentralized applications and the users of those services. Events are commonly used as an abstraction of contract execution that is relevant from the users' perspective. Users must, therefore, be able to understand the meaning and trust the validity of the emitted events. This paper presents a source-level approach for the formal specification and verification of Solidity contracts with the primary focus on events. Our approach allows the specification of events in terms of the on-chain data that they track, and the predicates that define the correspondence between the blockchain state and the abstract view provided by the events. The approach is implemented in solc-verify, a modular verifier for Solidity, and we demonstrate its applicability with various examples.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
Keywords
  • Smart contracts
  • Solidity
  • events
  • specification
  • verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. A guide to events and logs in Ethereum smart contracts. https://consensys.net/blog/blockchain-development/guide-to-events-and-logs-in-ethereum-smart-contracts, 2016.
  2. Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. A survey of attacks on Ethereum smart contracts. In Principles of Security and Trust, volume 10204 of Lecture Notes in Computer Science, pages 164-186. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54455-6_8.
  3. Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects, volume 4111 of LNCS, pages 364-387. Springer, 2006. Google Scholar
  4. Huashan Chen, Marcus Pendleton, Laurent Njilla, and Shouhuai Xu. A survey on Ethereum systems security: Vulnerabilities, attacks, and defenses. ACM Comput. Surv., 53(3), 2020. Google Scholar
  5. J. Chen, X. Xia, D. Lo, J. Grundy, X. Luo, and T. Chen. Defining smart contract defects on Ethereum. IEEE Transactions on Software Engineering, 2020. Early access. Google Scholar
  6. Séverine Colin and Leonardo Mariani. Run-time verification. In Model-Based Testing of Reactive Systems: Advanced Lectures, volume 3472 of Lecture Notes in Computer Science, chapter 18, pages 525-555. Springer, 2005. Google Scholar
  7. Josselin Feist, Gustavo Greico, and Alex Groce. Slither: A static analysis framework for smart contracts. In Proc. of the 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain, pages 8-15. IEEE, 2019. Google Scholar
  8. Ákos Hajdu and Dejan Jovanović. SMT-friendly formalization of the solidity memory model. In Programming Languages and System, volume 12075 of Lecture Notes in Computer Science, pages 224-250. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-44914-8_9.
  9. Ákos Hajdu and Dejan Jovanović. solc-verify: A modular verifier for Solidity smart contracts. In Verified Software. Theories, Tools, and Experiments, volume 12301 of Lecture Notes in Computer Science, pages 161-179. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-41600-3_11.
  10. Ao Li, Jemin Andrew Choi, and Fan Long. Securing smart contract with runtime validation. In Proc. of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, page 438–453. ACM, 2020. Google Scholar
  11. Shiqing Ma, Juan Zhai, Fei Wang, Kyu Hyung Lee, Xiangyu Zhang, and Dongyan Xu. MPI: Multiple perspective attack investigation with semantic aware execution partitioning. In Proc. of the 26th USENIX Security Symposium, pages 1111-1128. USENIX Association, 2017. Google Scholar
  12. Bernhard Mueller. Smashing Ethereum smart contracts for fun and real profit. In Proc. of the 9th Annual HITB Security Conference (HITBSecConf), 2018. Google Scholar
  13. A. Permenev, D. Dimitrov, P. Tsankov, D. Drachsler-Cohen, and M. Vechev. VerX: Safety verification of smart contracts. In Proc. of the 2020 IEEE Symposium on Security and Privacy, pages 414-430. IEEE, 2020. Google Scholar
  14. Solidity documentation. https://solidity.readthedocs.io, 2020.
  15. Nick Szabo. Smart contracts. https://web.archive.org/web/20011102030833/http://szabo.best.vwh.net:80/smart.contracts.html, 1994.
  16. 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 Verified Software. Theories, Tools, and Experiments, volume 12031 of Lecture Notes in Computer Science, pages 87-106. Springer, 2020. Google Scholar
  17. Gavin Wood. Ethereum: A secure decentralised generalised transaction ledger. https://ethereum.github.io/yellowpaper/paper.pdf, 2019.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact