Microsoft Azure Launches Open Sourced Tool For Auditing Smart Contracts
A Smart Contract audit is fundamentally the same as a regular code audit – which is meticulously investigating code to find security flaws and vulnerabilities before the code is publicly deployed. It’s like testing a bridge before it’s opened to the public. In both cases, the builders have a responsibility for the security and safety of their products.
Azure is a cloud computing service created by Microsoft for building, testing, deploying, and managing applications and services through Microsoft-managed data centers. The blog that announced the product says:
“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 the 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.”
With VeriSol developers 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. But formal verification automatically identifies the different ways the code could potentially violate a given invariant, including those cases developers can’t predict.
Microsoft Principal Researcher Shuvendu Lahiri says:
“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.”