> Details

Schiffl, Jonas [Author]; Grundmann, Matthias [Author]; Leinweber, Marc [Author]; Stengele, Oliver [Author]; Friebe, Sebastian [Author]; Beckert, Bernhard [Author]

Towards Correct Smart Contracts: A Case Study on Formal Verification of Access Control

Reference
management

Bookmarks

Remove from
bookmarks

Share this on Whatsapp

Close

Bookmarks



You can manage bookmarks using lists, please log in to your user account for this.
  • Media type: Electronic Conference Proceeding; Text; E-Article
  • Title: Towards Correct Smart Contracts: A Case Study on Formal Verification of Access Control
  • Contributor: Schiffl, Jonas [Author]; Grundmann, Matthias [Author]; Leinweber, Marc [Author]; Stengele, Oliver [Author]; Friebe, Sebastian [Author]; Beckert, Bernhard [Author]
  • Published: Association for Computing Machinery, 2021-06-28
  • Language: English
  • DOI: https://doi.org/10.5445/IR/1000134475; https://doi.org/10.1145/3450569.3463574
  • ISBN: 978-1-4503-8365-3
  • Keywords: DATA processing & computer science
  • Origination:
  • Footnote: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Description: Ethereum is a platform for deploying smart contracts, which due to their public nature and the financial value of the assets they manage are attractive targets for attacks. With asset management as a main task of smart contracts, access control aspects are naturally part of the application itself, but also of the functions implemented in a smart contract. Therefore, it is desirable to establish the correctness of smart contracts and their access control on application and single-function level through formal methods. However, there is no established methodology of formalising and verifying correctness properties of smart contracts. In this work, we make an attempt in this direction on the basis of a case study. We choose an existing smart contract application which aims to ascertain the integrity of binary files distributed over the Internet by means of decentralised identity management and access control. We formally specify and verify correctness at the level of single functions as well as temporal properties of the overall application. We demonstrate how to use verified low-level correctness properties for showing correctness at the higher level. In addition, we report on our experience with existing verification tools.
  • Access State: Open Access