Microsoft conveyed in its research blog dated 03 June about strengthening formal verification to secure Azure blockchain smart contracts.
Microsoft threw light on the potential of blockchain technologies having great applicability in financial services, supply chain, and governance. The software giant quoted the technology as being almost disruptive while promising much business value in the years ahead. Microsoft touched upon the key feature of blockchain that renders much of its versatility – smart contracts. Being programmable, smart contracts are intuitive but plagued by inherent problems.
Microsoft sustained by adding about a few high-profile compromises in public blockchains like the DAO exploit and the Parity wallet bug. These incidents resulted in the loss of millions of dollars worth of cryptocurrency. Microsoft expressed that in a bid to fortify smart contract auditing tools for Ethereum, the Azure Blockchain team has partnered with Microsoft Research. The collaboration has resulted in a new verification tool being developed by the researchers.
Microsoft further added that with the tool christened VeriSol (Verifier for Solidity), developers could begin to express the required behaviors of smart contracts. Post this they can use mathematical logic to rigorously check those specifications against the implementation. Microsoft clarified that this logic has been included in the continuous integration pipeline.
Cody Born, Senior Software Engineer on the Azure Blockchain team echoed insight as –
“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.”
Microsoft touched upon few logistics of the tool by informing that VeriSol operates by encoding the semantics of Solidity programs into the intermediate verification language Boogie. In the process, VeriSol leverages and extends the Boogie verification toolchain. It supports high-coverage testing as well as performing correctness proofs automatically or with some user intervention.
In May, there were reports about Starbucks resorting to technology to better connect with its customers. By joining forces with Microsoft, Starbucks is on an endeavor to scale customer experience. Starbucks uses a technology called ‘reinforcement learning’ to make better decisions for a personalized experience.
Microsoft concluded by emphasizing that the VeriSol team is not only working on supporting a large subset of Solidity but also developing a library to allow users to write intuitive code. The software major indicated the importance of automation to infer common problems to reduce manual overhead for performing correctness proofs. Microsoft expressed the goals of researchers to bring formal verification to mainstream smart contract development.