Formal Specification and Verification of Hyperledger Fabric Chaincode

@InProceedings{BeckertHerdaKirstenEA2018,
  author                = {Bernhard Beckert and
                           Mihai Herda and
                           Michael Kirsten and
                           Jonas Schiffl},
  title                 = {Formal Specification and Verification of Hyperledger Fabric Chaincode},
  booktitle             = {3rd Symposium on Distributed Ledger Technology (SDLT-2018)
                           co-located with ICFEM 2018: the 20th International Conference
                           on Formal Engineering Methods},
  editor                = {Guangdong Bai and Kamanashis Biswas},
  month                 = nov,
  year                  = {2018},
  note                  = {Accepted.},
  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.},
  place                 = {Gold Coast, Australia},
  date                  = {November 12}
}