2.5 Trust and agreement

2.5 Trust and agreement

Original link

In the previous section, we let Alice and Bob bet with tokens while playing rock, paper, scissors. However, the version of the application we wrote has a fundamental flaw: Bob can win every game!
how can that be possible? Let's review the process of Alice's victory:

$ ./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. Copy code

The problem is that Bob's honest version is being executed. In other words, this is the version that completely follows our Reach program (included in his private local step). If Bob's backend is dishonest, he can execute a different code, calculate the value of handA provided by Alice, and then punch, so that Bob can be safe.
For example: If Bob's code is changed to:

.. //... 25 B.only( () => { 26 interact.acceptWager(wager); 27 const handB = (handA + 1 )% 3 ; }); 28 B.publish(handB) 29 .pay (wager); .. //... Copy code

Then he will ignore the front end and directly calculate the winning value.
Running this version of the program, we see the following output:

$ ./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. Copy code

In this version, unlike the previous honest version, Bob has never queried the front end, so there is no line in the output above that shows what gesture Bob made. At this point, Bob will win no matter what Alice plays.
If Bob wins several to, how do we know he is really cheating or luck is on his side of it?
Reach has an automatic verification engine, which can mathematically prove that Bob always wins in this version (that is, the final result variable is 0), which means Bob cheated. We can add these lines of code to Reach to do this:

.. //... 31 const outcome = (handA + ( 4 -handB))% 3 ; 32 require (handB == (handA + 1 )% 3 ); 33 assert(outcome == 0 ); 34 const [ forA, forB] = .. //... Copy code
  • Line 32 requires proof that this version of Bob is dishonest.
  • Add an assert statement on line 33 to make the program prove.

Before adding this piece of code, when we run

./reach run
When, it will output 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 16 theorems; No failures! Copy code

But now, it outputs 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 21 theorems; No failures! Copy code
  • Line 7 is different from the above. He proved more theorems for our program. Because the proof of the theorem is different in different verification modes, it outputs 5 more, not just one.

Many programming languages contain such a determination, but Reach is one of the few special compiler does not just check when inserting run for this property, but rather mathematical proof at compile time to prove that the expression is always true.
In this example, we used Reach's automatic verification engine to prove that Bob's attack behavior was consistent with our expectations. But the ideal situation is: the use of verification shows that the program is not flawed, that is, we are not attacked.
Reach automatically includes some of these assertions in every program. This is why every version of our Rock Paper Scissors will show and check a series of theorems after running. In order to see this, we can deliberately add an error to the program to see the effect of these theorems.
Now we deliberately modified the settlement rules by mistake: when Alice won, she only got her own chips, not Bob.

.. //... 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(); .. //... Copy code
  • [0, 1] in line 36 should be [0, 2] in the correct version.

When we run

When compiling tut-5-attack/index-bad.rsh, its error report is as follows:

Verification failed: when ALL participants are honest of theorem: assert msg: "balance assertion" at ./index-bad.rsh:45:11:application //Violation witness const interact_Alice_wager = 2; //^ from interaction at ./index-bad.rsh:14:12:application const handA/4 = 2; //^ from evaluating interact("Alice")."getHand"() at ./index-bad.rsh:20:50:application //Theorem formalization const outcome/26 = (handA/4 + (4-((handA/4 + 1)% 3)))% 3; //^ would be 0 const v37 = (outcome/26 == 0)? [0, 1]: ((outcome/26 == 1)? [1, 1]: [2, 0]); //^ would be [0, 1] assert(0 == (((interact_Alice_wager + interact_Alice_wager)-(v37[0] * interact_Alice_wager))-(v37[1] * interact_Alice_wager))); Copy code

There is a lot of information in the compiler output to help experienced programmers track down problems. The most important parts are

  • Line 7 tries to prove the theorem: "The balance at the end of the program is 0, that is, no tokens are left in the contract forever."
  • Line 8 states that this happens when the program exits from line 45, and it prompts the programmer to check the code on line 45.
  • Lines 10-14 describe the values that may cause the theorem to fail.
  • Lines 16-21 outline the failure theorem.

These automatic verifications can help Reach programmers. Even if they are not written in the code, Reach will still prevent these types of errors from occurring in the program.
However, we can also add an explicit assertion in the program, make sure that you see directly all before punching each version Alice punches Bob results were rejected.
We will use the tut-4/index. rsh version from the previous section, which is Bob's honest version. (If you need to view its content, please click the previous link.)
After Alice publishes and before Bob runs the local step, we add a line of code:

.. //... 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()); }); .. //... Copy code
  • Line 25 is an additional knowledge assertion that Bob cannot know Alice's value HandA at this time. Here, this is obviously impossible, because Alice has already disclosed HandA on line 21. In many cases, the problem is not so obvious. Reach's automatic verification engine will consider the correlation between the value that Bob knows and Alice's confidential value.

When we run the new

./reach run
When, it will report this assertion is wrong:
tut-5-attack/index-fails.txt !

.. 3 of theorem unknowable("Bob", handA/7) 4 at ./index-fails.rsh:25:17:application 5 .. Copy code

When errors and attacks are discovered, it is not enough to fix them. Be sure to remember to add an assertion to the code so that when a similar attack or error occurs, the assertion will not be established. This will ensure that we will not suffer from all similar attacks and will not make mistakes again.
Now we use this concept of automatic verification, to rewrite our "rock-paper-scissors"! Make it more safe and reliable.
1. we define the rules of rock, paper, scissors! Abstract it, build a logical framework and fill in the details:

. 1 'REACH 0.1' ; 2 . 3 const [isHand, of ROCK, PAPER, SCISSORS] = makeEnum ( . 3 ); . 4 const [isOutcome, B_WINS, the DRAW, A_WINS] = makeEnum ( . 3 ); . 5 . 6 const Winner = ( Handa, Handb ) => 7 ((handA + ( 4 -handB))% 3 ); .. //... Copy code
  • Line 1 is the usual Reach version number.
  • Lines 3 and 4 define the gestures that can be made and the result of the game.
  • Lines 6 and 7 define the function to calculate the winner of the game.

When we first wrote Rock Paper Scissors, we convinced you that this formula for calculating the winner is correct, but it is safer to let the program actually check. One way to check is to implement a JavaScript front-end that does not interact with real users and does not randomly generate values. Instead, it returns specific test scenario values and checks whether the output meets expectations. This is a typical debugging method, and it is also feasible in Reach. In Reach, we can write such test cases directly into the Reach program as a verification assertion.

.. //... 9 assert(winner(ROCK, PAPER) == B_WINS); 10 assert(winner(PAPER, ROCK) == A_WINS); 11 assert(winner(ROCK, ROCK) == DRAW); .. //... Copy code
  • Line 9 asserts that when Alice plays a stone and Bob plays, the winner should be Bob

However, in Reach, we can use automatic verification to express stronger assertions about program behavior. For example, we can assert that no matter what the values of handA and handB are, the winner will always return the correct result:

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

We can specify that when the values of handA and handB are the same (no matter what), the winner always returns a tie:

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

Both of these examples use forall , which allows Reach programmers to traverse all possible values of some variables in a certain part of the program. You may think that proving these theorems is time-consuming because you have to traverse the possibilities of the bits of hand A and hand B: 1552518092300708935148,...(there are 247 bits in between)...,468750892846853816057856 possibilities (for example, Ethereum uses 256 Bit unsigned integer). But in fact, on the author's 2015 MacBook Pro, Reach only took less than half a second. This is because Reach uses an advanced symbolic execution engine to abstractly calculate this theorem, rather than considering these possibilities one by one.
Back in this program, we then specify the participant interaction interface for Alice and Bob. Most of it is the same as before, but now we have to provide a random number for each front end. This random number will be used to protect Alice's gestures later.

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

The only difference is line 21, which calls hasRandom in the Reach standard library .

.. //... 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 }); .. //... Copy code

Similarly, we only need to modify one line of the JavaScript front end. Line 21 allows each participant's Reach code to generate random numbers as needed.
These two changes may look the same, but their meanings are completely different. The first part, line 21 of the Reach program, adds hasRandom to the interface that the backend needs to provide from the frontend. The second part, line 21 in JavaScript, adds hasRandom to the implementation provided by the front-end to the back-end.
Next is the important point. We will implement this application and make sure that Alice's gestures are protected until Bob punches. First of all, Alice still has to announce the bet. Then we let Alice be able to punch, but also keep it secret, this is a scenario where encryption promises . Reach's standard library comes with makecommitment , which can help you easily complete this task.

.. //... 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(); .. //... Copy code
  • In line 37, Alice decides her gesture, but it is not made public.
  • Line 38 Alice promises the gesture. At the same time, there is a secret "salt", which will be made public later.
  • On line 39, Alice decrypts the promise and the bet.
  • On line 40, Alice makes them public, and line 41 asks Alice to pay the bet into the contract.

At this point, we can declare the knowledge assertion "Bob knows neither gestures nor "salt"", and then continue his program.

The key is to include the salt value in the promise, so that the promise to the same handA value will not always be the same. Another key is not to disclose the value of the salt first, and then disclose it later, because if the attacker knows the range of possible values, they can enumerate and compare with the promised result to finally get the value we want to keep secret.


.. //... 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(); .. //... Copy code
  • Line 44 is the knowledge assertion.
  • Lines 45 to 49 remain the same as before.
  • Line 50 is the payment operation, but we have not yet calculated who the bet belongs to because Alice's gesture has not been made public.

Back to Alice, now she can reveal her secrets.

.. //... 52 A.only( () => { 53 const [saltA, handA] = declassify([_saltA, _handA]); }); 54 A.publish(saltA, handA); 55 checkCommitment( commitA, saltA, handA); .. //... Copy code
  • In line 53, Alice decrypts the secret information.
  • In line 54 Alice discloses it.
  • Line 55 checks whether the published value matches the original value. Honest participants will do this, but dishonest participants may violate this.

The rest of the program is the same as the original version, except that the name of the result has been changed:

.. //... 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(); }); Copy code

Since we did not make any substantial changes to the front end, run

./reach run
The output is still the same as before:

$ ./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. Copy code

So far, the front end has not changed, but in essence, Alice's operation has become two steps, and Bob's operation has only one step, which prevents Alice from losing the game because Bob "slowly out".
When we compiled this version, Reach's automatic verification engine proved many theorems and avoided a lot of mistakes that might be made when writing such a simple application. Those non-Reach programmers trying to write decentralized applications have to make sure that these problems do not exist.

If your program does not run correctly, please check the complete tut-5/index. rsh version and tut -5/index. mjs version to make sure you copied everything correctly!

Now, the rock-paper-scissors we have implemented are safe. Neither Alice nor Bob can cheat to guarantee victory. However, there is one last type of error common in decentralized applications: not participating.
We will solve this problem in the next step ;
make sure not to release this version, otherwise Alice may quit the game first when she knows she will lose!

Do you understand?:

True or false:

Since blockchain programs run on a single, global, publicly inspected and certified consensus network, you don't need to test them like ordinary software, they run on a variety of different platforms and operating systems.

Answer: wrong

Do you understand?:

True or false:

It is easy to write the correct procedures for handling financial information. Even if you make a mistake, the blockchain supports "undo" operations, allowing you to roll back to an earlier version of the ledger to correct errors and recover lost funds.

The answer is: wrong

Do you understand?:

True or false:

Reach provides automatic verification to ensure that your program will not lose, lock or overspend funds, and ensure that your application will not have all types of errors.

The answer is: yes

Do you understand?:

True or false:

Reach provides you with tools to add custom verification to the program, such as ensuring that information is only known to one party, or ensuring that the implementation of sensitive algorithms is correct.

The answer is: yes

Previous: 2.4 Betting and betting

Next: 2.6 Handling of timeout issues