Document Open Access Logo

A Practical Notion of Liveness in Smart Contract Applications

Authors Jonas Schiffl , Bernhard Beckert

PDF
Thumbnail PDF

File

OASIcs.FMBC.2024.8.pdf
  • Filesize: 0.61 MB
  • 13 pages

Document Identifiers

Author Details

Jonas Schiffl
  • KASTEL - Institute of Information Security and Dependability, Karlsruhe Institute of Technology, Germany
Bernhard Beckert
  • KASTEL - Institute of Information Security and Dependability, Karlsruhe Institute of Technology, Germany

Funding

This work was supported by funding from the topic Engineering Secure Systems of the Helmholtz Association (HGF) and by KASTEL Security Research Labs.

Cite As Get BibTex

Jonas Schiffl and Bernhard Beckert. A Practical Notion of Liveness in Smart Contract Applications. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 8:1-8:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/OASIcs.FMBC.2024.8

Abstract

Smart contracts are programs which manage resources in blockchain networks in an automated fashion. In this context, liveness properties are often essential: If I transfer money to a contract, will I eventually get it back?
This kind of property can be hard to specify and verify, in particular because application-specific fairness assumptions w.r.t. function invocation and the behavior of other parties are usually necessary for any liveness proof to succeed. In this work, we analyze smart contract liveness properties discussed in the literature. We find that the smart contract paradigm of decentralization and trustlessness implies that "real" liveness properties do not usually occur. The properties that have been classified as liveness can be more aptly described as enabledness, i.e., the ability of an agent to induce a state change, such as a transfer of resources.
Our contribution in this work is a specification language based on LTL to capture this kind of property. It features some special constructs to describe common properties in smart contracts, such as transfers or ownership of cryptocurrency. We show how often-used examples of liveness properties can be succinctly specified in our language. Moreover, we show how our notion of liveness can simplify formal verification compared to existing approaches.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
Keywords
  • Smart Contracts
  • Formal Verification
  • Security
  • Safety and Liveness

Metrics

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

References

  1. Patrick Baudin, Vincent Prevosto, Jean-Christophe Filliâtre, Yannick Moy, Benjamin Monate, and Claude Marché. ANSI/ISO C Specification Language (version 1.4), 2008. Google Scholar
  2. Samvid Dharanikota, Suvam Mukherjee, Chandrika Bhardwaj, Aseem Rastogi, and Akash Lal. Celestial: A Smart Contracts Verification Framework. In 2021 Formal Methods in Computer Aided Design (FMCAD), pages 133-142, oct 2021. URL: https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_22.
  3. Javier Godoy, Juan Pablo Galeotti, Diego Garbervetsky, and Sebastian Uchitel. Predicate abstractions for smart contract validation. In Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems, MODELS '22, pages 289-299, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3550355.3552462.
  4. Akos Hajdu and Dejan Jovanovic. Solc-verify: A modular verifier for solidity smart contracts. In Supratik Chakraborty and Jorge A. Navas, editors, Verified Software. Theories, Tools, and Experiments, pages 161-179, Cham, 2020. URL: https://doi.org/10.1007/978-3-030-41600-3_11.
  5. Daojing He, Rui Wu, Xinji Li, Sammy Chan, and Mohsen Guizani. Detection of Vulnerabilities of Blockchain Smart Contracts. IEEE Internet of Things Journal, pages 1-1, 2023. URL: https://doi.org/10.1109/JIOT.2023.3241544.
  6. Gary T Leavens, Albert L Baker, and Clyde Ruby. JML: A Java modeling language. In Formal Underpinnings of Java Workshop (at OOPSLA'98), pages 404-420, 1998. Google Scholar
  7. Matteo Marescotti, Rodrigo Otoni, Leonardo Alt, Patrick Eugster, Antti E. J. Hyvärinen, and Natasha Sharygina. Accurate Smart Contract Verification Through Direct Modelling. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Applications, LNCS, pages 178-194, Cham, 2020. URL: https://doi.org/10.1007/978-3-030-61467-6_12.
  8. Anastasia Mavridou, Aron Laszka, Emmanouela Stachtiari, and Abhishek Dubey. VeriSolid: Correct-by-Design Smart Contracts for Ethereum. In Ian Goldberg and Tyler Moore, editors, Financial Cryptography and Data Security, pages 446-465, Cham, 2019. URL: https://doi.org/10.1007/978-3-030-32101-7_27.
  9. Sundas Munir and Walid Taha. Pre-deployment Analysis of Smart Contracts - A Survey, jan 2023. URL: https://doi.org/10.48550/arXiv.2301.06079.
  10. Wonhong Nam and Hyunyoung Kil. Formal verification of blockchain smart contracts via atl model checking. IEEE Access, 10:8151-8162, 2022. URL: https://doi.org/10.1109/ACCESS.2022.3143145.
  11. Keerthi Nelaturu, Anastasia Mavridou, Andreas Veneris, and Aron Laszka. Verified Development and Deployment of Multiple Interacting Smart Contracts with VeriSolid. In 2020 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), pages 1-9, may 2020. URL: https://doi.org/10.1109/ICBC48266.2020.9169428.
  12. Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, and Martin Vechev. VerX: Safety Verification of Smart Contracts. In 2020 IEEE Symposium on Security and Privacy (SP), pages 1661-1677, may 2020. URL: https://doi.org/10.1109/SP40000.2020.00024.
  13. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pages 46-57. ieee, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  14. Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu Lahiri, and Isil Dillig. SmartPulse: Automated Checking of Temporal Properties in Smart Contracts. In 2021 IEEE Symposium on Security and Privacy (SP), pages 555-571, may 2021. URL: https://doi.org/10.1109/SP40001.2021.00085.
  15. Shufang Zhu, Lucas M Tabajara, Jianwen Li, Geguang Pu, and Moshe Y Vardi. A symbolic approach to safety ltl synthesis. In Hardware and Software: Verification and Testing: 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017, Proceedings 13, pages 147-162. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-70389-3_10.
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