In its young existence, the tamperproof and distributed ledger technology blockchain has already generated a lot of buzz and is being seen as disruptive, influencing approaches in such diverse areas as financial services, supply chains, and governance. To say its future is bright might be an understatement. According to Gartner, the technology is positioned to bring an added business value upward of $360 billion by 2026.
One of the key drivers making blockchain-based applications programmable, accessible to enterprise customers, and able to meet the diverse needs of a variety of sectors is the smart contract, a type of software program running on top of the technology. Because of the immutable nature and extreme transparency inherent in smart contracts, they foster trust in adversarial environments, but also make it challenging to secure compared to traditional code.
Microsoft Research Podcast
AI Frontiers: Models and Systems with Ece Kamar
Ece Kamar explores short-term mitigation techniques to make these models viable components of the AI systems that give them purpose and shares the long-term research questions that will help maximize their value.
Recent high-profile breaches in public blockchains such as the The DAO exploit and the Parity wallet bug—which resulted in the loss and freezing, respectively, of millions of dollars in cryptocurrency—demonstrate what’s at stake when vulnerabilities in smart contracts are exploited; they significantly undermine the trust in blockchain technologies. To make matters worse, performing bug fixes for smart contracts post-deployment is no small matter, incurring a great cost in both time and money.
The Microsoft Azure Blockchain team, which delivers products and services for creating, deploying, and managing end-to-end blockchain-powered applications to enterprise customers, takes these threats seriously. Smart contracts play an integral role in their blockchain offerings—from administering the governance of consortium members in Azure Blockchain Service to implementing proof-of-concept solutions with Azure Blockchain Workbench. The team also offers an Azure Blockchain development kit for rapidly deploying smart contracts from Visual Studio Code, Logic Apps, and Microsoft Flow.
With a vision of fortifying smart contracts in Azure Blockchain, the team found a partner in researchers at Microsoft Research working on advanced techniques for ensuring correctness of software programs. The collaboration has resulted in VeriSol, a brand-new open-source formal verification tool being developed by the researchers. With VeriSol—short for Verifier for Solidity—developers can begin to express the desirable behaviors of smart contracts written in a subset of the popular Solidity language and then use mathematical logic machinery to rigorously check those specifications against the implementation. It has recently been incorporated into Azure Blockchain’s continuous integration pipeline for smart contract development.
“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.
Formal verification and smart contracts a perfect match
Formal verification has long been viewed as the only option to rigorous verification of safety-critical components in hardware and software. However, there is a caveat.
“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,” explains 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.”
But smart contracts possess several characteristics that make them a great candidate for bringing automated formal verification to mainstream smart contract developers.
“The modest code size and the sequential execution semantics of smart contracts make them amenable to scalable verification, and the open operating environment substantially reduces the need to manually model the environment in which a smart contract operates,” says Lahiri, who has spent the last decade leveraging and adapting formal verification techniques for highly automated and high-coverage bug finding in operating system and browser components.
So Lahiri, Microsoft Senior Researcher and security expert Shuo Chen, and The University of Texas at Austin’s Yuepeng Wang, a Microsoft intern at the time of the work, and Isil Dillig, a visiting researcher, set out on a journey in the summer of 2018 to help Azure Blockchain—and ultimately its customers—author safer and higher-quality smart contracts.
With VeriSol, Born and his fellow developers, including Microsoft Software Engineer Xinxing Liu, can begin to specify and prove the security of their work in ways not feasible before. More traditional testing relies on developers’ ability to foresee exactly how a product will be used, an exercise that involves some corner cases being overlooked, as humans can only think of so many different logical test cases, says Born. But formal verification automatically identifies the different ways the code could potentially violate a given invariant, including those cases developers can’t predict.
Smart contracts in Azure Blockchain
Even in its nascent existence, VeriSol has been applied to a diverse set of smart contracts in the Azure Blockchain ecosystem.
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. Formal verification of such governance contracts can help ensure the management of membership—how members are admitted and removed and how they vote on proposals and other matters, for example—is carried out in the way Microsoft specified for its customers.
In another study, the team applied VeriSol to smart contracts implementing proof-of-concept enterprise workflow applications on Azure Blockchain Workbench. A workflow application consists of a high-level workflow policy described as a state machine, where transitions are predicated by role-based access control, and a Solidity smart contract that implements the state machine, along with the business logic, on the blockchain. It is crucial to the reliability and security of the application to ensure the Solidity program correctly implements the workflow policy, explains Lahiri. VeriSol was used to check the “semantic conformance” of such applications—that is, that state machines implemented in the smart contract and specified in the workflow policy are never out of sync during deployment.
“Many enterprise multiparty workflows naturally fit into a state-machine pattern that can easily be represented by a smart contract,” says Lahiri. “The ability to leverage the high-level workflow policies as formal specifications to be checked against Solidity code provides an exciting opportunity to bring formal verification seamlessly to customers of Workbench without the upfront burden of requiring explicit formal specifications from them.”
Along the way, VeriSol automatically revealed subtle bugs that were fixed during development and helped perform full correctness proofs of most properties and invariants with high levels of automation.
Standing on the shoulder of giants
VeriSol operates by encoding the semantics of Solidity programs into the formal intermediate verification language Boogie and leveraging and extending the Boogie verification toolchain. It supports high-coverage symbolic testing for finding counterexample traces automatically, as well as performing correctness proofs automatically or with some user guidance.
VeriSol is built on a decade of work in verification already undertaken by Microsoft and its researchers as part of the company’s larger commitment to security, the user experience, and high-quality, state-of-the-art products and services. That work includes such verification components as Z3, Corral, and Boogie. These components, all of which are open-source, represent well-tested and established techniques without which VeriSol would not be possible.
VeriSol—short for Verifier for Solidity—is a brand-new open-source formal verification tool being designed to improve the quality of smart contracts written in a subset of the Solidity language using the Boogie verification toolchain.
However, the journey is far from complete.
The VeriSol team is not only actively working toward supporting a large enough subset of Solidity that covers most enterprise smart contracts while keeping the verification tractable, but is also developing a code-contracts library to allow users to write expressive yet concise specifications and invariants without leaving the comforts of Solidity. Finally, they’re investing in improving the automation in inferring common inductive invariants to reduce manual overhead for performing correctness proofs.
While VeriSol is still a prototype primarily driven so far by smart contracts in Azure, the researchers have lofty goals for the verification tool and encourage open collaboration to help bring advances in formal verification to mainstream smart contract development.
“We envision empowering not just Azure Blockchain developers and customers, but contributing to a full blockchain ecosystem that is safer and helping people realize the full potential of the technology without being plagued by the costly mistakes in smart contracts,” says Lahiri.
Programming languages and software engineering