Document Open Access Logo

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

Authors Jonas Schiffl , Bernhard Beckert

PDF

File

Thumbnail PDF
PDF
OASIcs.FMBC.2025.14.pdf
  • Filesize: 0.87 MB
  • 13 pages

Document Identifiers

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

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 Get BibTex

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) https://doi.org/10.4230/OASIcs.FMBC.2025.14

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.

References

  1. CertiK. CertiK - Securing The Web3 World, 2024. URL: https://www.certik.com.
  2. Stefanos Chaliasos, Marcos Antonios Charalambous, Liyi Zhou, Rafaila Galanopoulou, Arthur Gervais, Dimitris Mitropoulos, and Ben Livshits. Smart Contract and DeFi Security: Insights from Tool Evaluations and Practitioner Surveys, April 2023. URL: https://doi.org/10.48550/arXiv.2304.02981.
  3. 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, October 2021. URL: https://doi.org/10.34727/2021/ISBN.978-3-85448-046-4_22.
  4. David Gerard. Attack of the 50 Foot Blockchain, June 2024. URL: https://davidgerard.co.uk/blockchain/.
  5. 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. Springer International Publishing. Google Scholar
  6. 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. Google Scholar
  7. Anastasia Mavridou and Aron Laszka. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. In Sarah Meiklejohn and Kazue Sako, editors, Financial Cryptography and Data Security, pages 523-540, Berlin, Heidelberg, 2018. Springer. URL: https://doi.org/10.1007/978-3-662-58387-6_28.
  8. B. Meyer. Applying 'design by contract'. Computer, 25(10):40-51, October 1992. Google Scholar
  9. Sundas Munir and Walid Taha. Pre-deployment Analysis of Smart Contracts - A Survey, January 2023. URL: https://doi.org/10.48550/arXiv.2301.06079.
  10. 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.
  11. Jonas Schiffl. Jonas Schiffl / Scar ⋅ GitLab, June 2024. URL: https://gitlab.kit.edu/jonas.schiffl/Scar.
  12. Jonas Schiffl and Bernhard Beckert. A Practical Notion of Liveness in Smart Contract Applications. In OASIcs FMBC 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/OASICS.FMBC.2024.8.
  13. Jonas Schiffl, Alexander Weigl, and Bernhard Beckert. Static Capability-based Security for Smart Contracts. In 2023 IEEE International Conference on Decentralized Applications and Infrastructures (DAPPS), Athens, July 2023. Google Scholar
  14. Oliver Stengele, Andreas Baumeister, Pascal Birnstill, and Hannes Hartenstein. Access Control for Binary Integrity Protection using Ethereum. In Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, SACMAT '19, pages 3-12, New York, NY, USA, May 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3322431.3325108.
  15. 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.
  16. Molly White. Web3 is Going Just Great, February 2024. URL: https://web3isgoinggreat.com/.
  17. Zhuo Zhang, Brian Zhang, Wen Xu, and Zhiqiang Lin. Demystifying Exploitable Bugs in Smart Contracts. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE), pages 615-627, May 2023. URL: https://doi.org/10.1109/ICSE48619.2023.00061.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact