Paper Info
Title
Towards Correct Smart Contracts: A Case Study on Formal Verification of Access Control
Abstract
ABSTRACTEthereum 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.
Year
DOI
Venue
2021
10.1145/3450569.3463574
SACMAT
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
0
6
Name
Order
Citations
PageRank
Jonas Schiffl101.35
Matthias Grundmann221.07
Marc Leinweber320.73
Oliver Stengele401.01
Sebastian Friebe502.70
Bernhard Beckert686286.50