2.5 Trust and Commitments

In the last section, we made it so that Alice and Bob can actually exchange currency when they play Rock, Paper, Scissors!. However, the version of the application we wrote has a fundamental flaw: Bob can win every game!

How is that possible? We showed executions of the game where Alice won, like the following

$ ./reach run

Alice played Rock

Bob accepts the wager of 5.

Bob played Scissors

Alice saw outcome Alice wins

Bob saw outcome Alice wins

Alice went from 10 to 14.9999.

Bob went from 10 to 4.9999.

The problem is that this version of the game only executed an honest version of Bob, that is, one that followed the Reach program exactly, including in his private local steps. It is possible for a deviant and dishonest version of a Bob backend to execute different code and always win by computing the appropriate guess based on what value Alice provided for handA.

If we change Bob’s code to the following:

..    // ...
27    Bob.only(() => {
28      interact.acceptWager(wager);
29      const handBob = (handAlice + 1) % 3;
30    });
31    Bob.publish(handBob)
32      .pay(wager);
..    // ...

then he will ignore the frontend and just compute the correct value.

If we run this version of the program, we will see output like this:

$ ./reach run

Alice played Scissors

Bob accepts the wager of 5.

Alice saw outcome Bob wins

Bob saw outcome Bob wins

Alice went from 10 to 4.9999.

Bob went from 10 to 14.9999.

In this version, unlike the honest version, Bob never consults the frontend and so it never prints out the message of what hand Bob played. No matter what Alice chooses, Bob will always win.

Is it just a fluke of the random number generator that we observed Bob always winning? How would we know? Reach comes with an automatic verification engine that we can use to mathematically prove that this version will always result in the outcome variable equalling 0, which means Bob wins. We can instruct Reach to prove this theorem by adding these lines after computing the outcome:

..    // ...
34    const outcome = (handAlice + (4 - handBob)) % 3;
35    require(handBob == (handAlice + 1) % 3);
36    assert(outcome == 0);
37    const            [forAlice, forBob] =
..    // ...

Before we had this line in the file, when we ran ./reach compile, it would print out the message:

..    // ...

 2    Verifying for generic connector

 3      Verifying when ALL participants are honest

 4      Verifying when NO participants are honest

 5      Verifying when ONLY "Alice" is honest

 6      Verifying when ONLY "Bob" is honest

 7    Checked 18 theorems; No failures!

But now, it prints out

..    // ...

 2    Verifying for generic connector

 3      Verifying when ALL participants are honest

 4      Verifying when NO participants are honest

 5      Verifying when ONLY "Alice" is honest

 6      Verifying when ONLY "Bob" is honest

 7    Checked 23 theorems; No failures!

Many programming languages include assertions like this, but Reach is one of a small category where the compiler doesn’t just insert a runtime check for the property, but actually conducts a mathematical proof at compile-time that the expression always evaluates to true.

In this case, we used Reach’s automatic verification engine to prove that an attack did what we expected it would. But, it is better to use verification to show that no flaw exists and no attack is possible.

Reach includes some such assertions automatically in every program. That’s why every version of Rock, Paper, Scissors! has said that a number of theorems were checked. We can see what these theorems do by deliberately inserting an error into the program.

Let’s change the computation of the payout and make it so that if Alice wins, then she only gets her wager back, not Bob’s.

..    // ...
34      const outcome = (handAlice + (4 - handBob)) % 3;
35      const            [forAlice, forBob] =
36        outcome == 2 ? [       1,      0] : // <- Oops. was: [2, 0]
37        outcome == 0 ? [       0,      2] :
38        /* tie      */ [       1,      1];
39      transfer(forAlice * wager).to(Alice);
40      transfer(forBob * wager).to(Bob);
41      commit();
..    // ...

When we run ./reach compile tut-5-attack/index-bad.rsh, it gives details about the error:

..    

 4    Verification failed:

 5      when ALL participants are honest

 6      of theorem: assert

 7      msg: "balance zero at application exit"

 8      at ./index-bad.rsh:compileDApp

 9    

10      // Violation Witness

11    

12      const v71 = "Alice".interact.wager;

13      //    ^ could = 1

14      //      from: ./index-bad.rsh:9:28:application

15      const v74 = "Alice".interact.getHand();

16      //    ^ could = 0

17      //      from: ./index-bad.rsh:21:50:application

18      const v84 = "Bob".interact.getHand();

19      //    ^ could = 2

20      //      from: ./index-bad.rsh:29:48:application

21    

22      // Theorem Formalization

23    

24      const v93 = (v74 + (4 - v84)) % 3;

25      //    ^ would be 2

26      const v100 = (v93 == 2) ? [1, 0 ] : (v93 == 0) ? [0, 2 ] : [1, 1 ];

27      //    ^ would be [1, 0 ]

28      const v114 = 0 == (((v71 + v71) - (v100[0] * v71)) - (v100[1] * v71));

29      //    ^ would be false

30      assert(v114);

31    

..    

There’s a lot of information in the compiler output that can help an experienced programmer track down the problem. But the most important parts are

These kinds of automatic verifications are helpful for Reach programmers, because they don’t need to remember to put them in their program, and they will still be protected from entire categories of errors.

However, now let’s add an assertion to the program that will ensure that every version of the program that allows Bob to know Alice’s hand before he chooses his own will be rejected.

We’ll go back to the version of tut-4/index.rsh from the last section, which has an honest version of Bob. (Click on the preceeding link if you need to see what it contained.)

We’ll add a single line to the program after Alice publishes, but before Bob takes a local step:

..    // ...
23    Alice.publish(wager, handAlice)
24      .pay(wager);
25    commit();
26    
27    unknowable(Bob, Alice(handAlice));
28    Bob.only(() => {
29      interact.acceptWager(wager);
30      const handBob = declassify(interact.getHand());
31    });
..    // ...

When we run ./reach run, it reports that this assertion is false:

..    

 2    Verification failed:

 3      of theorem unknowable("Bob", handAlice/77)

 4      at ./index-fails.rsh:27:13:application

 5    

 6      Bob knows of handAlice/77 because it is published.

..    

It is not enough to correct failures and attacks when you discover them. You must always add an assertion to your program that would fail to hold if the attack or failure were present. This ensures that all similar attacks are not present and that they will not accidentally be reintroduced.

Let’s use these insights into automatic verification and rewrite our Rock, Paper, Scissors! so that it is more trustworthy and secure.

Since we’ve been making lots of changes to the code, let’s start fresh with a new version and we’ll look at every single line again, to make sure that you aren’t missing anything.

First, we’ll define the rules of Rock, Paper, Scissors! a little bit more abstractly, so we can separate the logic of the game from the details of the application:

 1    'reach 0.1';
 2    
 3    const [ isHand, ROCK, PAPER, SCISSORS ] = makeEnum(3);
 4    const [ isOutcome, B_WINS, DRAW, A_WINS ] = makeEnum(3);
 5    
 6    const winner = (handA, handB) =>
 7      ((handA + (4 - handB)) % 3);
..    // ...

When we first wrote Rock, Paper, Scissors!, we asked you to trust that this formula for computing the winner is correct, but it is good to actually check. One way to check would be to implement a JavaScript frontend that didn’t interact with a real user, nor would it randomly generate values, but instead, it would return specific testing scenario values and check that the output is as expected. That’s a typical way to debug and is possible with Reach. However, Reach allows us to write such test cases directly into the Reach program as verification assertions.

..    // ...
 9    assert(winner(ROCK, PAPER) == B_WINS);
10    assert(winner(PAPER, ROCK) == A_WINS);
11    assert(winner(ROCK, ROCK) == DRAW);
..    // ...

But, Reach’s automatic verification allows us to express even more powerful statements about our program’s behavior. For example, we can state that no matter what values are provided for handA and handB, winner will always provide a valid outcome:

..    // ...
13    forall(UInt, handA =>
14      forall(UInt, handB =>
15        assert(isOutcome(winner(handA, handB)))));
..    // ...

And we can specify that whenever the same value is provided for both hands, no matter what it is, winner always returns DRAW:

..    // ...
17    forall(UInt, (hand) =>
18      assert(winner(hand, hand) == DRAW));
..    // ...

These examples both use forall, which allows Reach programmers to quantify over all possible values that might be provided to a part of their program. You might think that these theorems will take a very long time to prove, because they have to loop over all the billions and billions of possibilities (e.g., Ethereum uses 256-bits for its unsigned integers) for the bits of handA (twice!) and handB. In fact, on rudimentary laptops, it takes less than half a second. That’s because Reach uses an advanced symbolic execution engine to reason about this theorem abstractly without considering individual values.

Let’s continue the program by specifying the participant interact interfaces for Alice and Bob. These will be mostly the same as before, except that we will also expect that each frontend can provide access to random numbers. We’ll use these later on to protect Alice’s hand.

..    // ...
20    const Player = {
21      ...hasRandom, // <--- new!
22      getHand: Fun([], UInt),
23      seeOutcome: Fun([UInt], Null),
24    };
..    // ...

The only line that is different is line 21, which includes hasRandom, from the Reach standard library, in the interface. We’ll use this to generate a random number to protect Alice’s hand.

..    // ...
20    const Player = (Who) => ({
21      ...stdlib.hasRandom, // <--- new!
22      getHand: () => {
23        const hand = Math.floor(Math.random() * 3);
24        console.log(`${Who} played ${HAND[hand]}`);
25        return hand;
26      },
27      seeOutcome: (outcome) => {
28        console.log(`${Who} saw outcome ${OUTCOME[outcome]}`);
29      },
30    });
..    // ...

Similarly, we only need to modify one line of our JavaScript frontend. Line 21 allows each participant’s Reach code to generate random numbers as necessary.

These two changes might look identical, but they mean very different things. The first, line 21 in the Reach program, adds hasRandom to the interface that the backend expects the frontend to provide. The second, line 21 in the JavaScript, adds hasRandom to the implementation that the frontend provides to the backend.

We’re now at the crucial juncture where we will implement the actual application and ensure that Alice’s hand is protected until after Bob reveals his hand. The simplest thing would be to have Alice just publish the wager, but this, of course, would just leave Bob vulnerable. We need Alice to be able to publish her hand, but also keep it secret. This is a job for a cryptographic commitment scheme. Reach’s standard library comes with makeCommitment to make this easier for you.

..    // ...
37    Alice.only(() => {
38      const wager = declassify(interact.wager);
39      const _handAlice = interact.getHand();
40      const [_commitAlice, _saltAlice] = makeCommitment(interact, _handAlice);
41      const commitAlice = declassify(_commitAlice);
42    });
43    Alice.publish(wager, commitAlice)
44      .pay(wager);
45    commit();
..    // ...

At this point, we can state the knowledge assertion that Bob can’t know either the hand or the "salt" and continue with his part of the program.

It is important to include the salt in the commitment, so that multiple commitments to the same value are not identical. Similarly, it is important not to share the salt until later, because if an attacker knows the set of possible values, they can enumerate them and compare with the result of the commitment and learn the value. That’s why we use a randomly generated salt.

..    // ...
47    unknowable(Bob, Alice(_handAlice, _saltAlice));
48    Bob.only(() => {
49      interact.acceptWager(wager);
50      const handBob = declassify(interact.getHand());
51    });
52    Bob.publish(handBob)
53      .pay(wager);
54    commit();
..    // ...

We now return to Alice who can reveal her secrets.

..    // ...
56    Alice.only(() => {
57      const saltAlice = declassify(_saltAlice);
58      const handAlice = declassify(_handAlice);
59    });
60    Alice.publish(saltAlice, handAlice);
61    checkCommitment(commitAlice, saltAlice, handAlice);
..    // ...

The rest of the program is unchanged from the original version, except that it uses the new names for the outcomes:

..    // ...
63    const outcome = winner(handAlice, handBob);
64    const                 [forAlice, forBob] =
65      outcome == A_WINS ? [       2,      0] :
66      outcome == B_WINS ? [       0,      2] :
67      /* tie           */ [       1,      1];
68    transfer(forAlice * wager).to(Alice);
69    transfer(forBob   * wager).to(Bob);
70    commit();
71    
72    each([Alice, Bob], () => {
73      interact.seeOutcome(outcome);
74    });
..    // ...

Since we didn’t have to change the frontend in any meaningful way, the output of running ./reach run is still the same as it ever was:

$ ./reach run

Alice played Scissors

Bob accepts the wager of 5.

Bob played Paper

Bob saw outcome Alice wins

Alice saw outcome Alice wins

Alice went from 10 to 14.9999.

Bob went from 10 to 4.9999.

 

$ ./reach run

Alice played Paper

Bob accepts the wager of 5.

Bob played Scissors

Bob saw outcome Bob wins

Alice saw outcome Bob wins

Alice went from 10 to 4.9999.

Bob went from 10 to 14.9999.

 

$ ./reach run

Alice played Scissors

Bob accepts the wager of 5.

Bob played Scissors

Bob saw outcome Draw

Alice saw outcome Draw

Alice went from 10 to 9.9999.

Bob went from 10 to 9.9999.

Except now, behind the scenes, and without any changes to the frontend, Alice takes two steps in our program and Bob only takes one, and she is protected against Bob finding her hand and using it to ensure he wins!

When we compile this version of the application, Reach’s automatic formal verification engine proves many theorems and protects us against a plethora of mistakes one might make when writing even a simple application like this. Non-Reach programmers that try to write decentralized applications are on their own trying to ensure that these problems don’t exist.

If your version isn’t working, look at the complete versions of tut-5/index.rsh and tut-5/index.mjs to make sure you copied everything down correctly!

Now our implementation of Rock, Paper, Scissors! is secure and doesn’t contain any exploits for either Alice or Bob to guarantee a win. However, it still has a final category of mistake that is common in decentralized applications: non-participation. We’ll fix this in the next step; make sure you don’t launch with this version, or Alice may decide to back out of the game when she knows she’s going to lose!

Check your understanding: True or false: Since blockchain programs run on a single, global, publicly-checked and certified consensus network, you don’t need to test them as much as normal software, which run on a wide variety of different platforms and operating systems.

Answer:

False

Check your understanding: True or false: It is easy to write correct programs that handle financial information, and even if you make a mistake, blockchains support an "Undo" operation that allows you to rollback to earlier versions of the ledger to correct mistakes and recover lost funds.

Answer:

False

Check your understanding: True or false: Reach provides automatic verifications to ensure that your program does not lose, lock away, or overspend funds and guarantees that your applications are free from entire categories of errors.

Answer:

True

Check your understanding: True or false: Reach provides tools for you to add custom verifications to your program, like ensuring that information is known only to one party, or that your implementation of a sensitive algorithm is correct.

Answer:

True