Formal Verification of Anti-Cheating Protocols in Cryptoeconomic Systems
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

131 lines
6.3 KiB

  1. // Formal Model based on Snowflake from Scalable and Probabilistic Leaderless BFTConsensus through Metastability (https://avalanchelabs.org/QmT1ry38PAmnhparPUmsUNHDEGHQusBLD6T5XJh4mUUn3v.pdf)
  2. // Model Authored by Sarah Jamie Lewis
  3. ctmc
  4. const samples;
  5. const alpha;
  6. const beta;
  7. const color1init;
  8. const color2init;
  9. const color3init;
  10. const color4init;
  11. const timeout_max;
  12. const origcol1 = color1init;
  13. const origcol2 = color1init;
  14. const origcol3 = color1init;
  15. formula hsum = (color1+color2+color3);
  16. formula htotal_diff = (hsum=3 | hsum=6) ? 0 : 1;
  17. formula sum = (color1+color2+color3+jit);
  18. formula total_diff = (sum=4 | sum=8) ? 0 : (
  19. (sum=5 | sum=7) ? 1 : 2
  20. );
  21. // This will always return false.
  22. formula consensus_check = (color1 > 0) & (color1 = color2) & (color3 = jit) & (color3 = color1);
  23. formula have_enough_samples = samples = 2 ? (sampled_1_2 > 0 & sampled_1_3 > 0) | (sampled_1_2 > 0 & sampled_1_4 > 0) | (sampled_1_3 > 0 & sampled_1_4 > 0) : (sampled_1_2 > 0 & sampled_1_3 > 0 & sampled_1_4 > 0);
  24. formula opposite_color = (color1 = 1) ? 2 : 1;
  25. formula diff2 = (sampled_1_2 = opposite_color);
  26. formula diff3 = (sampled_1_3 = opposite_color);
  27. formula diff4 = (sampled_1_4 = opposite_color);
  28. formula count_diff = (diff2 & diff3 & diff4) ? 3 : (
  29. (diff2 & diff3) | (diff3 & diff4) | (diff2 & diff4) ? 2 : (
  30. (diff2 | diff3 | diff4) ? 1 : 0
  31. ));
  32. formula over_alpha = (count_diff >= alpha);
  33. // If all honest nodes have reached their beta then we are done
  34. formula done = (count1 = beta) & (count2 = beta) & (count3 = beta);
  35. // If there is no skew among the honest nodes, seed doubt
  36. formula jit = (htotal_diff = 0) ? opposite_color: color1;
  37. module adversarial_scheduler
  38. [p1] (color1 > 0) -> true;
  39. [p2] (count1 = beta) -> true;
  40. [p3] (count2 = beta) -> true;
  41. endmodule
  42. module peer1
  43. color1: [0..2] init color1init;
  44. // Sampled This Round
  45. sampled_1_2: [0..samples] init 0;
  46. sampled_1_3: [0..samples] init 0;
  47. sampled_1_4: [0..samples] init 0;
  48. count1: [0..beta] init 0;
  49. delay: bool init false;
  50. timeout: [0..(timeout_max+1)] init 0;
  51. // Atomic Lookups make this *much* easier for the correct nodes...yet they will still fail...
  52. [] (samples=2 & !delay & consensus_check = false & count1 < beta & sampled_1_2 = 0 & sampled_1_3 = 0 & have_enough_samples = false) -> (sampled_1_2' = color2) & (sampled_1_3' = color3);
  53. [] (samples=2 & !delay & consensus_check = false & count1 < beta & sampled_1_4 = 0 & sampled_1_2= 0 & have_enough_samples = false) -> (delay' = true) & (sampled_1_2' = color2) & (timeout' = 0);
  54. [] (samples=2 & !delay & consensus_check = false & count1 < beta & sampled_1_4 = 0 & sampled_1_3 = 0 & have_enough_samples = false) -> (delay' = true) & (sampled_1_3' = color3) & (timeout' = 0);
  55. [] (samples=3 & !delay & consensus_check = false & count1 < beta & sampled_1_4 = 0 & sampled_1_3 = 0 & sampled_1_2 = 0 & have_enough_samples = false) -> (delay' = true) & (timeout' = 0) & (sampled_1_3' = color3) & (sampled_1_2' = color2) ;
  56. // Delay and Reset
  57. [](delay = true & timeout < timeout_max) -> (delay' = true) & (timeout' = timeout + 1);
  58. []((delay = true & timeout = timeout_max) | timeout_max = 0) -> (delay' = false) & (timeout' = 0) & (sampled_1_2' = 0) & (sampled_1_3' = 0) & (sampled_1_4' = 0);
  59. // Original non-atomic sampling code
  60. // Query Peer 2
  61. //[p1] (consensus_check = false & count1 < beta & sampled_1_2 = 0 & have_enough_samples = false) -> (sampled_1_2' = color2);
  62. // Query Peer 3
  63. //[p1] (consensus_check = false & count1 < beta & sampled_1_3 = 0 & have_enough_samples = false) -> (sampled_1_3' = color3);
  64. // Query Peer 4
  65. //[] (consensus_check = false & count1 < beta & sampled_1_4 = 0 & have_enough_samples = false) -> (sampled_1_4' = color4);
  66. // Model an adversarial node
  67. [p1] (samples=2 & delay = true & consensus_check = false & count1 < beta & sampled_1_4 = 0 & sampled_1_2 = 0 & have_enough_samples = false) -> (sampled_1_4' = opposite_color) & (delay' = false);
  68. [p1] (samples=2 & delay = true & consensus_check = false & count1 < beta & sampled_1_4 = 0 & sampled_1_3 = 0 & have_enough_samples = false) -> (sampled_1_4' = opposite_color) & (delay' = false);
  69. [p1] (samples=3 & delay = true & consensus_check = false & count1 < beta & sampled_1_4 = 0 & have_enough_samples = false) -> (sampled_1_4' = opposite_color) & (delay' = false);
  70. // If there are more of the opposite color than our chosen color, switch and reset the count
  71. [] (consensus_check = false & count1 < beta & have_enough_samples & over_alpha) -> (color1' = opposite_color) & (count1' = 0) & (sampled_1_2' = 0) & (sampled_1_3' = 0) & (sampled_1_4' = 0) & (delay' = false);
  72. // If the threshold isn't met then increase count
  73. [] (consensus_check = false & count1 < beta & have_enough_samples & over_alpha = false) -> (count1' = count1 + 1) & (sampled_1_2' = 0) & (sampled_1_3' = 0) & (sampled_1_4' = 0) & (delay' = false);
  74. // Update Color
  75. [] (consensus_check = true | count1 = beta) -> (color1' = color1);
  76. endmodule
  77. module peer2 = peer1 [ color1=color2, color2=color1, color1init = color2init, color3=color3, count1=count2, round_samples=round_samples2, sampled_1_2=sampled_2_1, sampled_1_3=sampled_2_3,sampled_1_4=sampled_2_4, diff_votes_1=diff_votes_2,p1=p2, delay = delay2, timeout = timeout2,origcol1=origcol2 ] endmodule
  78. module peer3 = peer1 [ color1=color3, color2=color1, color3=color1, color1init = color3init, count1=count3, round_samples=round_samples3, sampled_1_2=sampled_3_1, sampled_1_3=sampled_3_2,sampled_1_4=sampled_3_4, diff_votes_1=diff_votes_3, p1=p3, delay = delay3, timeout = timeout3,origcol1=origcol3 ] endmodule
  79. //module peer4 = peer1 [ color1=color4,color1init=color4init, count1=count4, round_samples=round_samples4, sampled_1_2=sampled_4_1, sampled_1_3=sampled_4_2,sampled_1_4=sampled_4_3, diff_votes_1=diff_votes_4, color4=color1 ] endmodule
  80. label "finished" = done;
  81. label "consensus" = done & (color1 = color2) & (color2 = color3);
  82. formula done_split = done & (((color1 +color2 + color3) = 3) | ((color1 +color2 + color3) = 6)) = false;
  83. label "finished_without_consensus" = done & (((color1 +color2 + color3) = 3) | ((color1 +color2 + color3) = 6)) = false;
  84. // Calculate probability of consensus
  85. rewards "network_skew"
  86. true: 1 - (htotal_diff/2);
  87. endrewards
  88. // Calculate chance of revision
  89. rewards "beta"
  90. true: count1/beta;
  91. endrewards
  92. rewards "time"
  93. true : 1;
  94. endrewards