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.0.

Bob played Scissors

Alice saw outcome Alice wins

Bob saw outcome Alice wins

Alice went from 10.0 to 14.999999999999687175.

Bob went from 10.0 to 4.999999999999978229.

The problem is that these 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:

..    // ...
25    B.only(() => {
26      interact.acceptWager(wager);
27      const handB = (handA + 1) % 3; });
28    B.publish(handB)
29      .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.0.

Alice saw outcome Bob wins

Bob saw outcome Bob wins

Alice went from 10.0 to 4.999999999999683071.

Bob went from 10.0 to 14.999999999999978232.

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:

..    // ...
31    const outcome = (handA + (4 - handB)) % 3;
32    require(handB == (handA + 1) % 3);
33    assert(outcome == 0);
34    const [forA, forB] =
..    // ...

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

..    // ...

 2    Verifying knowledge assertions

 3    Verifying with mode = VM_Honest

 4    Verifying with mode = VM_Dishonest RoleContract

 5    Verifying with mode = VM_Dishonest (RolePart "Alice")

 6    Verifying with mode = VM_Dishonest (RolePart "Bob")

 7    Checked 14 theorems; No failures!

..    // ...

But now, it prints out

..    // ...

 2    Verifying knowledge assertions

 3    Verifying with mode = VM_Honest

 4    Verifying with mode = VM_Dishonest RoleContract

 5    Verifying with mode = VM_Dishonest (RolePart "Alice")

 6    Verifying with mode = VM_Dishonest (RolePart "Bob")

 7    Checked 19 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 deliberating inserting an error in 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 [forA, forB] =
35          // was: outcome == 0 ? [0, 2] :
36          outcome == 0 ? [0, 1] : // <-- Oops
37          outcome == 1 ? [1, 1] :
38          [2, 0];
39    transfer(forA * wager).to(A);
40    transfer(forB * wager).to(B);
41    commit();
..    // ...

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

..    

 4    Verification failed:

 5      in VM_Honest mode

 6      of theorem TBalanceZero

 7      at ./tut-4-attack/index-bad.rsh:45:11:application

 8    

 9      Theorem formalization:

10      (= ctc_balance4 0 )

11    

12      This could be violated if...

..    

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-3/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:

..    // ...
21    A.publish(wager, handA)
22      .pay(wager);
23    commit();
24    
25    unknowable(B, A(handA));
26    B.only(() => {
27      interact.acceptWager(wager);
28      const handB = declassify(interact.getHand()); });
..    // ...

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

..    

 3    Verification failed:

 4      of theorem unknowable("Bob", v1)

 5      at ./tut-4-attack/index-fails.rsh:25:17:application

..    

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 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(UInt256, handA =>
14      forall(UInt256, 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(UInt256, (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 1,552,518,092,300,708,935,148,...247 digits...,468,750,892,846,853,816,057,856 possibilities for the bits of handA (twice!) and handB. In fact, on the author’s MacBook Pro from early 2015, 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([], UInt256),
23            seeOutcome: Fun([UInt256], Null) };
..    // ...

The only line that is different is line 21, which includes hasRandom, from the Reach standard library, in the interface.

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

Similarly, we only need to modify one line of our JavaScript frontend. Line 19 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 19 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.

..    // ...
36    A.only(() => {
37      const _handA = interact.getHand();
38      const [_commitA, _saltA] = makeCommitment(interact, _handA);
39      const [wager, commitA] = declassify([interact.wager, _commitA]); });
40    A.publish(wager, commitA)
41      .pay(wager);
42    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.

..    // ...
44    unknowable(B, A(_handA, _saltA));
45    B.only(() => {
46      interact.acceptWager(wager);
47      const handB = declassify(interact.getHand()); });
48    B.publish(handB)
49      .pay(wager);
50    commit();
..    // ...

We now return to Alice who can reveal her secrets.

..    // ...
52    A.only(() => {
53      const [saltA, handA] = declassify([_saltA, _handA]); });
54    A.publish(saltA, handA);
55    checkCommitment(commitA, saltA, handA);
..    // ...

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

..    // ...
57    const outcome = winner(handA, handB);
58    const [forA, forB] =
59          outcome == A_WINS ? [2, 0] :
60          outcome == B_WINS ? [0, 2] :
61          [1, 1];
62    transfer(forA * wager).to(A);
63    transfer(forB * wager).to(B);
64    commit();
65    
66    each([A, B], () => {
67      interact.seeOutcome(outcome); });
68    exit(); });

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.0.

Bob played Paper

Bob saw outcome Alice wins

Alice saw outcome Alice wins

Alice went from 10.0 to 14.999999999999553643.

Bob went from 10.0 to 4.999999999999969352.

 

$ ./reach run

Alice played Paper

Bob accepts the wager of 5.0.

Bob played Scissors

Bob saw outcome Bob wins

Alice saw outcome Bob wins

Alice went from 10.0 to 4.999999999999553626.

Bob went from 10.0 to 14.999999999999969352.

 

$ ./reach run

Alice played Scissors

Bob accepts the wager of 5.0.

Bob played Scissors

Bob saw outcome Draw

Alice saw outcome Draw

Alice went from 10.0 to 9.999999999999550271.

Bob went from 10.0 to 9.999999999999969352.

Except now, behind the scenes, and without any changes to the frontend, Alice now takes two steps in 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-4/index.rsh and tut-4/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!