Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain
- Yuepeng Wang ,
- Shuvendu Lahiri ,
- Shuo Chen ,
- Rong Pan ,
- Isil Dillig ,
- Cody Born ,
- Immad Naseer ,
- Kostas Ferles
Verified Software: Theories, Tools and Experiments |
Published by Springer
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 Azure Blockchain Workbench, an enterprise Blockchain-as-a-Service offering from Microsoft.
In particular, we formalize semantic conformance of smart contracts against a state machine workflow with access-control policy and propose an approach to reducing semantic conformance checking to safety verification using program instrumentation.
We develop a new Solidity program verifier VeriSol that is based on translation to Boogie, and have applied it to analyze all application contracts shipped with the Azure Blockchain Workbench and found previously unknown bugs in these published smart contracts.
After fixing these bugs, VeriSol was able to successfully perform full verification for all of these contracts.