PNNL

A new chapter, coauthored by PNNL cybersecurity researcher Glenn Fink, describes a method to identify vulnerabilities in blockchain smart contracts as they are developed.

Blockchain is a computer technology that creates an open, verifiable record of transactions that is essentially impossible to forge. It is best known as the backbone of cryptocurrency trading. However, plans are in the works to write smart contracts for buying things like cars, real estate, and stocks so that no human agents need to help with paperwork.

“If you write a program that allows no human to interfere, then that program must be flawless,” Fink says. “Smart contract language must be good from the first block.”

Blockchains are strings of data blocks, where each block contains one or more transactions. Each successive block is linked to the previous one by an irreversible cryptographic transformation called a hash that can be used to authenticate the entire blockchain from block to block.

Transactions could be as simple as records of ownership of money or goods, or they could be steps in a complex program that executes a legal contract with conditions and programming logic. These all-digital contracts do not require or permit human intervention to execute, and this is why they must be written perfectly. Otherwise, the cost to one or more parties could be devastating.

The most infamous smart contract bug enabled the hack of a decentralized autonomous organization (DAO) on the cryptocurrency Ethereum Classic. The DAO hacker exploited a bug in the smart contract language that slowly drained the organization of its reserve automatically and anonymously. The organization worked for more than a year to recover, fighting lawsuits where claimants sought refunds in real cash for lost Ether coin, before collapsing. The hacker was never identified.

Right now, examining smart contracts for bugs is done mostly with human effort. While humans can find many problems, Fink says, they aren’t good at identifying problems in temporal logic or all the different ways a program could possibly run depending on the order of events.

To identify these problems in a blockchain, Fink and his coauthor, Weifeng Xu, now at the University of Baltimore, used an open-source temporal logic analyzer called TLA+ to find vulnerabilities in blockchain smart contracts. The work is now a chapter in a book titled Financial Cryptography and Data Security, recently published by Springer.

In the article, Xu and Fink showed how TLA+ checkers could be written to find four different kinds of common temporal logic errors in smart contracts, one of which is similar to the flaw in the DAO. This work could help smart contract writers create more secure code and make third-party evaluation of the code more thorough.

“The more that people use blockchain for commerce, the more important it is that smart contracts work flawlessly,” Fink says. “They become like critical infrastructure—they must work all the time.”