From 1e811d34d268266dab87bd68cfdcabec167cd2e1 Mon Sep 17 00:00:00 2001 From: ernestognw Date: Thu, 18 Apr 2024 10:53:54 -0600 Subject: [PATCH 1/6] Update certora-cli to 7.3.0 --- certora/specs/ERC20.spec | 4 ++-- certora/specs/ERC721.spec | 6 +++--- requirements.txt | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec index 21a03358508..6b9b55de5d0 100644 --- a/certora/specs/ERC20.spec +++ b/certora/specs/ERC20.spec @@ -23,11 +23,11 @@ ghost mathint sumOfBalances { // overflows Alice's balance when receiving a transfer. This is not possible unless the contract is deployed into an // already used address (or upgraded from corrupted state). // We restrict such behavior by making sure no balance is greater than the sum of balances. -hook Sload uint256 balance _balances[KEY address addr] STORAGE { +hook Sload uint256 balance _balances[KEY address addr] { require sumOfBalances >= to_mathint(balance); } -hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { +hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) { sumOfBalances = sumOfBalances - oldValue + newValue; } diff --git a/certora/specs/ERC721.spec b/certora/specs/ERC721.spec index bad4c473772..e5d5546f2e9 100644 --- a/certora/specs/ERC721.spec +++ b/certora/specs/ERC721.spec @@ -113,7 +113,7 @@ ghost mapping(address => mathint) _ownedByUser { init_state axiom forall address a. _ownedByUser[a] == 0; } -hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STORAGE { +hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) { _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0); _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0); _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0); @@ -132,13 +132,13 @@ ghost mapping(address => mathint) _balances { init_state axiom forall address a. _balances[a] == 0; } -hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { +hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) { _supply = _supply - oldValue + newValue; } // TODO: This used to not be necessary. We should try to remove it. In order to do so, we will probably need to add // many "preserved" directive that require the "balanceOfConsistency" invariant on the accounts involved. -hook Sload uint256 value _balances[KEY address user] STORAGE { +hook Sload uint256 value _balances[KEY address user] { require _balances[user] == to_mathint(value); } diff --git a/requirements.txt b/requirements.txt index bdea09aa819..60f7546c341 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1 +1 @@ -certora-cli==4.13.1 +certora-cli==7.3.0 From 274acce46760b0847ffa40de4ec49814dc0c1296 Mon Sep 17 00:00:00 2001 From: ernestognw Date: Fri, 19 Apr 2024 10:22:52 -0600 Subject: [PATCH 2/6] Use SOLC_VERSION 0.8.24 --- .github/workflows/formal-verification.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index 6b4ca2cad7c..0200b6b6b34 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -12,7 +12,7 @@ on: env: PIP_VERSION: '3.10' JAVA_VERSION: '11' - SOLC_VERSION: '0.8.20' + SOLC_VERSION: '0.8.24' concurrency: ${{ github.workflow }}-${{ github.ref }} From 52665fd9b3a7fe7b114f633657c53df97ee993dd Mon Sep 17 00:00:00 2001 From: ernestognw Date: Fri, 19 Apr 2024 11:34:12 -0600 Subject: [PATCH 3/6] Fix AccessManaged summarization --- certora/specs/AccessManaged.spec | 3 +++ 1 file changed, 3 insertions(+) diff --git a/certora/specs/AccessManaged.spec b/certora/specs/AccessManaged.spec index adcb8593634..7e4619d96d0 100644 --- a/certora/specs/AccessManaged.spec +++ b/certora/specs/AccessManaged.spec @@ -7,6 +7,9 @@ methods { function authority_canCall_immediate(address) external returns (bool); function authority_canCall_delay(address) external returns (uint32); function authority_getSchedule(address) external returns (uint48); + + // Summaries + function _.setAuthority(address) external => DISPATCHER(true); } invariant isConsumingScheduledOpClean() From cd865969382f9f5b15d6339e8482b3782ebf978f Mon Sep 17 00:00:00 2001 From: ernestognw Date: Fri, 19 Apr 2024 12:02:44 -0600 Subject: [PATCH 4/6] Add setAuthority rule to AccessManaged --- certora/harnesses/AccessManagedHarness.sol | 15 ++++++++------ certora/specs/AccessManaged.spec | 24 +++++++++++++++++++++- 2 files changed, 32 insertions(+), 7 deletions(-) diff --git a/certora/harnesses/AccessManagedHarness.sol b/certora/harnesses/AccessManagedHarness.sol index 50be23ad5bd..1e73d445d85 100644 --- a/certora/harnesses/AccessManagedHarness.sol +++ b/certora/harnesses/AccessManagedHarness.sol @@ -10,27 +10,30 @@ contract AccessManagedHarness is AccessManaged { constructor(address initialAuthority) AccessManaged(initialAuthority) {} - function someFunction() public restricted() { + function someFunction() public restricted { // Sanity for FV: the msg.data when calling this function should be the same as the data used when checking // the schedule. This is a reformulation of `msg.data == SOME_FUNCTION_CALLDATA` that focuses on the operation // hash for this call. require( - IAccessManager(authority()).hashOperation(_msgSender(), address(this), msg.data) - == - IAccessManager(authority()).hashOperation(_msgSender(), address(this), SOME_FUNCTION_CALLDATA) + IAccessManager(authority()).hashOperation(_msgSender(), address(this), msg.data) == + IAccessManager(authority()).hashOperation(_msgSender(), address(this), SOME_FUNCTION_CALLDATA) ); } function authority_canCall_immediate(address caller) public view returns (bool result) { - (result,) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector); + (result, ) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector); } function authority_canCall_delay(address caller) public view returns (uint32 result) { - (,result) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector); + (, result) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector); } function authority_getSchedule(address caller) public view returns (uint48) { IAccessManager manager = IAccessManager(authority()); return manager.getSchedule(manager.hashOperation(caller, address(this), SOME_FUNCTION_CALLDATA)); } + + function _hasCode(address account) public view returns (bool) { + return account.code.length > 0; + } } diff --git a/certora/specs/AccessManaged.spec b/certora/specs/AccessManaged.spec index 7e4619d96d0..2b232a4bfb7 100644 --- a/certora/specs/AccessManaged.spec +++ b/certora/specs/AccessManaged.spec @@ -7,9 +7,10 @@ methods { function authority_canCall_immediate(address) external returns (bool); function authority_canCall_delay(address) external returns (uint32); function authority_getSchedule(address) external returns (uint48); + function _hasCode(address) external returns (bool) envfree; // Summaries - function _.setAuthority(address) external => DISPATCHER(true); + function _.setAuthority(address) external => DISPATCHER(true); } invariant isConsumingScheduledOpClean() @@ -35,3 +36,24 @@ rule callRestrictedFunction(env e) { ) ); } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Only valid authorities can be set by the current authority │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule setAuthority(env e) { + require nonpayable(e); + + address newAuthority; + + address previousAuthority = authority(); + + setAuthority@withrevert(e, newAuthority); + bool success = !lastReverted; + + assert (success && authority() == newAuthority) <=> ( + previousAuthority == e.msg.sender && + _hasCode(newAuthority) + ); +} From 6a100abfe1954cc96fbc5065aa4d131b469c2cdc Mon Sep 17 00:00:00 2001 From: ernestognw Date: Fri, 19 Apr 2024 16:03:05 -0600 Subject: [PATCH 5/6] Bump solc to 0.8.25 --- .github/workflows/formal-verification.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index 0200b6b6b34..232c786777e 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -12,7 +12,7 @@ on: env: PIP_VERSION: '3.10' JAVA_VERSION: '11' - SOLC_VERSION: '0.8.24' + SOLC_VERSION: '0.8.25' concurrency: ${{ github.workflow }}-${{ github.ref }} From 42bf8c3c7458133b3e66cd190a40aef25b05ec49 Mon Sep 17 00:00:00 2001 From: ernestognw Date: Wed, 24 Apr 2024 10:35:02 -0600 Subject: [PATCH 6/6] Update AccessManaged spec --- certora/specs/AccessManaged.spec | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/certora/specs/AccessManaged.spec b/certora/specs/AccessManaged.spec index 2b232a4bfb7..fdd57d00283 100644 --- a/certora/specs/AccessManaged.spec +++ b/certora/specs/AccessManaged.spec @@ -52,8 +52,9 @@ rule setAuthority(env e) { setAuthority@withrevert(e, newAuthority); bool success = !lastReverted; - assert (success && authority() == newAuthority) <=> ( + assert success <=> ( previousAuthority == e.msg.sender && _hasCode(newAuthority) ); + assert success => newAuthority == authority(); }