DROPS

Document

Tool Paper

DOI: 10.4230/OASIcs.FMBC.2025.14

Scar: Verification-Based Development of Smart Contracts (Tool Paper)

Authors: Jonas Schiffl and Bernhard Beckert

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract

Compared to other kinds of computer programs, smart contracts have some unique characteristics, e.g., immutability, and the public availability of source code. This means that any vulnerability has a large probability of being exploited. Since smart contracts cannot be patched, it is very important that smart contracts are correct and secure upon deployment. While much research has been invested in this goal, smart contract correctness and security remains a challenging problem. In this paper, we present the Scar approach for model-driven development of correct and secure smart contract applications. Before implementing an application, smart contract developers first describe it in terms of an intuitive, platform-agnostic metamodel. Within this model, they can also specify high-level security and behavioral correctness properties, and check whether the model contains any inconsistencies. Finally, a combination of code generation, static analyses, and formal verification of automatically generated formal annotations leads to an implementation that is correct and secure w.r.t. the initial model.

Cite as

Jonas Schiffl and Bernhard Beckert. Scar: Verification-Based Development of Smart Contracts (Tool Paper). In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 14:1-14:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{schiffl_et_al:OASIcs.FMBC.2025.14,
  author =	{Schiffl, Jonas and Beckert, Bernhard},
  title =	{{Scar: Verification-Based Development of Smart Contracts}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{14:1--14:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.14},
  URN =		{urn:nbn:de:0030-drops-230410},
  doi =		{10.4230/OASIcs.FMBC.2025.14},
  annote =	{Keywords: Smart Contracts, Formal Verification, Security, Safety and Liveness}
}

Document

DOI: 10.4230/OASIcs.FMBC.2024.8

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}
}

Search Results

Documents authored by Beckert, Bernhard

Scar: Verification-Based Development of Smart Contracts (Tool Paper)

Abstract

Cite as

A Practical Notion of Liveness in Smart Contract Applications

Abstract

Cite as

Thanks for your feedback!

Could not send message