KIT | KIT-Bibliothek | Impressum | Datenschutz

Formal Specification and Verification of Hyperledger Fabric Chaincode

Beckert, Bernhard ORCID iD icon; Herda, Mihai; Kirsten, Michael ORCID iD icon; Schiffl, Jonas ORCID iD icon


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.

Postprint §
DOI: 10.5445/IR/1000092715
Veröffentlicht am 13.11.2019
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsdatum 12.11.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
Seiten 44–48
Schlagwörter formal program verification, blockchain, smart contract, Hyperledger Fabric
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page