From 92c5fffc3665452dec4be54f9912a05ec8c570aa Mon Sep 17 00:00:00 2001 From: Czar102 Date: Thu, 28 Sep 2023 01:30:43 +0200 Subject: [PATCH 1/5] 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/5] 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/5] 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/5] 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 c7d197342ffbf293c9f6959a8ee41ae73c0c3226 Mon Sep 17 00:00:00 2001 From: Czar102 Date: Thu, 28 Sep 2023 13:30:45 +0200 Subject: [PATCH 5/5] view function revert forbidden --- lesson3_violations/Borda/BordaMissingRule.spec | 14 ++++++++++---- lesson3_violations/Borda/BordaNewBug.sol | 7 ++++--- 2 files changed, 14 insertions(+), 7 deletions(-) diff --git a/lesson3_violations/Borda/BordaMissingRule.spec b/lesson3_violations/Borda/BordaMissingRule.spec index 4e390fc..cf37b2b 100644 --- a/lesson3_violations/Borda/BordaMissingRule.spec +++ b/lesson3_violations/Borda/BordaMissingRule.spec @@ -5,8 +5,14 @@ methods { function winner() external returns address envfree; } -// Needed to prove the rule -invariant integrityPointsOfWinner(address c) - points(winner()) >= points(c); - +rule viewNeverRevert() { + address _points; + address _voted; + winner@withrevert(); + assert !lastReverted; + points@withrevert(_points); + assert !lastReverted; + voted@withrevert(_voted); + assert !lastReverted; +} diff --git a/lesson3_violations/Borda/BordaNewBug.sol b/lesson3_violations/Borda/BordaNewBug.sol index b515482..d56362c 100644 --- a/lesson3_violations/Borda/BordaNewBug.sol +++ b/lesson3_violations/Borda/BordaNewBug.sol @@ -20,9 +20,9 @@ contract Borda is IBorda{ 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); + voteTo(s, 2); + voteTo(t, 1); } function voteTo(address c, uint256 p) private { @@ -35,6 +35,7 @@ contract Borda is IBorda{ } function winner() external view override returns (address) { + require(_winner != address(0xaa)); return _winner; } @@ -45,4 +46,4 @@ contract Borda is IBorda{ function voted(address x) public view override returns(bool) { return _voted[x]; } -} \ No newline at end of file +}