KIT | KIT-Bibliothek | Impressum | Datenschutz

Formal Specification and Verification of Hyperledger Fabric Chaincode

Beckert, Bernhard; Herda, Mihai; Kirsten, Michael; Schiffl, Jonas

Abstract:
Smart contracts are programs building on blockchain technology.
They implement functionality that has been agreed on between
the concerned parties on a network. However, their immutability
and exposed position make them vulnerable to programming errors,
leading to faulty behavior and possible exploits. Therefore,
smart contracts demand a particularly thorough analysis,
ideally using formal program verification. In this paper, we
present an approach for the deductive verification of
Hyperledger Fabric smart contracts using the KeY prover.
We have extended KeY to handle Fabric ledger implementations;
in particular, we have developed mechanisms for reasoning about
serialization and object persistence. The feasibility of our
approach is demonstrated with a small case study.

Open Access Logo


Postprint §
DOI: 10.5445/IR/1000092715
Frei zugänglich ab 13.11.2019
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Jahr 2018
Sprache Englisch
Identifikator urn:nbn:de:swb:90-927156
KITopen-ID: 1000092715
Erschienen in 3rd Symposium on Distributed Ledger Technology (SDLT-2018) co-located with ICFEM 2018: the 20th International Conference on Formal Engineering Methods, Gold Coast, Australia, November 12, 2018
Verlag Institute for Integrated and Intelligent Systems, Griffith University, Australia
Seiten 44–48
Schlagworte formal program verification blockchain smart contract Hyperledger Fabric
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page