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:
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
:
Line 32 requires that the dishonest version of Bob be used for the proof.
Line 33 conducts the proof by including an assert statement in the program.
Before we had this line in the file, when we ran ./reach run, 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 14 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 19 theorems; No failures! 
Line 7 is different and shows that more theorems have been proven about our program. It prints out five more, rather than one more, because the theorem is proved differently in the different verification modes.
—
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 compiletime 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.
Line 36 has
[0, 1]
, but should have[0, 2]
.
When we run ./reach compile tut5attack/indexbad.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 ./indexbad.rsh:45:11:application 
9 
10 // Violation witness 
11 const interact_Alice_wager = 2; 
12 // ^ from interaction at ./indexbad.rsh:14:12:application 
13 const handA/23 = 2; 
14 // ^ from evaluating interact("Alice")."getHand"() at ./indexbad.rsh:20:50:application 
15 
16 // Theorem formalization 
17 const outcome/42 = (handA/23 + (4  ((handA/23 + 1) % 3))) % 3; 
18 // ^ would be 0 
19 const v53 = (outcome/42 == 0) ? [0, 1] : ((outcome/42 == 1) ? [1, 1] : [2, 0]); 
20 // ^ would be [0, 1] 
21 assert(0 == (((interact_Alice_wager + interact_Alice_wager)  (v53[0] * interact_Alice_wager))  (v53[1] * interact_Alice_wager))); 
22 
... 
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
Line 7 says that this is an attempt to prove the theorem that the balance at the end of the program is zero, which means that no network tokens are sealed in the contract forever.
Line 8 says that this happens when the program exits on line 45, which directs the programmer to that path through the program.
Lines 1014 describe the values that could cause the theorem to fail.
Lines 1621 outline the theorem that failed.
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 tut4/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()); });
.. // ...
Line 25 contains a knowledge assertion that Bob cannot know Alice’s value
handA
at this point in the program. In this case, it is obvious that this is not true, because Alice shareshandA
at line 21. In many cases, this is not obvious and Reach’s automatic verification engine has to reason about how values that Bob does know are connected to values that might be related to Alice’s secret values.
When we run ./reach run, it reports that this assertion is false:
.. 
3 of theorem unknowable("Bob", handA/26) 
4 at ./indexfails.rsh:25:17:application 
5 
.. 
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:
Line 1 is the usual Reach version header.
Lines 3 and 4 define enumerations for the hands that may be played, as well as the outcomes of the game.
Lines 6 and 7 define the function that computes the winner of the game.
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.
Line 9 makes an assertion that when Alice plays Rock and Bob plays Paper, then Bob wins as expected.
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:
And we can specify that whenever the same value is provided for both hands, no matter what it is, winner
always returns 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 (e.g., Ethereum uses 256bits for its unsigned integers) 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.
The only line that is different is line 21, which includes hasRandom
, from the Reach standard library, in the interface.
.. // ...
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.
Line 37 has Alice compute her hand, but not declassify it.
Line 38 has her compute a commitment to the hand. It comes with a secret "salt" value that must be revealed later.
Line 39 has Alice declassify the commitment and her wager.
Line 40 has her publish them and with line 41 has her include the wager funds in the publication.
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();
.. // ...
Line 44 states the knowledge assertion.
Lines 45 through 49 are unchanged from the original version.
Line 50 has the transaction commit, without computing the payout, because we can’t yet, because Alice’s hand is not yet public.
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);
.. // ...
Line 53 has Alice declassify the secret information.
Line 54 has her publish it.
Line 55 checks that the published values match the original values. This will always be the case with honest participants, but dishonest participants may violate this assumption.
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. 
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 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. NonReach 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 tut5/index.rsh and tut5/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: nonparticipation. 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, publiclychecked 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