The same approach that helped ensure that the software aboard NASA’s rovers didn’t fail once they landed more than 30 million miles away on Mars could help ensure the security of cryptocurrency transactions.
Called “formal verification,” the approach uses a combination of mathematical proofs and logic to ensure that the contracts that govern blockchain transactions are less likely to suffer unforeseen failures or deliberate fraud.
It’s the same approach used by programmers to test the software running everything from industrial equipment to interplanetary probes, and there’s growing interest in using it to help protect cryptocurrency. Tezos, Cardano and Ethereum all are developing approaches that allow smart contracts to be more easily tested using formal verification techniques. The idea is to ensure that holders of these organizations’ cryptocurrencies can’t lose money from exploitable issues with the software that powers them.
The financial sector has used formal verification to develop algorithms, so the concept has precedent. Tezos, for example, is making formal verification a key selling point of its platform, arguing that its Michelson programming language is structured in ways that simplify the formal verification of smart contracts.
What Can Go Wrong
Most cryptocurrencies allow people to create programs or scripts to process transactions. In currencies like Ethereum’s, this has given rise to “smart contracts,” which are basically programs that live in the blockchain and govern how transactions are conducted.
At their heart, smart contracts are like software applications—and like software applications, they can be exploited, crash or just fail to work as expected under unique circumstances. The problem is complicated by the reality that smart contracts are often written in new programming languages. They also require programmers to think about incentives to defraud the system in ways they may not be familiar with.
Researchers at the University of Maryland, for example, found the potential for problems in even “very simple smart contracts,” such as an electronic version of the rock-paper-scissors game. Also, the nature of how smart contracts work makes it difficult to fix them once they’re put into action.
Nor is the issue theoretical. Ethereum, for example, has seen high-profile losses, including the 2016 exploitation of a smart contract for a fund called the DAO that led to at least $50 million in losses.
“If you load money into a buggy smart contract, you will likely lose it,” write the University of Maryland researchers.
What it Takes
The “formal” part of formal verification involves the development of mathematical models and proofs that reflect the software’s specifications and the way it works in practice. This can be time-consuming. For example, it took 20 person-years to write the proofs that formally solved a longstanding mathematical problem involving the stacking of spheres called the Kepler conjecture. But in theory, formal verification can ensure that software is as error-free as a mathematical proof.
Proof-testing programs such as Coq support formal verification methodologies, and new services using formal verification, including Imandra Contracts, are emerging to ensure smart contracts. Computer scientists also have envisioned outsourcing the process, although early sites such as Proofmarket and Mathgate, which allowed smart contract writers to offer bounties for proofs, have since shut down.
And as with everything, the differences between theoretical proofs and real-world conditions will force tradeoffs. “Adversaries can be arbitrarily intelligent and capable,” Cardano’s developers write. “To say they are defeated solely through a mathematical model is extraordinary. And, of course, it is not entirely true. Reality introduces factors and circumstances that prevent the utopia of pure security and correct behavior from existing. Implementations can be wrong. Hardware can introduce attack vectors previously unconsidered. The security model might be insufficient and not conform to real life use. A judgement call is needed about how much specification, rigor and checking is demanded for a protocol.”