在上一节中,我们让 Alice 和 Bob 在玩石头剪刀布的时候可以以代币下注。但是,我们编写的应用程序版本有一个根本性的漏洞: Bob可以赢得每场比赛!
怎么可能呢?我们回顾一下 Alice 获胜的过程:
/reach 运行 |
---|
Alice出石头 |
Bob下5 注 |
Bob出剪刀 |
Alice看到的结果是她赢了 |
Bob看到了Alice获胜 |
Alice筹码从10变成14.9999 |
Bob从10变成4.9999 |
问题是这个版本的游戏只执行的是Bob 诚实的版本,换句话说这是完全遵循 Reach 程序的版本(包括在他私有的本地步骤中)。对于一个不诚实的 Bob 后端来说,可以执行一份不同的代码,通过 Alice 提供的 handA 的值计算后再出拳,这样Bob就能无往不利。
如果我们将 Bob 的代码更改为:
tut-4-attack/index.rsh
.. // ...
25 B.only(() => {
26 interact.acceptWager(wager);
27 const handB = (handA + 1) % 3; });
28 B.publish(handB)
29 .pay(wager);
.. // ...
那么他会忽略前端,直接计算能获胜的值。
运行这个版本的程序,我们看到的输出如下:
reach 运行 |
---|
Alice出剪刀 |
Bob下5注 |
Alice 看到了 Bob 获胜的结果 |
Bob看到了结果Bob赢了 |
Alice从10变成4.9999 |
Bob从10升到了14.9999 |
在这个版本中,不像之前诚实的版本,Bob从来没有查询前端,所以上面没有看到Bob出什么手势的输出。无论Alice出什么,Bob都会赢。
—
如果Bob连胜了好几把,我们怎么知道他是作弊了还是运气真的站在他这边了呢?Reach有自动验证引擎,它可以从数学上证明这个版本中Bob总是获胜(即最终结果变量是0) ,这就表示Bob作弊了。我们可以在 Reach中添加这几行代码以做到这件事:
tut-4-attack/index.rsh
.. // ...
31 const outcome = (handA + (4 - handB)) % 3;
32 require(handB == (handA + 1) % 3);
33 assert(outcome == 0);
34 const [forA, forB] =
.. // ...
- 32行要求使用Bob不诚实的版本证明。
- 第33行加入一个assert语句使程序进行证明。
在加入这一段代码之前,当我们运行./reach run时,它会输出消息:
tut-3/index.txt
.. // … |
---|
2.验证通用链接器 |
3.验证所有参与者是否诚实 |
4.验证参与者是否均不诚实 |
5.验证只有“Alice”才是诚实的 |
6.验证只有“Bob”才是诚实的 |
7.检查了16个定理,没有失败! |
但现在,它输出消息:
tut-4-attack/index.txt
.. // … |
---|
2.通用连接器的评定 |
3.当所有参与者都是诚实的时,核实所有参与者都是诚实的 |
4.无参与者诚实时的无偿性 |
5.只有“Alice”才是诚实的 |
6.只有“Bob”才是诚实的 |
7.检查了21个定理,没有失败! |
- 第 7 行跟上面不一样了,他对我们的程序证明了更多的定理。因为在不同的验证模式下,定理的证明是不同的,所以它多输出 5 个,不止是 1 个。
—
许多编程语言都包含这样的判定,但 Reach 是其中少数特别的,编译器不只是为这个属性插入运行时检查,而是在编译时进行数学证明,证明表达式始终为 true 。
在这个例子里,我们使用了 Reach 的自动验证引擎来证明Bob的攻击行为与我们预期的一致。但是理想的情况是 : 使用验证表明程序没有缺陷,即我们没有遭受攻击。
Reach 在每个程序中都自动包含一些这样的断言。这就是为什么《剪刀石头布》的每一个版本运行完都显示检查了一系列的定理。为了看出这点,我们可以在程序中故意加入一个错误,看看这些定理的作用。
现在我们改变结算规则 : 在Alice获胜时,她只得到她自己的筹码,没有得到Bob的。
tut-4-attack/index-bad.rsh
.. // ...
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();
.. // ...
- 第 36 行中的 [0, 1]在正确版本中应该是[0, 2]。
当我们运行./ reach 编译tut-4-attack/index-bad.rsh时,它的报错如下:
tut-4-attack/index-bad.txt
… |
---|
4 Verification failed: |
5 when ALL participants are honest |
6 of theorem: assert |
7 msg: “balance assertion” |
8 at ./index-bad.rsh:45:11:application |
9 |
10 // Violation witness |
11 const interact_Alice_wager = 2; |
12 // ^ from interaction at ./index-bad.rsh:14:12:application |
13 const handA/4 = 2; |
14 // ^ from evaluating interact(“Alice”).”getHand”() at ./index-bad.rsh:20:50:application |
15 |
16 // Theorem formalization |
17 const outcome/26 = (handA/4 + (4 - ((handA/4 + 1) % 3))) % 3; |
18 // ^ would be 0 |
19 const v37 = (outcome/26 == 0) ? [0, 1] : ((outcome/26 == 1) ? [1, 1] : [2, 0]); |
20 // ^ would be [0, 1] |
21 assert(0 == (((interact_Alice_wager + interact_Alice_wager) - (v37[0] interact_Alice_wager)) - (v37[1] interact_Alice_wager))); |
22 |
… |
编译器输出中有很多信息可以帮助有经验的程序员追踪问题。但最重要的几个部分是
- 第 7 行试图证明定理 : “程序结束时的余额是0,即没有代币被永远遗留在合约里。”
- 第 8 行指出,这发生在程序从第 45 行退出时,它提示程序员检查第45行的代码。
- 第 10 - 14 行描述了可能导致定理失败的值。
- 第 16 - 21 行概述了失败的定理。
这些自动验证可以帮助 Reach 程序员,即使他们没有写在代码里,Reach仍然会保护程序不发生这些类型的错误。
—
但是,我们也可以明确的在程序中添加一个断言,直接确保所有 Bob 出拳之前就看到 Alice 出拳结果的每个版本都被拒绝
我们将使用上一节中的 tut - 3 / index . rsh 版本,也就是 Bob 诚实的版本。(如果您需要查看它的内容,请单击前面的链接。)
在 Alice 发布之后、 Bob 运行本地步骤之前,我们添加一行:
tut-4-attack/index-fails.rsh
.. // ...
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()); });
.. // ...
- 第25行是一个额外的知识断言,即Bob此时不能知道Alice的值HandA。此时,这显然不可能,因为Alice在第21行已经公开HandA了。很多时候问题不会这么明显,Reach的自动验证引擎会考虑Bob所知道的值与Alice的机密值的相关性。
当我们运行新的 ./reach run时,它会报这个断言是错误的:
tut-4-attack/index-fails.txt!
.. |
---|
3 of theorem unknowable(“Bob”, handA/7) |
4 at ./index-fails.rsh:25:17:application |
5 |
.. |
当发现错误和攻击时,仅仅修正它们还不够。一定要记得在代码里添加一个断言,使得如发生攻击或错误时,这个断言将无法成立。这样就可以确保不会遭受所有类似的攻击,并且不会再次发生错误。
—
现在我们利用这个自动验证的概念,重写我们的“剪刀石头布”!使其更加安全可靠。
首先,我们定义剪刀石头布的规则!将其抽象化,先搭建逻辑框架再填入细节:
tut-4/index.rsh
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);
.. // ...
- 第 1 行是通常的 Reach 版本号。
- 第3行和第4行定义了可以出的手势,以及游戏的结果。
- 第6行和第7行定义了计算游戏赢家的函数。
我们第一次写《剪刀石头布》的时候,我们说服您相信这个计算获胜者的公式是正确的,但是实际检查还是比较保险。检查的一种方法是实现一个 JavaScript 前端,它不与真正的用户交互,也不会随机生成值,而是返回特定的测试场景值,并检查输出是否符合预期。这是一种典型的调试方式,在Reach 中也可行。 Reach 允许我们将这样的测试用例直接写入 Reach 程序,作为验证断言。
tut-4/index.rsh
.. // ...
9 assert(winner(ROCK, PAPER) == B_WINS);
10 assert(winner(PAPER, ROCK) == A_WINS);
11 assert(winner(ROCK, ROCK) == DRAW);
.. // ...
- 第 9 行断言,当 Alice 出石头 而 Bob出布时,则胜者应该是 Bob
但是, Reach 的自动验证允许我们表达关于程序行为的更有力的断言。例如,我们可以断言,无论 handA 和 handB 的值是什么,winner总是会返回正确的结果:
tut-4/index.rsh
.. // ...
13 forall(UInt, handA =>
14 forall(UInt, handB =>
15 assert(isOutcome(winner(handA, handB)))));
.. // ...
我们可以指定,当handA, handB的值相同(无论是什么)时,winner总是返回平局:
tut-4/index.rsh
.. // ...
17 forall(UInt, (hand) =>
18 assert(winner(hand, hand) == DRAW));
.. // ...
这两个例子都用到了forall ,这让Reach 程序员可以遍历程序中某部份的一些变量的所有可能值。你可能觉得证明这些定理很费时,因为必须遍历hand A和hand B的bits的可能性为1552518092300708935148,…(247位)…,468750892846853816057856种可能性(例如,以太坊使用256 位的无符号整数)。但实际上,在笔者 2015 年版的 MacBook Pro上,Reach只运行了不到半秒钟的时间。这是因为 Reach 使用了高级的符号执行引擎抽象地运算这个定理,而不一一考虑这些可能。
回到这个程序中,我们接着为 Alice 和 Bob 指定参与者交互接口。大部份都和以前一样,除了我们要为每个前端提供一个随机数。我们等下会用这个来保护Alice的手势。
tut-4/index.rsh
.. // ...
20 const Player =
21 { ...hasRandom, // <--- new!
22 getHand: Fun([], UInt),
23 seeOutcome: Fun([UInt], Null) };
.. // ...
唯一不同的是第 21 行,它调用了 Reach 标准库中的 hasRandom 。
tut-4/index.mjs
.. // ...
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 });
.. // ...
同样,我们只需要修改 JavaScript 前端的一行。第 21 行允许每个参与者的 Reach 代码根据需要生成随机数。
这两处修改看起来可能一样,但它们的含义完全不同。前一部分, Reach 程序的第 21 行,将 hasRandom 添加到后端需要前端提供的接口。第二部份, JavaScript 中的第 21 行,将 hasRandom 添加到前端提供给后端的实现中。
接下来是重点,我们将实现这个应用程序,并确保在Bob出拳之前Alice 的手势一直受到保护。首先 Alice 还是要公布赌注。然后我们让Alice 能出拳,但也要保密,这是一个加密承诺方案的场景。Reach 的标准库附带了 makecommitment ,这可以帮助你轻松完成这个任务。
tut-4/index.rsh
.. // ...
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();
.. // ...
- 第 37 行有Alice计算她的手势,但没有公开。
- 第 38 行有她的承诺的手势。它还带有一个秘密的“salt”,在稍后会公开。
- 第 39 行Alice将承诺和赌注解密。
- 第 40 行让Alice公开,第 41 行则让Alice把赌注付到合约中。
此时,我们可以声明知识断言,即 Bob 既不知道手势,也不知道“salt”,接着再继续他的程序。
关键是要把salt值纳入承诺,这样对同一值的几个承诺就不会都一样。另一个关键是先不要公开salt的值,一会儿再公开,因为如果攻击者知道一些可能值的范围,他们可以通过枚举,并与承诺的结果进行比较,最终得出我们要保密的值。
.. // ...
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();
.. // ...
- 第 44 行是知识断言。
- 第45至49行仍然与先前一样。
- 第 50 行是支付操作,但是我们还没计算赌注归谁,因为 Alice 的手势还没有公开。
回到Alice这边,现在她可以公开她的秘密了。
tut-4/index.rsh
.. // ...
52 A.only(() => {
53 const [saltA, handA] = declassify([_saltA, _handA]); });
54 A.publish(saltA, handA);
55 checkCommitment(commitA, saltA, handA);
.. // ...
- 第 53 行是Alice将秘密信息解密。
- 54 行中Alice公开它。
- 第 55 行检查已发布的值是否与原始值匹配。诚实的参与者会这么做,但不诚实的参予者可能会违背这点。
程序的其余部分都与原始版本相同,只是结果名称改变了一下:
tut-4/index.rsh
.. // ...
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(); });
由于我们没有对前端做任何实质改变, 运行 ./ reach run 的输出还是跟以前一样:
$ ./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. |
到了现在,前端没有任何变化,但本质上Alice的操作变成两步,Bob的操作只有一步,这使得Alice不会因为Bob通过”慢出”而输了游戏。
当我们编译这个版本时, Reach 的自动验证引擎证明了许多定理,并替我们避免了大量写这样一个简单的应用程序时可能犯的错误。那些试图编写去中心化应用程序的非Reach程序员得自己确保这些问题不存在。
如果您的程序不能正确运行,请查看完整的 tut - 4 / index . rsh 版本和 tut -4/index. mjs 版本,确保您正确地复制了所有内容!
现在,我们实现的剪刀石头布是安全的,无论是Alice或Bob都不能通过作弊,以保证取胜。然而,它还有最后一类在去中心化应用程序中常见的错误:不参与。我们将在下一步解决这个问题;确保不要发布这个版本,否则Alice在知道她会输的时候,可能就先退出游戏了!
你知道了吗?:是非题: 由于区块链程序运行在一个单一的、全球的、经过公开检查和认证的共识网络上,你不需要像普通软件那样测试它们,它们运行在各种不同的平台和操作系统上。 答案是: 错 你知道了吗?:是非题: 编写处理财务信息的正确程序很容易,即使你犯了错误,区块链也支持“撤销”操作,允许你回滚到账本的早期版本,以纠正错误并收回损失的资金。 答案是: 错 你知道了吗?:是非题: Reach 提供自动验证,以确保您的程序不会丢失、锁定或超支资金,并保证您的应用程序不会出现所有类别的错误。 答案是: 对 你知道了吗?:是非题: Reach 为您提供了向程序添加自定义验证的工具,比如确保信息仅为一方所知,或者确保敏感算法的实现是正确的。 答案是: 对