From 77f44c0ae8eca9c615297edb888f7613bd0be881 Mon Sep 17 00:00:00 2001 From: sitvanit Date: Thu, 7 Dec 2023 12:41:51 +0200 Subject: [PATCH] Rule quality examples --- RuleQuality/Manager/Manager.sol | 52 ++++++++++ RuleQuality/Manager/Manager.spec | 94 +++++++++++++++++++ .../Manager/ManagerAdvancedSanity.conf | 8 ++ RuleQuality/Manager/ManagerBasicSanity.conf | 9 ++ RuleQuality/Manager/ManagerPartial.spec | 81 ++++++++++++++++ .../Manager/ManagerPartialBasicSanity.conf | 9 ++ RuleQuality/Manager/README.md | 7 ++ RuleQuality/Manager/run.sh | 1 + RuleQuality/NativeBalances/README.md | 30 ++++++ .../NativeBalances/certora/specs/Auction.spec | 44 +++++++++ .../NativeBalances/contracts/Auction.sol | 16 ++++ .../NativeBalances/contracts/AuctionFixed.sol | 17 ++++ RuleQuality/NativeBalances/runAuction.conf | 10 ++ .../NativeBalances/runAuctionFixed.conf | 11 +++ 14 files changed, 389 insertions(+) create mode 100644 RuleQuality/Manager/Manager.sol create mode 100644 RuleQuality/Manager/Manager.spec create mode 100644 RuleQuality/Manager/ManagerAdvancedSanity.conf create mode 100644 RuleQuality/Manager/ManagerBasicSanity.conf create mode 100644 RuleQuality/Manager/ManagerPartial.spec create mode 100644 RuleQuality/Manager/ManagerPartialBasicSanity.conf create mode 100644 RuleQuality/Manager/README.md create mode 100755 RuleQuality/Manager/run.sh create mode 100644 RuleQuality/NativeBalances/README.md create mode 100644 RuleQuality/NativeBalances/certora/specs/Auction.spec create mode 100644 RuleQuality/NativeBalances/contracts/Auction.sol create mode 100644 RuleQuality/NativeBalances/contracts/AuctionFixed.sol create mode 100644 RuleQuality/NativeBalances/runAuction.conf create mode 100644 RuleQuality/NativeBalances/runAuctionFixed.conf diff --git a/RuleQuality/Manager/Manager.sol b/RuleQuality/Manager/Manager.sol new file mode 100644 index 00000000..d62d9d65 --- /dev/null +++ b/RuleQuality/Manager/Manager.sol @@ -0,0 +1,52 @@ + +contract Manager { + + struct ManagedFund { + // The current manager of the fund + address currentManager; + // Management can be transferred, however the new manager needs to claim the management after being set as pending manager. + address pendingManager; + // amount managed + uint256 amount; + } + + // Maps a fundId to its struct + mapping (uint256 => ManagedFund) public funds; + + // A flag indicating if an address is a current manager + mapping (address => bool) public isActiveManager; + + + function createFund(uint256 fundId) public { + require(msg.sender != address(0)); + require(funds[fundId].currentManager == address(0)); + require(!isActiveManager[msg.sender]); + funds[fundId].currentManager = msg.sender; + isActiveManager[msg.sender] = true; + } + + + function setPendingManager(uint256 fundId, address pending) public { + require(funds[fundId].currentManager == msg.sender); + funds[fundId].pendingManager = pending; + } + + + function claimManagement(uint256 fundId) public { + require(msg.sender != address(0) && funds[fundId].currentManager != address(0)); + require(funds[fundId].pendingManager == msg.sender); + require(!isActiveManager[msg.sender]); + isActiveManager[funds[fundId].currentManager] = false; + funds[fundId].currentManager = msg.sender; + funds[fundId].pendingManager = address(0); + isActiveManager[msg.sender] = true; + } + + function getCurrentManager(uint256 fundId) public view returns (address) { + return funds[fundId].currentManager; + } + + function getPendingManager(uint256 fundId) public view returns (address) { + return funds[fundId].pendingManager; + } +} diff --git a/RuleQuality/Manager/Manager.spec b/RuleQuality/Manager/Manager.spec new file mode 100644 index 00000000..0d0d24b7 --- /dev/null +++ b/RuleQuality/Manager/Manager.spec @@ -0,0 +1,94 @@ +methods { + function getCurrentManager(uint256 fundId) external returns (address) envfree; + function getPendingManager(uint256 fundId) external returns (address) envfree; + function isActiveManager(address a) external returns (bool) envfree; +} + +invariant ManagerZeroIsNotActive() + !isActiveManager(0); + +invariant tautologyInv() + !isActiveManager(0) <=> isActiveManager(0)==false ; + + + +rule uniqueManager(uint256 fundId1, uint256 fundId2, method f) { + require fundId1 != fundId2; + requireInvariant ManagerZeroIsNotActive(); + require getCurrentManager(fundId1) != 0 => isActiveManager(getCurrentManager(fundId1)); + require getCurrentManager(fundId2) != 0 => isActiveManager(getCurrentManager(fundId2)); + require getCurrentManager(fundId1) != getCurrentManager(fundId2) ; + + env e; + if (f.selector == sig:claimManagement(uint256).selector) + { + uint256 id; + /// Advanced sanity check: + /// Since there is symetry between fundId1 and funcdId2 and they are havoced it is enough to have require id == fundId1 + require id == fundId1 || id == fundId2; + claimManagement(e, id); + } + else { + calldataarg args; + f(e,args); + } + assert getCurrentManager(fundId1) != getCurrentManager(fundId2), "managers not different"; + assert getCurrentManager(fundId1) != 0 => isActiveManager(getCurrentManager(fundId1)), "manager of fund1 is not active"; + assert getCurrentManager(fundId2) != 0 => isActiveManager(getCurrentManager(fundId2)), "manager of fund2 is not active"; +} + + +rule uniqueManagerWeak(uint256 fundId1, uint256 fundId2, method f) { + require fundId1 != fundId2; + requireInvariant ManagerZeroIsNotActive(); + require getCurrentManager(fundId1) != 0 && isActiveManager(getCurrentManager(fundId1)); + require getCurrentManager(fundId2) != 0 && isActiveManager(getCurrentManager(fundId2)); + require getCurrentManager(fundId1) != getCurrentManager(fundId2) ; + + env e; + if (f.selector == sig:claimManagement(uint256).selector) + { + uint256 id; + require id == fundId1 || id == fundId2; + claimManagement(e, id); + } + else { + calldataarg args; + f(e,args); + } + assert getCurrentManager(fundId1) != getCurrentManager(fundId2), "managers not different"; + assert getCurrentManager(fundId1) != 0 && isActiveManager(getCurrentManager(fundId1)), "manager of fund1 is not active"; + assert getCurrentManager(fundId2) != 0 && isActiveManager(getCurrentManager(fundId2)), "manager of fund2 is not active"; +} + +/// This is a taughtology because by the require, it is never the case that newManager== other && newManager == manager. +rule tautology(uint256 fundId, method f) { + address manager = getCurrentManager(fundId); + address other; + require other != manager; + env e; + calldataarg args; + f(e,args); + address newManager = getCurrentManager(fundId); + assert ( newManager!= other || newManager != manager); +} + +rule vacuityMistake(uint256 fundId, address pending ) { + env e; + require pending == getPendingManager(fundId); + require e.msg.sender != pending; + claimManagement(e, fundId ); + assert getCurrentManager(fundId)== pending; +} + +rule mistake(uint256 fundId, address pending ) { + address manager; + env e; + require manager != pending ; + require pending != 0; + // changes manager to pending manger + claimManagement(e, fundId ); + // the following is wrong, the engineer wanted to reason about the pending before claimManagement + assert getPendingManager(fundId) == pending => getCurrentManager(fundId)== pending; +} + diff --git a/RuleQuality/Manager/ManagerAdvancedSanity.conf b/RuleQuality/Manager/ManagerAdvancedSanity.conf new file mode 100644 index 00000000..cb123146 --- /dev/null +++ b/RuleQuality/Manager/ManagerAdvancedSanity.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "Manager.sol" + ], + "msg": "manager", + "verify": "Manager:Manager.spec", + "rule_sanity": "advanced" +} diff --git a/RuleQuality/Manager/ManagerBasicSanity.conf b/RuleQuality/Manager/ManagerBasicSanity.conf new file mode 100644 index 00000000..1d6102eb --- /dev/null +++ b/RuleQuality/Manager/ManagerBasicSanity.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "Manager.sol" + ], + "msg": "manager", + "verify": "Manager:Manager.spec", + "rule_sanity": "basic" +} + diff --git a/RuleQuality/Manager/ManagerPartial.spec b/RuleQuality/Manager/ManagerPartial.spec new file mode 100644 index 00000000..875a7fff --- /dev/null +++ b/RuleQuality/Manager/ManagerPartial.spec @@ -0,0 +1,81 @@ +methods { + function getCurrentManager(uint256 fundId) external returns (address) envfree; + function getPendingManager(uint256 fundId) external returns (address) envfree; + function isActiveManager(address a) external returns (bool) envfree; +} + +invariant ManagerZeroIsNotActive() + !isActiveManager(0); + +rule uniqueManager(uint256 fundId1, uint256 fundId2, method f) { + require fundId1 != fundId2; + requireInvariant ManagerZeroIsNotActive(); + require getCurrentManager(fundId1) != 0 => isActiveManager(getCurrentManager(fundId1)); + require getCurrentManager(fundId2) != 0 => isActiveManager(getCurrentManager(fundId2)); + require getCurrentManager(fundId1) != getCurrentManager(fundId2) ; + + env e; + if (f.selector == sig:claimManagement(uint256).selector) + { + uint256 id; + /// Since there is symetry between fundId1 and funcdId2 and they are havoced it is enough to have require id == fundId1 + require id == fundId1 || id == fundId2; + claimManagement(e, id); + } + else { + calldataarg args; + f(e,args); + } + assert getCurrentManager(fundId1) != getCurrentManager(fundId2), "managers not different"; + assert getCurrentManager(fundId1) != 0 => isActiveManager(getCurrentManager(fundId1)), "manager of fund1 is not active"; + assert getCurrentManager(fundId2) != 0 => isActiveManager(getCurrentManager(fundId2)), "manager of fund2 is not active"; +} + + +rule uniqueManagerWeak(uint256 fundId1, uint256 fundId2, method f) { + require fundId1 != fundId2; + requireInvariant ManagerZeroIsNotActive(); + require getCurrentManager(fundId1) != 0 && isActiveManager(getCurrentManager(fundId1)); + require getCurrentManager(fundId2) != 0 && isActiveManager(getCurrentManager(fundId2)); + require getCurrentManager(fundId1) != getCurrentManager(fundId2) ; + + env e; + if (f.selector == sig:claimManagement(uint256).selector) + { + uint256 id; + require id == fundId1 || id == fundId2; + claimManagement(e, id); + } + else { + calldataarg args; + f(e,args); + } + assert getCurrentManager(fundId1) != getCurrentManager(fundId2), "managers not different"; + assert getCurrentManager(fundId1) != 0 && isActiveManager(getCurrentManager(fundId1)), "manager of fund1 is not active"; + assert getCurrentManager(fundId2) != 0 && isActiveManager(getCurrentManager(fundId2)), "manager of fund2 is not active"; +} + +/// This is a taughtology because by the require, it is never the case that newManager== other && newManager == manager. +rule tautology(uint256 fundId, method f) { + address manager = getCurrentManager(fundId); + address other; + require other != manager; + env e; + calldataarg args; + f(e,args); + address newManager = getCurrentManager(fundId); + assert ( newManager!= other || newManager != manager); +} + +rule mistake(uint256 fundId, address pending ) { + address manager; + env e; + require manager != pending ; + require pending != 0; + claimManagement(e, fundId ); + // the following is wrong, the engineer wanted to reason about the pending before claimManagement + assert getPendingManager(fundId) == pending => getCurrentManager(fundId)== pending; + // check that indeed the hypothesis is always false + // assert( getPendingManager(fundId) != pending); +} + diff --git a/RuleQuality/Manager/ManagerPartialBasicSanity.conf b/RuleQuality/Manager/ManagerPartialBasicSanity.conf new file mode 100644 index 00000000..c776f78c --- /dev/null +++ b/RuleQuality/Manager/ManagerPartialBasicSanity.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "Manager.sol" + ], + "msg": "manager", + "verify": "Manager:ManagerPartial.spec", + "rule_sanity": "basic" +} + diff --git a/RuleQuality/Manager/README.md b/RuleQuality/Manager/README.md new file mode 100644 index 00000000..8523b0b0 --- /dev/null +++ b/RuleQuality/Manager/README.md @@ -0,0 +1,7 @@ +# Vacuity and Tautology + +With `rule_sanity: basic` the vacuity and tautology are not recognized. + +With `rule_sanity: advanced` + +[A report of this run](https://prover.certora.com/output/1902/1c70db2a4dcd4b8d8f1cfa8827305920?anonymousKey=b738f329a0f3b14c43f754bb1b3ba8cb02d41ea5) diff --git a/RuleQuality/Manager/run.sh b/RuleQuality/Manager/run.sh new file mode 100755 index 00000000..34d76161 --- /dev/null +++ b/RuleQuality/Manager/run.sh @@ -0,0 +1 @@ +certoraRun Manager.sol --verify Manager:Manager.spec \ No newline at end of file diff --git a/RuleQuality/NativeBalances/README.md b/RuleQuality/NativeBalances/README.md new file mode 100644 index 00000000..e2d9c521 --- /dev/null +++ b/RuleQuality/NativeBalances/README.md @@ -0,0 +1,30 @@ +# nativeBalances + +This directory demonstrates how to use nativeBalances. + +## Incorrect Code +- The rule `bidIncreasesAssets` fails for `Auction.sol` because: + - `msg.value` is passed to `currentContract` at the entrance to `bid()` + - the sender changes to `currentContract` in internal `bid()` and all its balance is transferred so it does not increase. +- The rule `bidSuccessfullyExpectVacuous` passes vacuously because of the + `require e.msg.value > nativeBalances[currentContract]` in the spec + and `require msg.value >= msg.value + nativeBalances[currentContract]` in the code where + `nativeBalances[currentContract] > 0`. + +Run this configuration via: + +```certoraRun certora/conf/runAuction.conf``` + +[A report of this run](https://prover.certora.com/output/1902/32a97d6902c6418ebc5847c062073bce?anonymousKey=5c875dad99a1fcd5e39bda1acc5d47c3e18b9fe4) + +## Correct Code +- The rule passes for `AuctionFixed.sol` because at the entrance to `bid` `address(this).balance` is already increased by `msg.value`, +so the balance of `currentContract >= currentBid` and therefore the transfer succeeds. +- The rule `bidSuccessfullyExpectVacuous` passes non-vacuously for `AuctionFixed.sol` because the amount transferred is `currentBid` for which `msg.value >= currentBid` can hold. + +Run this configuration via: + +```certoraRun certora/conf/runAuctionFixed.conf``` + +[A report of this run](https://prover.certora.com/output/1902/d0aecf17decc482c8e0bceacf7f09b9e?anonymousKey=b17fa824c7ac14ab9b63dada5d53e4c4fda15988) + diff --git a/RuleQuality/NativeBalances/certora/specs/Auction.spec b/RuleQuality/NativeBalances/certora/specs/Auction.spec new file mode 100644 index 00000000..f6ee6195 --- /dev/null +++ b/RuleQuality/NativeBalances/certora/specs/Auction.spec @@ -0,0 +1,44 @@ +/** + * @title Native balances Example + * + * This is an example specification for using nativeBalances. + */ + +methods { + function currentBid() external returns uint256 envfree; +} + +/// @title Basic rules //////////////////////////////////////////////////// + +/*** + This rule demonstrates how the source of amount transferred affects the balance of the current contract. + This rule fails for `Auction.sol` because: + 1. The balance of `currentContract` is increased by `msg.value` at the entrance to `bid()`. + 2. the sender changes to `currentContract` in internal `bid()` and all his balance is transferred, so his balance does not increase. + This rule passes for `AuctionFixed.sol` because only `currentBid` is transferred. + */ +rule bidIncreasesAssets() { + env e; + require(e.msg.sender != currentContract); + require(e.msg.value > currentBid() ); + uint256 balanceBefore = nativeBalances[currentContract]; + bid(e); + assert nativeBalances[currentContract] > balanceBefore; +} + +/*** + This rule demonstrates how the source of amount transferred affects the balance of the current contract. + This rule passes vacuously for `Auction.sol` because of the `require e.msg.value > nativeBalances[currentContract]` in the spec + and `require msg.value >= msg.value + nativeBalances[currentContract]` in the code where `nativeBalances[currentContract] > 0`. + It passes non-vacuously for AuctionFixed.sol because the amount transferred is `currentBid` for which `msg.value >= currentBid` + can hold. + */ +rule bidSuccessfullyExpectVacuous() { + env e; + uint256 balanceBefore = nativeBalances[currentContract]; + require(e.msg.sender != currentContract); + require(e.msg.value > 0 && e.msg.value > balanceBefore); + require (balanceBefore > 0); + bid(e); + assert nativeBalances[currentContract] >= balanceBefore; +} diff --git a/RuleQuality/NativeBalances/contracts/Auction.sol b/RuleQuality/NativeBalances/contracts/Auction.sol new file mode 100644 index 00000000..79ab60e7 --- /dev/null +++ b/RuleQuality/NativeBalances/contracts/Auction.sol @@ -0,0 +1,16 @@ +contract Auction +{ + address currentBidder; + uint256 public currentBid; + + // At the entrance to `bid` address(this).balance is already increased by msg.value, + // so the receiver gets `msg.value + address(this).balance` before. + // This reverts only if msg.value < address(this).balance + function bid() public payable + { + require(msg.value >= address(this).balance); + payable(currentBidder).transfer(address(this).balance); + currentBidder = msg.sender; + currentBid = msg.value; + } +} \ No newline at end of file diff --git a/RuleQuality/NativeBalances/contracts/AuctionFixed.sol b/RuleQuality/NativeBalances/contracts/AuctionFixed.sol new file mode 100644 index 00000000..61dd5cc8 --- /dev/null +++ b/RuleQuality/NativeBalances/contracts/AuctionFixed.sol @@ -0,0 +1,17 @@ +contract AuctionFixed +{ + + address currentBidder; + uint256 public currentBid; + + // At the entrance to `bid` address(this).balance is already increased by `msg.value`, + // So the balance of `currentContract >= currentBid` and therefore the transfer succeeds. + // This reverts only if msg.value < currentBid. + function bid() public payable + { + require(msg.value >= currentBid); + payable(currentBidder).transfer(currentBid); + currentBidder = msg.sender; + currentBid = msg.value; + } +} \ No newline at end of file diff --git a/RuleQuality/NativeBalances/runAuction.conf b/RuleQuality/NativeBalances/runAuction.conf new file mode 100644 index 00000000..0cbbb547 --- /dev/null +++ b/RuleQuality/NativeBalances/runAuction.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "contracts/Auction.sol", + ], + "verify": "Auction:certora/specs/Auction.spec", + "msg": "Native balances", + "optimistic_loop": true, + "loop_iter": "3", + "rule_sanity" : "basic" +} \ No newline at end of file diff --git a/RuleQuality/NativeBalances/runAuctionFixed.conf b/RuleQuality/NativeBalances/runAuctionFixed.conf new file mode 100644 index 00000000..53514749 --- /dev/null +++ b/RuleQuality/NativeBalances/runAuctionFixed.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "contracts/AuctionFixed.sol", + ], + "verify": "AuctionFixed:certora/specs/Auction.spec", + "msg": "Native balances fixed", + "optimistic_loop": true, + "loop_iter": "3", // Unwind each loop in the contract 3 times. + "rule_sanity" : "basic" // check there is a trace satisfying the rule. + +}