A Modeling and Verification Framework for Ethereum Smart Contracts

Simone Valentini, Chiara Braghin, Elvinia Riccobene
Digital Printed Abstract View Cite
Type
Case Study
Publication
10th International Conference on Rigorous State Based Methods (ABZ'24)

Abstract

Blockchain has shown to be a versatile technology with applications ranging from financial services and supply chain management to healthcare, identity verification, etc. Thanks to the usage of smart contracts, blockchain can streamline and automate complex processes, eliminating the need for intermediaries and reducing administrative overhead. Smart contracts often handle valuable assets and execute critical functions, making them attractive targets for attackers. Thus, secure and reliable smart contracts are necessary. The long-term research we present aims to face the problem of safety and security assurance of smart contracts at design time. We are investigating the usage of the Abstract State Machine (ASM) formal method for the specification, validation, and verification of Ethereum smart contracts. We provide (i) a set of ASM libraries that simplify smart contracts modeling, (ii) models of malicious contracts to be used to check the robustness of a contract against some given attacks, (iii) patterns of properties to be checked to guarantee the operational correctness of the contract and its adherence to certain predefined properties.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{ValentiniBR24,
  author       = {Simone Valentini and
                  Chiara Braghin and
                  Elvinia Riccobene},
  editor       = {Silvia Bonfanti and
                  Angelo Gargantini and
                  Michael Leuschel and
                  Elvinia Riccobene and
                  Patrizia Scandurra},
  title        = {A Modeling and Verification Framework for Ethereum Smart Contracts},
  booktitle    = {Rigorous State-Based Methods - 10th International Conference, {ABZ}
                  2024, Bergamo, Italy, June 25-28, 2024, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14759},
  pages        = {201--207},
  publisher    = {Springer},
  year         = {2024},
  url          = {https://doi.org/10.1007/978-3-031-63790-2\_13},
  doi          = {10.1007/978-3-031-63790-2\_13},
  timestamp    = {Fri, 19 Jul 2024 23:15:46 +0200},
  biburl       = {https://dblp.org/rec/conf/zum/ValentiniBR24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'24

Related