KIT | KIT-Bibliothek | Impressum | Datenschutz

Smart Contracts: Application Scenarios for Deductive Program Verification

Beckert, Bernhard ORCID iD icon 1; Schiffl, Jonas ORCID iD icon 1; Ulbrich, Mattias ORCID iD icon 1
1 Karlsruher Institut für Technologie (KIT)

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.


Postprint §
DOI: 10.5445/IR/1000120220
Veröffentlicht am 19.06.2020
Originalveröffentlichung
DOI: 10.1007/978-3-030-54994-7_21
Scopus
Zitationen: 2
Dimensions
Zitationen: 2
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsdatum 13.08.2020
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
Seiten 293-298
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 Scopus
Dimensions
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page