KIT | KIT-Bibliothek | Impressum | Datenschutz

Smart Contracts: Application Scenarios for Deductive Program Verification

Beckert, Bernhard; Schiffl, Jonas; Ulbrich, Mattias

Abstract:
Smart contracts are programs that run on a distributed ledger platform. They usually manage resources representing valuable assets. Moreover, their source code is visible to potential attackers, they are distributed, and bugs are hard to fix. Thus, they are susceptible to attacks exploiting programming errors. Their vulnerability makes a rigorous formal analysis of the functional correctness of smart contracts highly desirable.
In this short paper, we show that the architecture of smart contract platforms offers a computation model for smart contracts that yields itself naturally to deductive program verification. We discuss different classes of correctness properties of distributed ledger applications, and show that design-by-contract verification tools are suitable to prove these properties. We present experiments where we apply the KeY verification tool to smart contracts in the Hyperledger Fabric framework which are implemented in Java and specified using the Java Modeling Language.

Open Access Logo


Postprint §
DOI: 10.5445/IR/1000120220
Veröffentlicht am 01.11.2020
Originalveröffentlichung
DOI: 10.1007/978-3-030-54994-7_21
Dimensions
Zitationen: 1
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsmonat/-jahr 10.2019
Sprache Englisch
Identifikator ISBN: 978-3-030-54993-0
ISSN: 0302-9743
KITopen-ID: 1000120220
Erschienen in Formal Methods. FM 2019 International Workshops : Porto, Portugal, October 7–11, 2019, Revised Selected Papers, Part I. Ed.: Emil Sekerinski
Verlag Springer
Serie Programming and Software Engineering ; 12232
Bemerkung zur Veröffentlichung FMBC - 1st Workshop on Formal Methods for Blockchains - hosted by the 3rd Formal Methods World Congress on October 11, 2019 in Porto, Portugal
Nachgewiesen in Dimensions
Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page