From 284949451b1f9dbcf1a66a0c6e198c80da68ded7 Mon Sep 17 00:00:00 2001 From: Czar102 Date: Thu, 28 Sep 2023 19:48:39 +0200 Subject: [PATCH] constructor doesn't change state --- lesson3_violations/Borda/Borda.conf | 5 +- lesson3_violations/Borda/Borda.spec | 55 ++++++++++++++++--- .../Borda/BordaMissingRule.spec | 25 +++++++++ lesson3_violations/Borda/BordaNewBug.sol | 54 ++++++++++++++++++ 4 files changed, 129 insertions(+), 10 deletions(-) create mode 100644 lesson3_violations/Borda/BordaMissingRule.spec create mode 100644 lesson3_violations/Borda/BordaNewBug.sol diff --git a/lesson3_violations/Borda/Borda.conf b/lesson3_violations/Borda/Borda.conf index 0a46999..1c35f38 100644 --- a/lesson3_violations/Borda/Borda.conf +++ b/lesson3_violations/Borda/Borda.conf @@ -2,8 +2,7 @@ "files": [ "Borda.sol:Borda" ], - "verify": "Borda:Borda.spec", - "send_only": false, + "verify": "Borda:BordaMissingRule.spec", + "send_only": true, "msg": "Verification of Borda", - "rule_sanity" : "advanced" } diff --git a/lesson3_violations/Borda/Borda.spec b/lesson3_violations/Borda/Borda.spec index d0c8ace..869f874 100644 --- a/lesson3_violations/Borda/Borda.spec +++ b/lesson3_violations/Borda/Borda.spec @@ -214,8 +214,12 @@ 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]; +} ghost mathint countVoters { init_state axiom countVoters == 0; @@ -226,16 +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; + countVoters = countVoters + (val ? 1 : 0) - (old_val ? 1 : 0); + voted_mirror[a] = val; } @@ -253,4 +258,40 @@ 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); + +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); +} + +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"; +} + +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/BordaMissingRule.spec b/lesson3_violations/Borda/BordaMissingRule.spec new file mode 100644 index 0000000..b598cf8 --- /dev/null +++ b/lesson3_violations/Borda/BordaMissingRule.spec @@ -0,0 +1,25 @@ +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; +} + +ghost bool accessed { + init_state axiom !accessed; +} + +hook Sstore _points[KEY address a] uint256 new_points (uint256 old_points) STORAGE { + accessed = true; +} + +hook Sstore _voted[KEY address a] bool val (bool old_val) STORAGE { + accessed = true; +} + +// require that !accessed in the initial state after the constructor concludes +invariant noConstructorSSTOREs() + !accessed + { preserved { + require false; // this is purposely vacuous + } } diff --git a/lesson3_violations/Borda/BordaNewBug.sol b/lesson3_violations/Borda/BordaNewBug.sol new file mode 100644 index 0000000..c650d24 --- /dev/null +++ b/lesson3_violations/Borda/BordaNewBug.sol @@ -0,0 +1,54 @@ +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; + + constructor() { + // many, many votes there + voteTo(address(0xaa), 6); + + _voted[address(0xaa)] = true; + } + + 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(f, 3); + voteTo(s, 2); + voteTo(t, 1); + } + + 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]; + } +}