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.
@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},
url = {http://symposium-dlt.org/},
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}
}