@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 = {https://symposium-dlt.org/3rd/}, 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.}, venue = {Gold Coast, Australia}, eventdate = {2018-11-12/2018-11-12} }
Formal Specification and Verification of Hyperledger Fabric Chaincode
Author(s): | Bernhard Beckert, Mihai Herda, Michael Kirsten, and Jonas Schiffl |
---|---|
In: | 3rd Symposium on Distributed Ledger Technology (SDLT-2018) co-located with ICFEM 2018: the 20th International Conference on Formal Engineering Methods |
Year: | 2018 |
URL: | https://symposium-dlt.org/3rd/ |
Links: | Preprint |
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.