Search Results

Documents authored by Schiffl, Jonas


Document
A Practical Notion of Liveness in Smart Contract Applications

Authors: Jonas Schiffl and Bernhard Beckert

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)


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.

Cite as

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)


Copy BibTex To Clipboard

@InProceedings{schiffl_et_al:OASIcs.FMBC.2024.8,
  author =	{Schiffl, Jonas and Beckert, Bernhard},
  title =	{{A Practical Notion of Liveness in Smart Contract Applications}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{8:1--8:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.8},
  URN =		{urn:nbn:de:0030-drops-198732},
  doi =		{10.4230/OASIcs.FMBC.2024.8},
  annote =	{Keywords: Smart Contracts, Formal Verification, Security, Safety and Liveness}
}
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