KIT | KIT-Bibliothek | Impressum | Datenschutz

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

Schiffl, Jonas ORCID iD icon; Grundmann, Matthias ORCID iD icon; Leinweber, Marc ORCID iD icon; Stengele, Oliver ORCID iD icon; Friebe, Sebastian; Beckert, Bernhard ORCID iD icon

Abstract (englisch):

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. ... mehr


Postprint §
DOI: 10.5445/IR/1000134475
Veröffentlicht am 12.06.2022
Originalveröffentlichung
DOI: 10.1145/3450569.3463574
Scopus
Zitationen: 1
Dimensions
Zitationen: 1
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Telematik (TM)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsmonat/-jahr 06.2021
Sprache Englisch
Identifikator ISBN: 978-1-4503-8365-3
KITopen-ID: 1000134475
HGF-Programm 46.23.01 (POF IV, LK 01) Methods for Engineering Secure Systems
Erschienen in SACMAT '21: Proceedings of the 26th ACM Symposium on Access Control Models and Technologies
Veranstaltung 26th ACM Symposium on Access Control Models and Technologies (SACMAT 2021), Barcelona, Spanien, 16.06.2021 – 18.06.2021
Verlag Association for Computing Machinery (ACM)
Seiten 125–130
Vorab online veröffentlicht am 11.06.2021
Nachgewiesen in Dimensions
Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page