3 posts on writing safe smart contracts: Design, Verification, Synthesis
Smart contracts are permanent, perpetually running applications on the blockchain. At Synthetic Minds, we are obsessed with ensuring that smart contracts function correctly.
Synthetic Minds’ Solidity Verifier and Synthesizer generates attackers for white-hat analysis of Solidity smart contracts. Usability has been a first-class goal for this verifier: it performs verification across multiple transactions and requires no program annotations, extracting its specifications from the ubiquitous unit tests. We will disclose our new results on Solidity in October. For now, we are happy to say that our Solidity verifier has matured to analyze some of the most complicated projects, including Augur.
Our September series of posts will discuss the Synthetic Minds Move Verifier and Synthesizer. We will report on lessons made possible by the retargetability of our technology. Both the verifier and the synthesizer are blockchain and language agnostic, and we were able to expand support for a new blockchain and language in a short span of time. In fact, it took us just six weeks to support the Move language released in June as part of the Facebook’s Libra blockchain. Our support for Move includes a verifier, a synthesizer, some standard libraries, as well as sample applications. Our next series of posts will describe what we learned in this exercise about the Move language and about using verification and synthesis for smart contracts.
If you are writing Solidity or Move smart contracts, please contact firstname.lastname@example.org. We’d be happy to verify your contracts using our analysis framework.
A few highlights from those posts may whet your appetite:
Driven by curiosity of how the Move semantics affected the architecture of common classes of contracts, we developed a time service, a name server, a multi-signature wallet. All these contracts are being released as well.
As a common running example for this series of posts, we developed a minimalistic contract that embodies the key aspects of typical auction and escrow contracts. This model contract arbitrates a distributed Rock-Paper-Scissors game between two players. The players are surrounded by attackers and they themselves attempt to cheat by exploiting the weaknesses in the contract and the blockchain platform. Later in this post, when we describe the design process for smart contract protocols, we’ll explain how these weaknesses impact how we build them.
Move’s linear type system provides strong compile-time guarantees, including the inability to duplicate unique resources, such as the LibraCoins. Since no type system can prevent all programmer errors, verifiers remain indispensable. Our next post reports how our Move verifier caught errors that escaped the Move type system, such as depositing the coin into a wrong account or frontrunning attacks.
Finally, in a subsequent post on automatically synthesizing contracts, we show that smart contracts can be automatically synthesized from just a few tests. A test-driven synthesis is practically important because the typical prerequisite to synthesis is a specification of the desired contract behavior. Specifications can be laborious to write, in part because they are formal, stating the behavior with pre- and postconditions. In contrast, a unit test promises to be an accessible specification format.
Designing Smart Contract Protocols
As an introduction to verification and synthesis of contracts, we first look at how to design smart contracts that are resilient to attacks. Specifically, we focus on how the possible attacks influence the design of the protocol exposed by the contract.
A contract is a program that facilitates interaction among untrusted parties. We can think of the contract as an object that receives calls from other objects. Trust in the contract is improved by logging its execution into the publicly visible blockchain and by opening its code. The two measures are insufficient, of course, because logging will not prevent an attack, only record it, and manual audits of source code have inherent limitations. Mechanized tools have the potential to explore all possible attacks before a contract is deployed, but preventing a discovered vulnerability may require a redesign of the contract.
This post shows several redesigns of a contract, improving its resistance to attacks. Our running example is the game Rock Paper Scissors (RPS). To motivate the attacks, Alice and Bob will play RPS for money. This simple distributed game is prone to many forms of attacks observed in real-world contracts. For example, Alice and Bob will exploit tactics to observe each other’s bets, and third parties will try to steal money deposited with their bets.
We start with a contract that is rather secure but lacks excitement of playing RPS in person. Next, we will make it more fun but in doing so, we will expose vulnerabilities, which we will gradually repair by redesigning the contract. Together, we will examine three attacks and one behavioral corner case.
The auto-man contract. If Alice and Bob are happy with the contract betting on their behalf, we can use a simple contract where players deposit funds and the rest is automated. The protocol is that Alice initiates a bet, sending funds to the contract. Bob next matches the bet by also sending funds.Then the RPS contract draws random hands on behalf of Alice and Bob, respectively, automatically finalizing the game. After the winner is determined, the contract deposits the winnings. This contract is difficult to attack thanks to its limited attack surface. In particular, the contract API exposes no methods for cashing out the winnings, whose bugs could be exploitable.
Fig: The Auto-man contract bets on behalf of players. Its simple API makes it difficult to attack. Note: following the notation of interface automata, we append “?” to names of actions that are inputs (i.e., calls to RPS) and “!” to actions that are outputs (i.e., calls to other accounts).
The strawman contract. Since generating random numbers on the blockchain is non-trivial, our next contract asks the player to select the hand as part of the bet. Additionally, players collect the winnings by calling the contract. This contract offers more excitement for players and also models real contracts where the participating parties perform multiple interactions with the contract.
Fig: The Strawman contract. The players enter their bets (chosen hand + funds) and later collect their winnings. The players coordinate off-chain, bypassing the contract.
// expected Alice-Bob game on-chain trace Alice: rps.player1_bet(n, handA) Bob: rps.player2_bet(m, handB) Alice: rps.cash_out()
Fig: The trace of an Alice-Bob game. This trace shows the expected on-chain calls involved in a game between Alice-Bob when both players follow protocol. It is also valid to have Bob call cash_out() instead of (or in addition to) Alice. However, the first call to cash_out with distribute all of the money so any subsequent calls will not change the state.
Attack 1: Attack by a third party. This contract offers an API that is sufficient to implement betting between two players. However, as soon as a third party is introduced, they can disrupt the game between two such players, Alice and Bob, by ensuring a denial of service of the challenging player. For example, a third player Mallory could superceed the Alice-Bob game with their own Mallory-Bob game, cutting Alice out of the game without either player realizing until cashout:
// Mallory disrupts the Alice-Bob game Alice: rps.player1_bet(n, handA)// Mallory blocks the Alice-Bob game with Mallory-Bob game Mallory: rps.player1_bet(p, handC)Bob: rps.player2_bet(m, handB)// Mallory cashes out on Bob's unintended game with Mallory Mallory: rps.cash_out()// There is no game for Alice to cash out on Alice: rps.cash_out()
Fig: The trace of Mallory’s disruption of the Alice-Bob game. The attack succeeds if the RPS contract insufficiently keeps track of the game state, specifically who exactly is involved in each game. Because Bob does not directly indicate his opponent, Mallory is able to have her game block that of Alice without Alice or Bob's knowledge until cash_out.
With this protocol, Bob is not automatically informed of a challenge, so Mallory can fail to inform Bob of her new challenge. This would result in Bob and Alice believing Bob is playing with Alice when in reality he is playing Mallory. This exploit does not guarantee Mallory a win, but is a clear exploit of the contract as Mallory can deny Alice from starting any games by blocking them with her own. To address this issue, both players need to indicate their opponent in their bets and at every stage the players' opponents need to be checked to ensure that the players are involved in the same game.
Attack 2: Bob reads Alice’s hand. Another class of attacks are strategies employed by non-cooperating players. For example, the strawman contract allows Bob to read Alice’s hand by locating her call to makeBet(bet,hand) in the (publicly readable) blockchain that records the contract. The access to her bet conveniently gives the malicious Bob a perfect winning strategy.
// malicious Bob reads Alice’s hand Alice: rps.player1_bet(n, handA)Bob: reads the chain to obtain handA Bob: determines the winning handB from handABob: rps.player2_bet(m, handB) Bob: rps.cash_out() // Bob (always) wins
Fig: The trace of Bob’s attack on Alice. The attack succeeds because Alice submits her hand in plaintext, allowing Bob to read the hand in the blockchain before responding to her challenge.
The Woodenman contract. Both attacks can be thwarted by changing the contract protocol. To account for other players, the initial bets must include the intended opponent. In implementation, cashing out will also include a check that the sender's opponent has the sender as their opponent. Preventing Bob always playing a winning hand requires another change to the contract protocol: Alice will encrypt her initial hand, revealing her hand only after Bob responds to her bet. The updated protocol is shown below. It includes a new API call, reveal, which Alice uses to send the encryption key, which allows the contract to confirm that Alice did not change her hand since the initial challenge.
Fig: The Woodenman protocol. Initial bets include a pointer to the intended opponent and Alice’s hand is encrypted and revealed only after Bob responds with his bet.
Attack 3: Alice abandons lost games. Alice is not immune to being a bad player either, and the current protocol unfortunately allows her to strategize. After she reads Bob’s bet which includes his plaintext hand, she can choose to abandon the game by not revealing her bet. Without the decryption key, it is impossible for the contract to determine the winner, which was presumably Bob.
Attack 4: Bob forces Alice to reveal before responding. In the Strawman and Woodenman protocols, Alice and Bob synchronize off-chain. For example, Bob sends the message done1 after he submitted his bet. A malicious Bob is free to send the message before he actually responds, making Alice to reveal her bet. If he can read her revealed hand by means of a frontrunning attack, he can submit a winning bet. If his bet is accepted by the blockchain before ALice’s reveal, he is guaranteed to win.
The Ironman contract. Attack 3 (Alice’s failure to call reveal) can be addressed by a timeout: if the reveal call does not arrive within a specified time, the game declares Alice the loser regardless of her hand. (Since smart contract environments do not include a timeout service, the RPS contract will need to ask an external account to send the timeout event to the RPS contract.) The timeout could perhaps be eliminated by Bob encrypting his hand as well, after which both Alice and Bob would provide their keys to the contract. They would however need to transfer the keys simultaneously, so that neither can see the other’s key.
Attack 4 can be thwarted by making the Bob-responded notification trusted, by making it come from the contract. This notification is typically implemented by emitting an event.
Fig: The Ironman protocol. Bob’s response and Alice’s reveal can both time out. If Alice does not reveal before the timeout, Bob is declared the winner by non-show. If Bob fails to respond, Alice collects her bet. To synchronize the players, the contract emits three events: response received, no response, and outcome. The challenge synchronization still happens off-chain. Note that it is sufficient that one of the players calls collect because the funds can be disbursed to either player in this call; the logic for this is not shown in the state machines.
Additional considerations. If both players abandon the game (in particular, they do not collect their winnings), what should happen to the bet(s) deposited with the contract? This is arguably not an attack but a neglected corner case of contract behavior. If we desire to return the funds, a solution is another timeout call to the contract, during which the contract to return the funds to the players’ accounts.
Discussion. RPS is a model contract. While Rock Paper Scissors is just a game, the RPS contract is a decent model of real contracts, in particular escrows and auctions. In escrows, two parties participate in a commit-finalize phased protocol, with a trusted party holding the funds until they can be released. In auctions, multiple people take turns betting, as in RPS. Furthermore, closed actions need to ensure that bets are not publicly visible, as in RPS.
Summary. We showed that to obtain an attack-resilient contract, it is necessary not only to ensure that the contract methods are implemented correctly but also to design a suitable contract protocol, which is the set of contract methods and events and the order in which they are to be called. We believe that the future of smart contract programming is in intelligent tools that will help programmers design such protocols.