Specification and Verification of Hyperledger Fabric Chaincode

@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}
}