Formal Specification and Verification of Smart Contracts for Azure Blockchain
share
In this paper, we describe the formal verification of Smart Contracts offered as part of the Azure Blockchain Content and Samples on github. We describe two sources of formal verification problems: (i) semantic conformance checking of smart contracts against a state-machine and access control based Azure Blockchain Workbench application configuration, and (ii) safety verification for smart contracts implementing the authority governance in Ethereum Proof-of-Authority (PoA) on Azure. We describe a new program verifier VeriSol for Solidity based on a translation to Boogie and leveraging the Boogie verification toolchain. We describe our experience applying VeriSol to Workbench sample contracts and Proof of Authority governance contracts in Azure, and finding previously unknown bugs in well-tested smart contracts. We provide push-button unbounded verification for the semantic conformance checking for all the sample contracts shipped in Workbench, once the bugs are fixed.
READ FULL TEXT