The Azure Blockchain Platform is taking smart contract verification seriously! Microsoft Research has recently come up with VeriSol, a smart contract verification tool and the Azure Blockchain Platform has adopted this.
Blockchain promises much, however, it’s a new and evolving technology. There are challenges that require solutions, e.g., smart contracts bugs that are causing financial losses.
Experts forecast that the blockchain technology market will grow up to $23.3 billion by 2023, and smart contracts will likely play a key role in this growth. Smart contracts are open-source pieces of code that automatically transfer cryptographic assets based on predefined conditions.
These are tamper-proof since one can’t modify them after deployment. The execution results of smart contracts are irreversible. Smart contracts promise transparency and efficient contract administration, as a result of these characteristics.
Immutability of smart contracts and their irreversible execution pose challenges though since recovering from smart contract bugs becomes harder! The Ethereum DAO hack was an example, and the Parity wallet breach was another.
Some estimates state that 25% of all smart contracts have critical bugs. The open-source nature of smart contracts allows malicious players to study these bugs and exploit them.
Software often has bugs, and there are ways to find them, e.g., testing, verification, etc. Best software development project teams try to use both testing and verification to identify bugs, however, smart contract verification isn’t easy! That’s where VeriSol assumes importance.
VeriSol: Making smart contract verification a reality
Software verification requires practitioners to have deep knowledge of the programming language, system environment, etc. Most blockchain developers code smart contracts using Solidity, a proprietary language from Ethereum.
It’s a niche skill, therefore, it’s hard to find suitable experts for smart contract verification. There are companies offering smart contract auditing services, however, these services are labour-intensive and costly. Finally, these services aren’t scalable enough.
VeriSol, which stands for “Verifier for Solidity”, is a solution from the Microsoft Research. This solution translates smart contracts written in Solidity to Boogie formal intermediate verification language.
Smart contract developers can then specify the exact behaviour their code should demonstrate, given certain conditions. VeriSol then mathematically verifies whether the smart contract actually meets these specifications.
Smart contracts often have relatively smaller code bases, and the team behind VeriSol has utilized this for the scalability of their solution. Blockchain developers still needed an easy way to access this, though.
The Azure Blockchain Platform is increasingly a prominent “Blockchain as a Service” (BaaS) platform, and now it includes VeriSol in its “Continuous Integration”(CI) / “Continuous Delivery” (CD) environment. Developers will now find it easier to use VeriSol.
Technology giants committing to blockchain
The ease of smart contract verification is a key requirement for blockchain adoption, therefore, this latest move from Microsoft augurs well. This, and other recent moves from technology giants, e.g., Salesforce unveiling their BaaS platform, signal their commitment to the promising technology, and that can only be good news!.
