How Formal Verification Can Reduce Bugs & Vulnerabilities in Smart Contracts
What is formal verification?
While most of us are already taking technologies such as cryptocurrencies, the blockchain, virtual machines, and smart contracts for granted, there’s still a lot of hard work going into making them viable.
It sounds surprising, but fixing bugs and patching vulnerabilities is also a thing in the crypto space where everything is code. A general description of smart contracts is that they are means that help us exchange money, property, shares, or basically anything of value in a transparent and conflict-free way while avoiding intermediaries.
On a more technical level, a smart contract is a computer protocol intended to digitally facilitate, verify, or enforce the negotiation or performance of a contract. In the context of software systems, formal verification is the process through which the correctness of an intended algorithm is either proved or disproved. In short, it’s a method that checks a system that meets a specific set of properties.
It’s easy to see then why formal verification is a method very well-suited for ensuring that blockchains are bug-free and protected against vulnerabilities as much as possible. Because the transfers of value are almost self-executed across decentralized networks when it comes to cryptocurrencies, there’s a lot more value at stake than in traditional financial networks. Hence, the correctness and smooth functionality of smart contracts is a serious issue, especially for platforms such as Ethereum.
Is formal verification suitable for smart contracts?
Speaking of Ethereum, a recent study pointed out that somewhere around 34,000 Ethereum smart contracts were, in fact, vulnerable (out of nearly 1 million smart contracts). Another important issue that needs to be grasped when it comes to the importance of formal verification on smart contracts is related to the immutable nature of the blockchain. For instance, if a block is committed to the blockchain and there are vulnerabilities within it, it’s easy to see why these could be potentially damaging to the system.
To further understand why formal verification is important for smart contracts, it’s important to note that there are two main ways a developer doesn’t get what they initially wanted from a smart contract. Either the developer doesn’t understand the intent of the smart contract, or makes a mistake when implementing the said intent. For example, if formal verification would have been done right, there wouldn’t have been incidents such as the incident with the Parity wallet or with Ehtereum’s recursive send exploit in the DAO incident.
Use-cases of format verification on various crypto projects
The team behind Ethereum has been hard at work researching how to implement formal verification. However, the current Gas limits on the network make it very difficult for this implementation to be a successful one
Nowadays, Ethereum isn’t the only platform that integrates formal verification as a standard procedure. Considering all of Ethereum’s current problems as well as its history, formal verification of smart contracts would be one of the best additions to its development medium as a way to reduce the risk of vulnerabilities.
Cardano is one of the biggest names in the cryptosphere right now and one of the projects that use smart contracts. On Cardano formal verification is arguably easier than on Ethereum since it doesn’t use a bounded stack design like the latter, meaning that there is no stack arithmetic flow. Cardano’s Computation Layer (CCL) is comprised out of 2 layers: a formally specified virtual machine and language framework and formally specified languages that facilitate verification of smart contract code.
Zilliqa is a project that’s mostly focused on offering a highly-scalable and secure decentralized blockchain network for smart contracts and dApps. Just like in the case of Ethereum, contracts have to be compiled to bytecode before performing analysis and verification tasks, which means that Zilliqa would also benefit from this technology.
Tezos is a blockchain project that aims to provide “the world’s first “self-amending” cryptocurrency.” Tezos’ smart contract language is called Michelson, and it’s based on OCaml. This programming language was chosen for its functional programming, speed, and easy-to-understand syntax. It’s also good at implementing formal proofs. In order to facilitate formal verification on its smart contracts, Tezos makes use of a technology called Coq Proof Assistant.
Even though formal verification is not a new concept, especially in the hardware industry where it’s the norm, the technology is gaining more and more acceptance in the software field. However, because formal verification of smart contracts is a very complex process, it will most likely require a few years until most crypto platforms running smart contracts will find the means to efficiently benefit from everything it has to offer.