How Formal Verification Can Reduce Bugs & Vulnerabilities in Smart Contracts

The formal verification of smart contracts is an emerging trend in the cryptocurrency space focused on reducing the instances of bugs and vulnerabilities of smart contracts that have led to numerous high-profile hacks and endemic security concerns.

Formal verification has a wide variety of applications in regards to hardware and software systems. It has become exceedingly important as the complexity of systems increases, particularly with hardware. In blockchain networks, the litany of smart contract vulnerabilities and exploits have led to a need for improved smart contract programming and auditing.

Background on Formal Verification

Formal verification uses formal methods to check whether or not a design of a hardware or software system meets a specific set of properties. Formal methods are a particular type of mathematical technique for the specification, development, and verification of both hardware and software systems. Using formal methods to prove or disprove the correctness of intended algorithms is known as formal verification.

Martin Davis is credited with developing the first computer-generated mathematical proof back in 1954. The concept started gaining traction in the 1960s for verifying the correctness of computer programs in early languages such as Pascal and Java. Following some high-profile computer bugs, such as the Pentium FDIV Bug in 1994, the sentiment that formal verification needed to be ubiquitous started snowballing.

Testing a software or hardware system can be broken down into two general phases:

1. Validation
2. Verification

Validation is determining whether the product meets the user’s needs.

Verification is testing whether or not the product conforms to the specifications.

Verification consists of producing an abstract mathematical model that correlates to the design specifications of the product (i.e., algorithm, hardware chip) while the formal methods used to generate the model mainly stem from theoretical computer science fundamentals.

The use of formal verification has become extremely important in hardware systems, where it is used by almost every major hardware manufacturer to ensure the robustness of their products. However, its use is not nearly as prevalent in software as it is in hardware, which is mainly attributed to the commercial nature of hardware manufacturing.

However, that dynamic is beginning to change with the advent of blockchains and cryptocurrencies where considerable transfers of value are autonomously executed across a decentralized network. With more value at stake than traditional systems, the correctness of smart contracts has become a pressing concern.

A brief history of smart contract exploits is all it takes to understand the consequences of simple vulnerabilities in contract code.

Why Use It For Smart Contracts?

According to a recent study performed on nearly 1 million Ethereum smart contracts, 34,200 of them were flagged as vulnerable, in 10 seconds per contract. That staggering number was reached by analyzing trace vulnerabilities of smart contracts including:

• Finding contracts that lock funds indefinitely
• Contracts that leak funds carelessly to arbitrary users
• Contracts that can be killed by anyone

Along with the general logical complexity and novelty associated with programming smart contracts for blockchains, their immutable nature — once they’re committed to the blockchain — makes vulnerabilities potentially much more damaging.

Brian Marick and Daejun Park provide an excellent analysis of smart contract vulnerabilities and how formal verification can help mitigate their instances. Essentially, there are typically two ways that a developer can fail to get what they want from a smart contract.

1. Misunderstood intent
2. Making a mistake when implementing that intent

Many of these standard errors can lead to enormous sums of locked up funds like with the Parity wallet or with Ethereum’s recursive send exploit in the DAO incident. Formal verification is used as a way of mathematically confirming that specific vulnerabilities will not lead to damaging exploit vectors.

A formal specification is used as the precise output or result that a smart contract is looking for, which a computer can check. Verification subsequently takes place once the contract compiles to the bytecode and the formal verification proves that the compiled bytecode implements the specification. However, manually performing formal verifications is an arduous process and sometimes comes with its own mistakes. Even verifying formal proof results can come with its nuances.

Tools like the Coq Proof Assistant have been developed to help facilitate the mechanized proofs about the properties of programs and is currently used by several emerging cryptocurrencies with the languages they use embedded into Coq.

While smart contract auditing provides a much-needed layer of assurance through code reviews, formal verification of smart contracts can help to reduce instances of vulnerabilities through mathematical analysis further. With smart contracts becoming more prevalent, it seems natural that the application of formal verification will become more widespread in the industry.

Current Applications of Formal Verification

Several platforms are either integrating formal verification already or plan on doing so soon. Evaluating the safety and security of smart contracts that operate within these platforms will be vital to gauging their effectiveness in stemming critical vulnerabilities.

Zilliqa

Zilliqa is a high-throughput blockchain designed to host scalable and secure decentralized applications (dapps). Several of the technical developers behind Zilliqa were authors of the earlier study that uncovered the thousands of smart contract weaknesses.

Zilliqa uses a new programming language called Scilla, designed by members of the Zilliqa team and some other affiliates. Scilla is an intermediate-level language that is embedded in the Coq Proof Assistant. It is intended to be a translation target for higher-level languages for performing analysis and verification before contracts are compiled to bytecode.

Tezos

Tezos is written in OCaml and its smart contract language is Michelson, based on OCaml. OCaml was selected because of its functional programming offerings of speed, unambiguous syntax and semantics, and capabilities for implementing formal proofs. Tezos also uses the Coq Proof Assistant for facilitating formal verification of smart contracts.

Arthur Breitman — the Tezos co-founder — posted details regarding the verification of some Michelson contracts in Coq, including a multi-sig contract on their testnet last year. Tezos recently launched, so its application of formal verification should provide an excellent gauge for the state of improved security of smart contracts using the method. Whether or not exploits that have plagued Solidity contracts will play out in Tezos will take some time to unfold but evaluating how secure smart contracts become on Tezos could be very indicative of a continuing trend.

Cardano

Cardano is written in Haskell and its smart contract language is Plutus, which is based on Haskell.

Cardano is designed with a Cardano Computation Layer (CCL) that consists of 2 layers:

1. A formally specified virtual machine and language framework
2. Formally specified languages that facilitate verification of smart contract code

The goal is to create an environment that streamlines the process of guaranteeing that a contract functions as designed without catastrophic vulnerabilities. Notably, Cardano does not use a bounded stack design like Ethereum’s EVM, so not worrying about stack arithmetic flow allows it to formally verify smart contracts much easier.

Ethereum

Ethereum has been researching the incorporation of formal verification for quite some time, with several projects investigating its potential. One such publication, “Making Smart Contracts Smarter,” focuses on smart contract bugs and suggests ways to mitigate them, including improving the operational semantics of Ethereum to foster formal verification.

Gas limits in Ethereum make it challenging to implement formal verification. Further, the only way to know the meaning of a Solidity program is to compile it into bytecode. The compiler changes rapidly, so verification tools would need to adjust to the rate of change as well. Considering Ethereum’s established network and history, formal verification of smart contracts in Ethereum would ostensibly provide the best gauge for their effectiveness in mitigating vulnerabilities were formal verification to become widely used in the network.

Conclusion

Formal verification is a highly complex and arduous task. Despite this, it has become a universal standard in the hardware industry and is likely to continue gaining momentum in the software space. Blockchains and cryptocurrency networks — where high-value transfers are common — will assuredly accelerate this effect. Measuring the positive impact of formal verification of smart contracts will likely take several years to unfold as we are only seeing the beginnings of what should become a much broader trend in the industry.

5,182