Formal Specification and Verification of Smart Contracts for Azure Blockchain

TL;DR

This paper presents a formal verification approach for Azure Blockchain smart contracts, introducing VeriSol, which automatically checks contract correctness, finds bugs, and ensures security in enterprise blockchain applications.

Contribution

It develops VeriSol, a highly-automated formal verifier for Solidity, and applies it to all Azure Blockchain Workbench contracts, uncovering and fixing previously unknown bugs.

Findings

VeriSol successfully verified all analyzed contracts after bug fixes.

The verifier identified previously unknown bugs in Azure Blockchain contracts.

All contracts became fully verified post-bug fixes.

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.