Loading...

Verifying Smart Contracts in the Move language

At Synthetic Minds we build technology to accelerate the development of provably correct smart contracts. Our technology is rapidly retargetable across languages, and so when Facebook Libra released its Move language, we didn’t just start playing with the language — we retargeted our verifier to Move and then wrote Move contracts and libraries, observing how Move’s linear type system and our verifier stacked up in ensuring correctness of Move code.

This post reports on our experience with Move and on the tooling needed to find what we believe are common bugs. We describe about six weeks of work: one week to port the verifier and five weeks building the Move contracts, which include a Time Service, Name Server, MultiSig wallet, and a toy example that forms the basis of Escrow and Auction.

You can find all the code we built over the Move infrastructure in Synthetic Minds' fork of libra/libra.

The Synthetic Minds Move Verifier and Synthesizer is now operational and allows us to validate the correctness of Move modules simply by taking specs from test scenarios, which should make verification as accessible as testing. Additional specifications can be added in the form of assertions.

Background on the Move language

Move differs substantially from Solidity, which forced us to rethink contract architectures as we developed new Move modules. A “Module” is the equivalent of a contract in Solidity. Besides encapsulating code, it instantiates “Resources”, which other modules can store and pass around but cannot open. Move’s linear type system ensures that resource objects cannot be opened, modified, copied or destroyed, except by the module that defined it.

We found the resource semantics to have three interesting consequences. First, since resource duplication is disallowed, resources act as non-fungible tokens (NFTs). Second, resources can wrap other resources, including the Libra coin. Since only the resource creator can open the resource, wrapping Alice’s coin in Bob’s resource will put the coin in escrow which only Bob can open. The third consequence comes from the restriction that each account can store only one instance of any type of resource. For example, you own only one LibraCoin. So what do you do when you receive another coin? The answer is the join operation, which merges the coin you own with the one you received and returns a new coin with the sum of the values. This join operation can only be done by the LibraCoin module, which can also split a coin, effectively withdrawing the newly created coin from your account.

The Rock-Paper-Scissors contract

Of the modules we built, the RPS contract that arbitrates the Rock-Paper-Scissors game between two players described in the previous post was especially illustrative of the issues present in typical auction and escrow contracts. We also saw how building such a protocol is non-trivial, and hence verification is invaluable. We will use RPS as a running example. Our implementation is on rock_paper_scissors.mvir

When Alice and Bob want to play the game, they communicate with the RPS contract using this four-step protocol:

  1. Alice: Creates a “challenge” for Bob with an encrypted handA and a LibraCoin betA.
  2. Bob: Creates a “response” to Alice’s challenge with an unencrypted “handB” and betB.
  3. Alice: Processes a “reveal” of handA and secret nonce, which validates that she did not change her hand since Step 1.
  4. Bob or Alice: Process a “cash out” that will deposit the appropriate pool to the winner’s account.

Specifying correctness using tests scenarios

For each module we wrote a set of “test scenarios.” Our verifier is end-to-end and uses just these test scenarios as the correctness conditions to perform verification. We have a special way of writing tests that involves a “Sym” module to get values for the tests. When doing verification this Sym module returns symbolic values and we are able to state properties that span a large space of concrete values. When doing a run on the test-net, this module returns concrete values allowing evaluation for specific concrete values.

For the RPS contract, we wrote three scenarios that collectively describe valid runs of the RPS protocol, thus specifying the desired behavior of the contract:

  1. Alice and Bob run the protocol to completion and whoever chose the winning hand gets the combined pool. If there is a tie, both get their deposit back. This scenario covers three tests (Alice wins; Bob wins; and the tie). -- see our transactions scripts for this test case here: tests/full_protocol/.
  2. Alice challenges, but Bob is unresponsive and so Alice gets to recover her bet -- see our transaction scripts for this test case here: tests/player1_unresponsive/.
  3. Alice challenges and Bob responds, but Alice fails to reveal and Bob wins by no-show -- see out transaction scripts for this test case here: tests/player1_abandon/.

Each scenario is a sequence of transactions created by the players, so we implemented the scenario as a sequence of transaction scripts -- they define the correctness conditions for the verifier. Transaction scripts in Move are one-off code fragments that correspond to a transaction: the scripts call existing modules on behalf of the sender. The transactions in the sequence can come from multiple accounts, and by reordering the scripts, we can create phases of contracts and arbitrary time interleavings between protocol steps.

Implementing the RPS contract in Move

The Move restriction that each account can hold at most one resource of a given type made us think of the architecture in a very specific way. In particular, auctions and escrows are multi-step protocols among multiple players. In Solidity, we would simply keep the “game state” for each set of interacting players “centrally” in the smart contract state. However, the current version of Move does not have collections, and the most obvious way we found to keep game state was to “distribute” it across the participating players. Additionally, we encoded the phases of the game as nominally different resources. This made us think of game states as physical resources, and pass them from one player to the other.

We model the protocol steps with three resources: “Challenge,” created by Alice during the challenge step; “Response,” created by Bob during the response step to wrap the Challenge resource; and “Outcome,” created by Alice during the reveal step. At the end of each step of the protocol, the resource is held by either Alice or Bob, depending on who executed the step.

We noticed an interesting design pattern that emerges when the language only allows the defining module to pack/unpack a resource. In the case of RPS, by wrapping a Challenge inside a Response, we get the following: 1) even though Bob might hold the Response, it cannot get to the Challenge inside it, eliminating any issues with Response being copied/duplicated other than through a deconstruction of the Challenge; 2) one cannot create a Response unless a Challenge already exists in Alice’s account, ensuring that protocol sequence is obeyed (Bob’s response will fail if issued before Alice challenges him).

The pack/unpack pattern becomes more interesting when we wrap a resource with an explicit value (e.g., LibraCoin) in a resource without explicit value (e.g., Response, Challenge, and Outcome). We used the ability to wrap a LibraCoin in an interesting way when designing the name server. When paying for a name, we had the name server module return a resource that wrapped the payment inside the name returned. This put the payment inside the thing being paid for -- making value assignment very explicit! Since nobody other than the name server can unwrap the resource, it meant that the coin was locked until the module was called. And we only had two operations: “extend lease”, and “abandon name” that unwrapped, meaning we were able to track payments in a decentralized manner.

While great as a pattern, we realized that wrapping a coin is a dangerous feature. For example, what if a module neglected to implement a function that unwraps the resource and releases the coin? Wrapped in the resource, the coin would be lost forever. Sometimes it may be non-obvious when such an unwrapping function is needed. For example, the RPS module provides functions that Alice and Bob can call when their opponent becomes non-responsive. These functions unwrap the Challenge and/or Response resources, returning the bets to players. We initially didn’t realize the need for these bailout functions.

This experience points out that while the type system successfully guards resources as they flow outside its defining module, it offers limited protection inside the defining module. This is because the module internals need the power to perform arbitrary manipulations and movement of its resources, and it would be too restrictive to put these operations under a type system control. Therefore, the implementation of a module is where verification can complement the type system.

The implementation

The set of public functions exposed by the module are directly in line with the protocol, the first four being the four steps of the protocol, while the last two are the bailout functions called when the other player is non-responsive:

public player1_bet(p2: address, bet: LibraCoin.T, salted_hand: bytearray)
public player2_bet(p1: address, bet: LibraCoin.T, hand: u64)
public reveal(p2: address, key: bytearray, p1_hand: u64)
public cash_out(p1: address, p2: address)

public player1_abandon_challenge()
public player2_other_player_nonresponsive()

The three resources that correspond to the three phases (challenge, response and outcome) are defined below.

To capture the protocol state explicitly, we decided to represent each phase with resources, which are respectively created by the first three functions described above:

resource Challenge {
    // address of other player
    player2: address,
    // the value of bet
    bet: LibraCoin.T,
    // choice between Rock(0), Paper(1), Scissor(2)
    hmac_hand: bytearray,
    // timestamp of challenge
    timestamp: u64
}


resource Response {
    // address of other player
    player1: address,
    // responding to which challenge
    challenge: Self.Challenge,
    // the value of the bet
    bet: LibraCoin.T,
    // choice between Rock(0), Paper(1), Scissor(2)
    hand: u64,
}


resource Outcome {
    // Player 1 info: address, plaintext hand and bet
    player1: address,
    player1_hand: u64,
    player1_bet: LibraCoin.T,

    // Player 2 info: address, plaintext hand and bet
    player2: address,
    player2_hand: u64,
    player2_bet: LibraCoin.T,
}

Benefits of the Move type-system

By wrapping the Challenge in the Response we get to use the language facilities to ensure that the protocols steps are sequentialized.

In Move, the only module that can modify a resource is the module that defined the resource. This compile time guarantee can enable faster verification through modularization, since it is often sufficient to only consider one module at a time, instead of a composition of multiple modules, reducing verification complexity. The compiler can also eliminate a class of bugs such as double spends: for example, in the code above, the Outcome resource wraps a LibraCoin which means double-cashout bugs are eliminated because cashout has to consume the coin to deposit the coin.

Verifying the RPS contract

Although the Move type system can eliminate some bugs, it can not eliminate all bugs. The type system can not ensure that a coin ends up with the correct recipient. An attacker can steal money through a buggy module by having the module deposit a coin under its control to the attacker. For example, in the initial version of the RPS module, the Outcome resource did not specify the `player1` and `player2` addresses and our `wins` function turned out to be incomplete. The implementation was validated by the typechecker. Our verifier found the following semantic issues:

  • Losing player or third-party attacker could steal payout:
    • A losing Alice could still win by calling `cash_out(Alice, Alice)`
    • A third party attacker could call `cash_out(Alice, Attacker)` after a game between Alice and Bob, but before either of them had cashed out; and the attacker would get their deposit back
  • Incomplete logic of winnings: Bob would always win in the case of a tie (due to incompleteness in our implementation of wins)
  • Front-running: A front-running attack was possible in which Alice could always win because Bob’s play would be visible on the network.

Our verifier integrates in a very natural way -- similar to how one would write tests for the module.

The process for verification starts by taking the correctness conditions defined by the (generalized) test-scenarios from the scenarios section above (code is available at /tests/). For the case of RPS, we have 3 test cases defining runs of the protocol between Alice and Bob. The system takes these runs, and creates additional scenarios by interleaving an attackers calls between them -- the attacker can be one of Alice or Bob as well. Additionally, in some scenarios we allow the attacker to have access to the parameters of the call coming immediately after (which models front-running msgs on the network that have not been fully committed to the blockchain yet.) With the starting test-scenarios, and these “perturbed” scenarios, we are able to run the verifier to identify semantic correctness issues in our implementation that would not be caught by the type-checker.

The verifier generates the following counterexample (i.e., attack demonstrations) for each of the above:

Alice_cash_out:
Alice: rps.challenge(Bob, n, E(handA)) Bob: rps.respond(Alice, m, handB) Alice: rps.reveal(handA) Alice: rps.collect(Alice, Alice)
Attacker_cash_out
Alice: rps.challenge(Bob, n, E(handA)) Bob: rps.respond(Alice, m, handB) Alice: rps.reveal(handA) Mallory: rps.collect(Alice, Mallory)
Bob_wins_on_tie:
Alice: rps.challenge(Bob, n, E(handAB)) Bob: rps.respond(Alice, m, handAB) Alice: rps.reveal(handAB) Alice/Bob: rps.collect(Alice, Bob) # note the tie in the hands played, Bob wins
Alice_front_runs_to_never_lose:
Alice: rps.challenge(Bob, n, E(handA)) Bob: (uncommitted) rps.respond(Alice, m, handB) // Alice is reading the network messages off-chain (assuming that can be done on the Libra network -- it might not be). Bob’s handB is sent unencrypted. If Alice is allowed unfettered abandons, she can compute whether she’ll win or not, and abandon before Bob’s transaction is processed. Alice: rps.abandon()

No false positives: For each of these, when the verifier creates a demonstration exploit, we postprocess that to generate a set of concrete transaction scripts (run-script). We execute this run-script on a local deployment of the Libra blockchain to ensure it is not a false positive and validating the outcome. You can find our scripts here: tests/_generated/

A “standard library” of modules for Move

Out of curiosity for exploring the language design and for checking safety the type-system provided versus that provided by a verifier to do, we build a set of sample programs. It turned out that sample modules were pretty illustrative, and so we are releasing all of them to the community. Code for these modules can be found at modules/ (Note: User-defined modules are going to be supported in Move very soon. They are not supported as of Aug 2019, and so we had to deploy all modules as part of the compiler standard library. Some of these modules are legitimate candidates as “standard library” components, while others are not. For the moment, we had no option but to put them all together.)

We have run our verifier to ensure some correctness properties of these modules:

  1. LibraCoin / LibraAccount: The LibraAccount module is a core module built by the Move team that defines per-address accounts. Accounts maintain a coin balance and supports depositing and withdrawing coins. The LibraAccount module builds on top of the LibraCoin module, which defines the LibraCoin resource and a few primitive operation to manipulate coins.

    Properties verified: We have run our verifier to check two correctness properties for these two modules. The first property has to do with the total coin balance in the system (Note: This is an inductive property, and we stated it outside of the test framework.) The second property is that only an owner can withdraw coin from an account. More precisely, we proved that an attacker can not destroy or create new coins in the system, and that an attacker can not withdraw coin from any account except their own.

  2. Name service: A name service allows referring to addresses or resources by human readable names (e.g. domain name system). The key functionality is the ability to lease names. Once the owner of a name is identified, binding them to destinations (e.g., addresses) and implementing a name resolver (given a name, return its binding) can be done in multiple ways. We have implemented three name services, each with a different mechanism to handle sales or resolution.

    1. Unlimited-buys: The Unlimited-buys name service does no checks, anyone that requests a domain gets it for the duration they paid for. When the Unlimited-buys name service sells a domain, it marks the sale with two time-stamps, inception time and expiration time. Resolution of a name is ordered by inception: the earliest sale matching the domain name that has not yet expired. See code here: lns_oprah.mvir
    2. Stake-Commit: The Unlimited-buys name service provides no guarantees to buyers that the name will be theirs when bought. In particular, aside from the fact that one might buy a name that is completely superseded by someone else’s inception-expiry; we also have the scenario where two buyers might put in a request at approximately the same time and the service will award both of them, causing one buyer to have spent coins with no effect. The Stake-Commit service is similar to Unlimited-buys, but it performs a two-phase sale. First the buyer gets a stake to a domain, they can then ensure that the stake they have is the earliest before they commit to it. See code here: lns_stake_final.mvir
    3. Exclusive-owners: Both Unlimited-buys and Stake-Commit allow multiple sales of the same domain name. This module records a fixed number of domains (currently 3; this is easily generalizable to arbitrarily large number of names if Move were to support collections). This allows the module to check if the name has already been sold, and if so reject a new sale. See code here: lns_domains_list.mvir

    Property verified: For these modules we have verified that an attacker can not steal or change a domain: if Alice has bought some domain D in the past and it has not expired yet, no sequence of calls can allow Malory to gain ownership of, or change D in any way.

  3. Time service: Currently, Move has no notion of time. Having access to a duration counter is important to implement timeout in RPS and expiration of domains in the domain services. We implemented a simple time service module that provides such a counter. The time service module maintains a counter that can only be incremented by a designated “maintainer” address. This internal time counter can be kept (approximately) in sync with world time (through messages being sent at real world intervals) or not. Modules that rely on this time service should function properly regardless.

    Property verified: We verify that time progresses monotonically and it can only be updated by the designated maintainer.

  4. MultiSig wallet: We implemented a “k of n” multisig wallet. There are no collections in Move currently, and hence our current implementation is for “k = 2” and “n = 3”, but it is trivially generalizable with collections.

    We encode a wallet as a Resource that identifies the “n” owners; and the current LibraCoin held within it. There is a notion of an “authorization”, which is a statement from one of the owners authorizing a certain amount of coin “c” to be transferred to destination address “d”. The owners can coordinate off-chain and create authorizations independently. If “k” authorizations exist for a particular destination then a “send” call will transfer the min of the authorized coins to destination “d”.

    Also, because of the no-collections restriction and that only one resource of a type can be at an address our current implementation will allow each address to only create one wallet. (An address can participate in as many other wallets as needed, as long as they are created by someone else.) Similarly, we store the authorization at the owner authorizing it, and so only one authorization can be outstanding at a time. This also implies we had to provide an “abandon authorization” function to prevent deadlocks.

    Properties verified: We verify that at least “k” authorizations are indeed needed to initiate sends, and that an attacker cannot intervene to disrupt the protocol; and that additionally they cannot withdraw or participate in sends from the multi-wallet unless they are one of the owners.

  5. Rock-paper-scissors game (as a precursor to Escrow and Auction): The RPS protocol and its properties has been used as a running example throughout this post.

Summary: Can we make it even simpler to get safer code?

This post showed the following:

  1. Move’s design and type-system lead to new thinking and provide some safety:
    1. Move’s one-resource-per-account forces extra decentralization of resources, and made us naturally encode protocol steps structurally.
    2. The type-system with linear types provides safety guarantees for resources *outside* of the module defining the resource.
  2. Synthetic Minds’ Move Verifier ensures safety properties that span protocol steps, multiple calls into the module, done by multiple interacting participants.
    1. Synthetic Minds’ Move Verifier takes its specifications from basic test-cases that we already wrote to sanity-check the implementation. We wrote test-cases as transaction scripts.
    2. There are NO false positives. When SM’s Move Verifier finds a property violating case, we instantiate it as a specific test-case and run it on the testnet to confirm that the violation indeed happens.

In the next post, we show how these test cases might be the basis of synthesizing the entire RPS module directly! I.e., Using verification we can match the test case (i.e., correctness spec) with the implementation. This lifts the limited concrete test to a symbolic space. Going beyond that, we do not even need the module implementation. Directly from the test case, we can synthesize an implementation that matches the protocol described in the tests.

Start using SM

Email request@synthetic-minds.com to get started.