Asia's Source for Enterprise Network Knowledge

Monday, May 27th, 2019

Security

The Importance of Formal Verification in Smart Contracts

Sun Life of Canada, Philippines’ Voyager to co-develop fintech services for insurance industry

Smart contract exploits have become an endemic problem in the cryptocurrency space that has led to enormous sums lost through hacking and accidental errors. According to CipherTrace’s Q3 AML report, more than $927 million has been stolen in cryptocurrencies in 2018 through the third quarter—a substantial amount of which came from smart contract vulnerabilities—and that number is expected to surpass $1 billion by the end of the year.

Cryptocurrency hacks are commonly performed by exploiting an error in critical functions of smart contracts that can lead to indefinitely locked funds, leaked funds, backdoor transfer/minting functions, and the ability to arbitrarily kill a contract. The problem is so widespread in Solidity smart contracts on Ethereum that a recent report utilizing MAIAN—a symbolic analysis tool—was able to identify more than 34,000 trace vulnerabilities in smart contracts out of nearly 1 million analyzed.

With so much value immutably committed to blockchains via smart contracts that are unable to be updated, it has become pertinent to develop innovative solutions for reducing instances of smart contract vulnerabilities. Promising developments include stripped-down smart contract languages—such as Vyper for Ethereum—that reduce logical ambiguity and remove features such as modifiers and recursive calling that can lead to critical exploits. Other solutions focus on early warning systems via an on-chain Oracle mechanism—such as MonitorChain—which identifies and produces alerts for triggers in critical contract functions such as mint and transfer that are commonly used to steal and transfer funds from exchanges.

One of the more powerful answers to mitigating smart contract vulnerabilities is the proliferation of an extensively studied mathematical tool derived from formal methods known as formal verification.

Leveraging Formal Verification for Enhanced Smart Contract Security

Formal verification is the use of formal methods to articulate a formal specification of a program or a system. Formal verification provides a proof of correctness and safety using an abstract mathematical model that validates whether a system or a program satisfies specific desired properties or faithfully implements the agreed-upon specification.

The concept has been around since the 1950s and is ubiquitous among hardware manufacturing where the commercial viability of products heavily relies on their correctness. In software, the commonality of formal verification lags behind hardware but has started gaining traction within the cryptocurrency realm due to the immutability of  blockchains.

Solidity—the primary smart contract language for Ethereum—is excellent for analyzing the value of formal verification in smart contracts while also providing some practical examples of instances where the technique could have prevented disaster. Formal verification cannot explicitly guarantee that a smart contract will not contain bugs, but it can mathematically prove that a contract will not violate specific properties. When applied to critical functions within a smart contract, formal proofs can help alleviate concerns of exploits that can lead to disastrous value loss.

Many smart contract exploits are based on peculiar errors in the virtual machine (i.e., EVM) such as gas calculations. Formal verification of a specification can be achieved using an automated theorem prover such as Coq that uses semantics to prove a specific compiled contract (into EVM bytecode) implements the required specification. However, determining the formal specification of a contract in Solidity is a very manual process that requires profound expertise and can even contain errors itself. Despite this, the small size of smart contracts makes formal verification practical to use today for blockchains.

Formal verification enables a user to identify bugs that smart contract audits and testing regularly miss such as frozen funds or unexpected changes to critical state variables. Reentrancy vulnerabilities such as errors in recursive sending can also be mitigated by implementing a tail-call programming style, which can facilitate formal verification by removing much of the complexities of arbitrary state changes involved with external calls.

Proving a contract’s safety and correctness with formal verification is an iterative process that adds a layer of verification to comparing the contract’s bytecode to its specification for the virtual machine. Several high-profile smart contract exploits may have been mitigated by using formal verification, including the DAO exploit and the BatchOverFlow exploit.

The infamous DAO incident was caused by a multi-stage exploit of the recursive send pattern within the splitDAO function. The hack led to roughly $60 million in stolen funds and the eventual hard fork of Ethereum into Ethereum and Ethereum Classic, demonstrating how substantial the consequences of smart contract vulnerabilities can be. The DAO exploit is classified as a reentrancy vulnerability that could have been identified with the help of formal verification tools.

The BatchOverFlow exploit was a critical vulnerability within the mint function of several ERC-20 token contracts that led to trillions of counterfeit tokens being minted and subsequently dumped on exchanges. Millions of dollars were lost, and the impact was severe on token holders  and exchanges. Formal verification of the token contracts that were exploited in the hack would have identified the vulnerabilities in the critical mint functions of the contracts when compiled to bytecode.

Other potential vulnerabilities where formal verification can provide effective correctness guarantees are with contract killing, which is what happened with the infamous Parity wallet incident that led to $150 million in frozen funds.

Formal verification is an intriguing concept that can add vital security depth to smart contracts running on blockchains. Complementary tools such as automated theorem provers and intermediary-level languages tailored explicitly towards improving formal verification are poised to become standard security features in the future proliferation of smart contracts.

Dr. Amrit Kumar is the Head of Research at Zilliqa.