From 92c5fffc3665452dec4be54f9912a05ec8c570aa Mon Sep 17 00:00:00 2001 From: Czar102 Date: Thu, 28 Sep 2023 01:30:43 +0200 Subject: [PATCH 1/7] main spec updated for all known additional constraints --- lesson3_violations/Borda/Borda.spec | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/lesson3_violations/Borda/Borda.spec b/lesson3_violations/Borda/Borda.spec index d0c8ace..2634895 100644 --- a/lesson3_violations/Borda/Borda.spec +++ b/lesson3_violations/Borda/Borda.spec @@ -217,6 +217,10 @@ ghost mapping(address => uint256) points_mirror { init_state axiom forall address c. points_mirror[c] == 0; } +ghost mapping(address => bool) voted_mirror { + init_state axiom forall address c. !voted_mirror[c]; +} + ghost mathint countVoters { init_state axiom countVoters == 0; } @@ -235,7 +239,8 @@ hook Sload uint256 curr_point _points[KEY address a] STORAGE { } hook Sstore _voted[KEY address a] bool val (bool old_val) STORAGE { - countVoters = countVoters +1; + countVoters = countVoters + 1; + voted_mirror[a] = val; } @@ -253,4 +258,10 @@ rule resolvabilityCriterion(address f, address s, address t, address tie) { Each voter contribute a total of 6 points, so the sum of all points is six time the number of voters */ invariant sumOfPoints() - sumPoints == countVoters * 6; \ No newline at end of file + sumPoints == countVoters * 6; + + +// ADDED RULES: + +invariant votedFunctionIsVotedMapping() + forall address a. voted_mirror[a] == voted(a); From 4bcab74f13d99e1e16d6663236492f8e0f66597e Mon Sep 17 00:00:00 2001 From: Czar102 Date: Thu, 28 Sep 2023 02:04:55 +0200 Subject: [PATCH 2/7] add winner manipulation --- .../Borda/BordaMissingRule.spec | 20 ++++++++ lesson3_violations/Borda/BordaNewBug.sol | 48 +++++++++++++++++++ 2 files changed, 68 insertions(+) create mode 100644 lesson3_violations/Borda/BordaMissingRule.spec create mode 100644 lesson3_violations/Borda/BordaNewBug.sol diff --git a/lesson3_violations/Borda/BordaMissingRule.spec b/lesson3_violations/Borda/BordaMissingRule.spec new file mode 100644 index 0000000..16ae0c1 --- /dev/null +++ b/lesson3_violations/Borda/BordaMissingRule.spec @@ -0,0 +1,20 @@ +methods { + function points(address) external returns uint256 envfree; + function vote(address,address,address) external; + function voted(address) external returns bool envfree; + function winner() external returns address envfree; +} + +// Needed to prove the rule +invariant integrityPointsOfWinner(address c) + points(winner()) >= points(c); + +rule preferLastVotedHigh(address f, address s, address t) { + env e; + uint prev_points = points(winner()); + vote(e, f, s, t); + address w = winner(); + assert (points(w) == points(f) => points(w) == prev_points || w == f); + assert (points(w) == points(s) => points(w) == prev_points || w == f || w == s); + assert (points(w) == points(t) => points(w) == prev_points || w == f || w == s || w == t); +} diff --git a/lesson3_violations/Borda/BordaNewBug.sol b/lesson3_violations/Borda/BordaNewBug.sol new file mode 100644 index 0000000..b515482 --- /dev/null +++ b/lesson3_violations/Borda/BordaNewBug.sol @@ -0,0 +1,48 @@ +pragma solidity ^0.8.0; +import "./IBorda.sol"; + +contract Borda is IBorda{ + + // The current winner + address public _winner; + + // A map storing whether an address has already voted. Initialized to false. + mapping (address => bool) _voted; + + // Points each candidate has recieved, initialized to zero. + mapping (address => uint256) _points; + + // current maximum points of all candidates. + uint256 public pointsOfWinner; + + + function vote(address f, address s, address t) public override { + require(!_voted[msg.sender], "this voter has already cast its vote"); + require( f != s && f != t && s != t, "candidates are not different"); + _voted[msg.sender] = true; + voteTo(t, 1); + voteTo(s, 2); + voteTo(f, 3); + } + + function voteTo(address c, uint256 p) private { + //update points + _points[c] = _points[c]+ p; + // update winner if needed + if (_points[c] > _points[_winner]) { + _winner = c; + } + } + + function winner() external view override returns (address) { + return _winner; + } + + function points(address c) public view override returns (uint256) { + return _points[c]; + } + + function voted(address x) public view override returns(bool) { + return _voted[x]; + } +} \ No newline at end of file From e7fee4ffee62d6bcca663e120b92397633c7e107 Mon Sep 17 00:00:00 2001 From: Czar102 Date: Thu, 28 Sep 2023 02:12:13 +0200 Subject: [PATCH 3/7] add winner manipulation spec to Borda.spec --- lesson3_violations/Borda/Borda.spec | 10 ++++++++++ lesson3_violations/Borda/BordaMissingRule.spec | 10 +--------- 2 files changed, 11 insertions(+), 9 deletions(-) diff --git a/lesson3_violations/Borda/Borda.spec b/lesson3_violations/Borda/Borda.spec index 2634895..b9cfaf6 100644 --- a/lesson3_violations/Borda/Borda.spec +++ b/lesson3_violations/Borda/Borda.spec @@ -265,3 +265,13 @@ invariant sumOfPoints() invariant votedFunctionIsVotedMapping() forall address a. voted_mirror[a] == voted(a); + +rule preferLastVotedHigh(address f, address s, address t) { + env e; + uint prev_points = points(winner()); + vote(e, f, s, t); + address w = winner(); + assert (points(w) == points(f) => points(w) == prev_points || w == f); + assert (points(w) == points(s) => points(w) == prev_points || w == f || w == s); + assert (points(w) == points(t) => points(w) == prev_points || w == f || w == s || w == t); +} diff --git a/lesson3_violations/Borda/BordaMissingRule.spec b/lesson3_violations/Borda/BordaMissingRule.spec index 16ae0c1..4e390fc 100644 --- a/lesson3_violations/Borda/BordaMissingRule.spec +++ b/lesson3_violations/Borda/BordaMissingRule.spec @@ -9,12 +9,4 @@ methods { invariant integrityPointsOfWinner(address c) points(winner()) >= points(c); -rule preferLastVotedHigh(address f, address s, address t) { - env e; - uint prev_points = points(winner()); - vote(e, f, s, t); - address w = winner(); - assert (points(w) == points(f) => points(w) == prev_points || w == f); - assert (points(w) == points(s) => points(w) == prev_points || w == f || w == s); - assert (points(w) == points(t) => points(w) == prev_points || w == f || w == s || w == t); -} + From 45d08746efd35fe274ca615bc307263f7b5a78a2 Mon Sep 17 00:00:00 2001 From: Czar102 Date: Thu, 28 Sep 2023 09:04:49 +0200 Subject: [PATCH 4/7] add peritoflores' spec (rephrased) --- lesson3_violations/Borda/Borda.spec | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/lesson3_violations/Borda/Borda.spec b/lesson3_violations/Borda/Borda.spec index b9cfaf6..8392a58 100644 --- a/lesson3_violations/Borda/Borda.spec +++ b/lesson3_violations/Borda/Borda.spec @@ -275,3 +275,11 @@ rule preferLastVotedHigh(address f, address s, address t) { assert (points(w) == points(s) => points(w) == prev_points || w == f || w == s); assert (points(w) == points(t) => points(w) == prev_points || w == f || w == s || w == t); } + +rule onlyVotingCanChangeTheWinner(env e, method m){ + address winnerBefore = winner(); + calldataarg args; + m(e, args); + address winnerAfter = winner(); + assert m.selector != sig:vote(address,address,address).selector => winnerAfter == winnerBefore, "The winner can be changed only after voting"; +} From b55652f7c1fd3e93f14a63d163b5b77f9ec3b05c Mon Sep 17 00:00:00 2001 From: Czar102 Date: Thu, 28 Sep 2023 13:39:34 +0200 Subject: [PATCH 5/7] add spec for view functions revert prevention --- lesson3_violations/Borda/Borda.spec | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/lesson3_violations/Borda/Borda.spec b/lesson3_violations/Borda/Borda.spec index 8392a58..5b2d9ce 100644 --- a/lesson3_violations/Borda/Borda.spec +++ b/lesson3_violations/Borda/Borda.spec @@ -283,3 +283,15 @@ rule onlyVotingCanChangeTheWinner(env e, method m){ address winnerAfter = winner(); assert m.selector != sig:vote(address,address,address).selector => winnerAfter == winnerBefore, "The winner can be changed only after voting"; } + +rule viewNeverRevert() { + address _points; + address _voted; + + winner@withrevert(); + assert !lastReverted; + points@withrevert(_points); + assert !lastReverted; + voted@withrevert(_voted); + assert !lastReverted; +} From 269a4b648c4d6010be03f6c6a33b7e451f294986 Mon Sep 17 00:00:00 2001 From: Czar102 Date: Thu, 28 Sep 2023 16:33:26 +0200 Subject: [PATCH 6/7] add constructor ghost corruption spec --- lesson3_violations/Borda/Borda.spec | 30 +++++++++---------- .../Borda/BordaMissingRule.spec | 13 ++++++-- 2 files changed, 25 insertions(+), 18 deletions(-) diff --git a/lesson3_violations/Borda/Borda.spec b/lesson3_violations/Borda/Borda.spec index 5b2d9ce..869f874 100644 --- a/lesson3_violations/Borda/Borda.spec +++ b/lesson3_violations/Borda/Borda.spec @@ -214,11 +214,11 @@ Resolvability criterion ghost mapping(address => uint256) points_mirror { - init_state axiom forall address c. points_mirror[c] == 0; -} + init_state axiom forall address c. points_mirror[c] == 0; +} ghost mapping(address => bool) voted_mirror { - init_state axiom forall address c. !voted_mirror[c]; + init_state axiom forall address c. !voted_mirror[c]; } ghost mathint countVoters { @@ -230,17 +230,17 @@ ghost mathint sumPoints { /* update ghost on changes to _points */ hook Sstore _points[KEY address a] uint256 new_points (uint256 old_points) STORAGE { - points_mirror[a] = new_points; - sumPoints = sumPoints + new_points - old_points; + points_mirror[a] = new_points; + sumPoints = sumPoints + new_points - old_points; } hook Sload uint256 curr_point _points[KEY address a] STORAGE { - require points_mirror[a] == curr_point; + require points_mirror[a] == curr_point; } hook Sstore _voted[KEY address a] bool val (bool old_val) STORAGE { - countVoters = countVoters + 1; - voted_mirror[a] = val; + countVoters = countVoters + (val ? 1 : 0) - (old_val ? 1 : 0); + voted_mirror[a] = val; } @@ -264,16 +264,16 @@ invariant sumOfPoints() // ADDED RULES: invariant votedFunctionIsVotedMapping() - forall address a. voted_mirror[a] == voted(a); + forall address a. voted_mirror[a] == voted(a); rule preferLastVotedHigh(address f, address s, address t) { - env e; + env e; uint prev_points = points(winner()); - vote(e, f, s, t); - address w = winner(); - assert (points(w) == points(f) => points(w) == prev_points || w == f); - assert (points(w) == points(s) => points(w) == prev_points || w == f || w == s); - assert (points(w) == points(t) => points(w) == prev_points || w == f || w == s || w == t); + vote(e, f, s, t); + address w = winner(); + assert (points(w) == points(f) => points(w) == prev_points || w == f); + assert (points(w) == points(s) => points(w) == prev_points || w == f || w == s); + assert (points(w) == points(t) => points(w) == prev_points || w == f || w == s || w == t); } rule onlyVotingCanChangeTheWinner(env e, method m){ diff --git a/lesson3_violations/Borda/BordaMissingRule.spec b/lesson3_violations/Borda/BordaMissingRule.spec index 4e390fc..6cdfd45 100644 --- a/lesson3_violations/Borda/BordaMissingRule.spec +++ b/lesson3_violations/Borda/BordaMissingRule.spec @@ -5,8 +5,15 @@ methods { function winner() external returns address envfree; } -// Needed to prove the rule -invariant integrityPointsOfWinner(address c) - points(winner()) >= points(c); +rule drawFavorsWinner(env e, address f, address s, address t) { + address w1 = winner(e); + + uint256 w1Points = points(e, w1); + + vote(e, f, s, t); + + address w2 = winner(e); + assert w1 != w2 => points(e, f) > w1Points || points(e, s) > w1Points || points(e, t) > w1Points; +} From fea3772618c7ef990445a502eb6306529a048aac Mon Sep 17 00:00:00 2001 From: Czar102 Date: Thu, 28 Sep 2023 19:55:39 +0200 Subject: [PATCH 7/7] constructor state change spec --- lesson3_violations/Borda/Borda.spec | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/lesson3_violations/Borda/Borda.spec b/lesson3_violations/Borda/Borda.spec index 869f874..a3bbffb 100644 --- a/lesson3_violations/Borda/Borda.spec +++ b/lesson3_violations/Borda/Borda.spec @@ -228,10 +228,15 @@ ghost mathint sumPoints { init_state axiom sumPoints == 0; } +ghost bool accessed { + init_state axiom !accessed; +} + /* update ghost on changes to _points */ hook Sstore _points[KEY address a] uint256 new_points (uint256 old_points) STORAGE { points_mirror[a] = new_points; sumPoints = sumPoints + new_points - old_points; + accessed = true; } hook Sload uint256 curr_point _points[KEY address a] STORAGE { @@ -241,6 +246,7 @@ hook Sload uint256 curr_point _points[KEY address a] STORAGE { hook Sstore _voted[KEY address a] bool val (bool old_val) STORAGE { countVoters = countVoters + (val ? 1 : 0) - (old_val ? 1 : 0); voted_mirror[a] = val; + accessed = true; } @@ -295,3 +301,10 @@ rule viewNeverRevert() { voted@withrevert(_voted); assert !lastReverted; } + +// require that !accessed in the initial state after the constructor concludes +invariant noConstructorSSTOREs() + !accessed + { preserved { + require false; // this is purposely vacuous + } }