In an announcement this week, Azure Blockchain Services explains how smart contracts have been fundamental to the success of blockchain. A smart contract is a software program that operated atop blockchain as a transparent level of verification. However, exploits in smart contracts can harm the trust customers place in blockchain. Furthermore, smart contracts can be a hassle to manage, especially in terms of issuing fixes. Microsoft aimed to bolster smart contracts within its own Azure Blockchain. The resulting VeriSol (Verifier for Solidity) allows developers to create smart contracts within the secure Solidity language. Microsoft has already implemented VeriSol into its own blockchain solutions and has now open sourced the service. “VeriSol allows us to iterate more quickly because of the automatic and continuous checking, and it allows us to catch bugs faster without having to worry about potentially affecting customers,” says Cody Born, Senior Software Engineer on the Azure Blockchain team. “The use of formal verification for production software requires individuals skilled in highly specialized formal languages and tools, which imposes on development teams a steep learning cost and often several person-years of investment to break down the highly sophisticated task of verification into those that can be discharged mechanically by the verification tools,” added Microsoft Principal Researcher Shuvendu Lahiri, one of several researchers behind VeriSol. “Such investment has confined the use and success of formal verification to a very small number of safety critical hardware and software components.”
New Formal Verification
While smart contracts can be vulnerable, they are excellent choices for automated formal verification. Microsoft points to reduced code size and sequential execution semantic as positives for smart contracts. The company says VeriSol has already been used in its own services: “In one application, the VeriSol team used the verifier to formalize and check specifications of the smart contracts that govern consortium members in Ethereum on Azure and Azure Blockchain Service. The governance smart contracts are designed to efficiently manage memberships in a consortium setting, where—unlike in public blockchains—the ledger is restricted to a group of members who are aware of the identities of other members.” VeriSol works by encoding the semantics of Solidity programs into a formal verification language called Boogie.
