Home  |  english  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

Specification and Verification of Hyperledger Fabric Chaincode

Masterarbeit

Autor(en):Jonas Schiffl
Hochschule:Karlsruhe Institute of Technology
Jahr:2018

Abstract

Smart contracts are programs that work on top of distributed ledgers. They regulate access to the ledger and define the assets that are managed in a blockchain network. Due to the nature of blockchain networks, smart contracts can be read by all agents on the network, and they cannot usually be changed after deployment. This makes programming errors in smart contracts highly severe and necessitates the use of formal methods: Smart contracts must be formally specified to establish consensus about their intended behavior, and adherence to the specification must be proven. In this work, we present an approach to specification and verification of smart contracts for Hyperledger Fabric, a platform for operating private, permissionless smart contract networks. We use the KeY tool for formal verification, and extend the tool to allow reasoning about serialization and persistent storage. The feasibility of our approach is demonstrated in a case study.

BibTeX

@mastersThesis{SchifflMSc2018,
  author   = {Jonas Schiffl},
  title    = {Specification and Verification of Hyperledger Fabric Chaincode},
  school   = {Karlsruhe Institute of Technology},
  month    = dec,
  year     = {2018},
  language = {english},
  abstract = {Smart contracts are programs that work on top of distributed
              ledgers. They regulate access to the ledger and define the
              assets that are managed in a blockchain network. Due to the
              nature of blockchain networks, smart contracts can be read
              by all agents on the network, and they cannot usually be
              changed after deployment. This makes programming errors in
              smart contracts highly severe and necessitates the use of
              formal methods: Smart contracts must be formally specified
              to establish consensus about their intended behavior, and
              adherence to the specification must be proven. In this work,
              we present an approach to specification and verification of
              smart contracts for Hyperledger Fabric, a platform for
              operating private, permissionless smart contract networks.
              We use the KeY tool for formal verification, and extend the
              tool to allow reasoning about serialization and persistent
              storage. The feasibility of our approach is demonstrated in
              a case study.},
  location = {Karlsruhe, Germany}
}