Formal Specification and Verification of Smart Contracts for Azure Blockchain
Abstract
Ensuring correctness of smart contracts is paramount to ensuring trust in blockchain-based systems. This paper studies the safety and security of smart contracts in the \emph{Azure Blockchain Workbench}, an enterprise Blockchain-as-a-Service offering from Microsoft. As part of this study, we formalize \emph{semantic conformance} of smart contracts against a state machine model with access-control policy and develop a highly-automated formal verifier for Solidity that can produce proofs as well as counterexamples. We have applied our verifier {\sc VeriSol} to analyze {\it all} contracts shipped with the Azure Blockchain Workbench, which includes application samples as well as a governance contract for Proof of Authority (PoA). We have found previously unknown bugs in these published smart contracts. After fixing these bugs, {\sc VeriSol} was able to successfully perform full verification for all of these contracts.
Keywords
Cite
@article{arxiv.1812.08829,
title = {Formal Specification and Verification of Smart Contracts for Azure Blockchain},
author = {Yuepeng Wang and Shuvendu K. Lahiri and Shuo Chen and Rong Pan and Isil Dillig and Cody Born and Immad Naseer},
journal= {arXiv preprint arXiv:1812.08829},
year = {2019}
}
Comments
13 pages