diff --git a/.github/workflows/certora-steward.yml b/.github/workflows/certora-steward.yml index adeac1f8..56a6a73a 100644 --- a/.github/workflows/certora-steward.yml +++ b/.github/workflows/certora-steward.yml @@ -32,6 +32,10 @@ jobs: - name: Install solc run: | + cd certora/steward/ + touch applyHarness.patch + make munged + cd ../.. wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux chmod +x solc-static-linux sudo mv solc-static-linux /usr/local/bin/solc8.10 @@ -48,4 +52,8 @@ jobs: max-parallel: 16 matrix: rule: - - rules.conf + - GhoAaveSteward.conf + - GhoBucketSteward.conf + - GhoCcipSteward.conf + - GhoGsmSteward.conf + diff --git a/audits/15-09-2024_Modular_Gho_Steward_Certora.pdf b/audits/15-09-2024_Modular_Gho_Steward_Certora.pdf new file mode 100644 index 00000000..45e8dd2e Binary files /dev/null and b/audits/15-09-2024_Modular_Gho_Steward_Certora.pdf differ diff --git a/certora/steward/Makefile b/certora/steward/Makefile new file mode 100644 index 00000000..611d7a80 --- /dev/null +++ b/certora/steward/Makefile @@ -0,0 +1,28 @@ +default: help + +PATCH = applyHarness.patch +CONTRACTS_DIR = ../../src +MUNGED_DIR = munged + +help: + @echo "usage:" + @echo " make clean: remove all generated files (those ignored by git)" + @echo " make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)" + @echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)" + +munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH) + rm -rf $@ + mkdir $@ + cp -r ../../src $@ + patch -p0 -d $@ < $(PATCH) + +record: + mkdir tmp + cp -r ../../src tmp + diff -ruN tmp $(MUNGED_DIR) | sed 's+tmp/++g' | sed 's+$(MUNGED_DIR)/++g' > $(PATCH) + rm -rf tmp + +clean: + git clean -fdX + touch $(PATCH) + diff --git a/certora/steward/applyHarness.patch b/certora/steward/applyHarness.patch new file mode 100644 index 00000000..6fc8ba12 --- /dev/null +++ b/certora/steward/applyHarness.patch @@ -0,0 +1,7 @@ +diff -ruN .gitignore .gitignore +--- .gitignore 1970-01-01 02:00:00.000000000 +0200 ++++ .gitignore 2024-08-12 17:28:45.843705526 +0300 +@@ -0,0 +1,2 @@ ++* ++!.gitignore +\ No newline at end of file \ No newline at end of file diff --git a/certora/steward/conf/GhoAaveSteward.conf b/certora/steward/conf/GhoAaveSteward.conf new file mode 100644 index 00000000..2d5296ec --- /dev/null +++ b/certora/steward/conf/GhoAaveSteward.conf @@ -0,0 +1,27 @@ +{ + "files": ["certora/steward/harness/GhoAaveSteward_Harness.sol"], + "packages": [ + "@aave/core-v3/=lib/aave-v3-core", + "@aave/periphery-v3/=lib/aave-v3-periphery", + "@aave/=lib/aave-token", + "@openzeppelin/=lib/openzeppelin-contracts", + "aave-stk-v1-5/=lib/aave-stk-v1-5", + "ds-test/=lib/forge-std/lib/ds-test/src", + "forge-std/=lib/forge-std/src", + "aave-address-book/=lib/aave-address-book/src", + "aave-helpers/=lib/aave-stk-v1-5/lib/aave-helpers", + "aave-v3-core/=lib/aave-address-book/lib/aave-v3-core", + "erc4626-tests/=lib/aave-stk-v1-5/lib/openzeppelin-contracts/lib/erc4626-tests", + "openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts", + "solidity-utils/=lib/solidity-utils/src" + ], + "build_cache": true, + "optimistic_loop": true, + "process": "emv", + "prover_args": ["-depth 15","-mediumTimeout 1000"], + "smt_timeout": "2000", + "solc": "solc8.10", + "verify": "GhoAaveSteward_Harness:certora/steward/specs/GhoAaveSteward.spec", + "rule_sanity": "basic", + "msg": "GhoAaveSteward: all rules" +} \ No newline at end of file diff --git a/certora/steward/conf/rules.conf b/certora/steward/conf/GhoBucketSteward.conf similarity index 74% rename from certora/steward/conf/rules.conf rename to certora/steward/conf/GhoBucketSteward.conf index 9585a2a3..19c24a9b 100644 --- a/certora/steward/conf/rules.conf +++ b/certora/steward/conf/GhoBucketSteward.conf @@ -1,10 +1,6 @@ { "files": [ - "certora/steward/harness/GhoStewardV2_Harness.sol", - "src/contracts/facilitators/aave/interestStrategy/FixedRateStrategyFactory.sol" - ], - "link": [ - "GhoStewardV2_Harness:FIXED_RATE_STRATEGY_FACTORY=FixedRateStrategyFactory", + "src/contracts/misc/GhoBucketSteward.sol" ], "packages": [ "@aave/core-v3/=lib/aave-v3-core", @@ -21,12 +17,13 @@ "openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts", "solidity-utils/=lib/solidity-utils/src" ], + "build_cache": true, "optimistic_loop": true, "process": "emv", "prover_args": ["-depth 15","-mediumTimeout 1000"], "smt_timeout": "2000", "solc": "solc8.10", - "verify": "GhoStewardV2_Harness:certora/steward/specs/rules.spec", + "verify": "GhoBucketSteward:certora/steward/specs/GhoBucketSteward.spec", "rule_sanity": "basic", - "msg": "STEWARD: all rules" + "msg": "GhoBucketSteward: all rules" } \ No newline at end of file diff --git a/certora/steward/conf/GhoCcipSteward.conf b/certora/steward/conf/GhoCcipSteward.conf new file mode 100644 index 00000000..556761d0 --- /dev/null +++ b/certora/steward/conf/GhoCcipSteward.conf @@ -0,0 +1,27 @@ +{ + "files": ["certora/steward/harness/GhoCcipSteward_Harness.sol"], + "packages": [ + "@aave/core-v3/=lib/aave-v3-core", + "@aave/periphery-v3/=lib/aave-v3-periphery", + "@aave/=lib/aave-token", + "@openzeppelin/=lib/openzeppelin-contracts", + "aave-stk-v1-5/=lib/aave-stk-v1-5", + "ds-test/=lib/forge-std/lib/ds-test/src", + "forge-std/=lib/forge-std/src", + "aave-address-book/=lib/aave-address-book/src", + "aave-helpers/=lib/aave-stk-v1-5/lib/aave-helpers", + "aave-v3-core/=lib/aave-address-book/lib/aave-v3-core", + "erc4626-tests/=lib/aave-stk-v1-5/lib/openzeppelin-contracts/lib/erc4626-tests", + "openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts", + "solidity-utils/=lib/solidity-utils/src" + ], + "build_cache": true, + "optimistic_loop": true, + "process": "emv", + "prover_args": ["-depth 15","-mediumTimeout 1000"], + "smt_timeout": "2000", + "solc": "solc8.10", + "verify": "GhoCcipSteward_Harness:certora/steward/specs/GhoCcipSteward.spec", + "rule_sanity": "basic", + "msg": "GhoCcipSteward: all rules" +} \ No newline at end of file diff --git a/certora/steward/conf/sanity.conf b/certora/steward/conf/GhoGsmSteward.conf similarity index 66% rename from certora/steward/conf/sanity.conf rename to certora/steward/conf/GhoGsmSteward.conf index b69e3c96..0929927c 100644 --- a/certora/steward/conf/sanity.conf +++ b/certora/steward/conf/GhoGsmSteward.conf @@ -1,10 +1,10 @@ { "files": [ - "certora/steward/harness/GhoStewardV2_Harness.sol", - "src/contracts/facilitators/aave/interestStrategy/FixedRateStrategyFactory.sol" + "certora/steward/harness/GhoGsmSteward_Harness.sol", + "src/contracts/facilitators/gsm/feeStrategy/FixedFeeStrategyFactory.sol" ], "link": [ - "GhoStewardV2_Harness:FIXED_RATE_STRATEGY_FACTORY=FixedRateStrategyFactory", + "GhoGsmSteward_Harness:FIXED_FEE_STRATEGY_FACTORY=FixedFeeStrategyFactory", ], "packages": [ "@aave/core-v3/=lib/aave-v3-core", @@ -21,13 +21,13 @@ "openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts", "solidity-utils/=lib/solidity-utils/src" ], + "build_cache": true, "optimistic_loop": true, - "prover_args": ["-depth 15","-mediumTimeout 1000","-cache none"], + "process": "emv", + "prover_args": ["-depth 15","-mediumTimeout 1000"], "smt_timeout": "2000", "solc": "solc8.10", - "verify": "GhoStewardV2_Harness:certora/steward/specs/rules.spec", - "rule": ["sanity"], - "disable_auto_cache_key_gen" :true, - "cache" :"none", - "msg": "STEWARD::sanity" + "verify": "GhoGsmSteward_Harness:certora/steward/specs/GhoGsmSteward.spec", + "rule_sanity": "basic", + "msg": "GhoGsmSteward: all rules" } \ No newline at end of file diff --git a/certora/steward/harness/GhoAaveSteward_Harness.sol b/certora/steward/harness/GhoAaveSteward_Harness.sol new file mode 100644 index 00000000..707a0476 --- /dev/null +++ b/certora/steward/harness/GhoAaveSteward_Harness.sol @@ -0,0 +1,24 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {GhoAaveSteward} from '../munged/src/contracts/misc/GhoAaveSteward.sol'; + +contract GhoAaveSteward_Harness is GhoAaveSteward { + constructor( + address owner, + address addressesProvider, + address poolDataProvider, + address ghoToken, + address riskCouncil, + BorrowRateConfig memory borrowRateConfig + ) + GhoAaveSteward( + owner, + addressesProvider, + poolDataProvider, + ghoToken, + riskCouncil, + borrowRateConfig + ) + {} +} diff --git a/certora/steward/harness/GhoCcipSteward_Harness.sol b/certora/steward/harness/GhoCcipSteward_Harness.sol new file mode 100644 index 00000000..cea98b0c --- /dev/null +++ b/certora/steward/harness/GhoCcipSteward_Harness.sol @@ -0,0 +1,19 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {GhoCcipSteward} from '../../../src/contracts/misc/GhoCcipSteward.sol'; + +contract GhoCcipSteward_Harness is GhoCcipSteward { + constructor( + address ghoToken, + address ghoTokenPool, + address riskCouncil, + bool bridgeLimitEnabled + ) GhoCcipSteward(ghoToken, ghoTokenPool, riskCouncil, bridgeLimitEnabled) {} + + function getCcipTimelocks() external view returns (CcipDebounce memory) { + return _ccipTimelocks; + } + + +} diff --git a/certora/steward/harness/GhoGsmSteward_Harness.sol b/certora/steward/harness/GhoGsmSteward_Harness.sol new file mode 100644 index 00000000..45c02b0c --- /dev/null +++ b/certora/steward/harness/GhoGsmSteward_Harness.sol @@ -0,0 +1,11 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {GhoGsmSteward} from '../../../src/contracts/misc/GhoGsmSteward.sol'; + +contract GhoGsmSteward_Harness is GhoGsmSteward { + constructor( + address fixedRateStrategyFactory, + address riskCouncil + ) GhoGsmSteward(fixedRateStrategyFactory, riskCouncil) {} +} diff --git a/certora/steward/harness/GhoStewardV2_Harness.sol b/certora/steward/harness/GhoStewardV2_Harness.sol new file mode 100644 index 00000000..54b23e14 --- /dev/null +++ b/certora/steward/harness/GhoStewardV2_Harness.sol @@ -0,0 +1,21 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {GhoStewardV2} from '../../../src/contracts/misc/GhoStewardV2.sol'; + +contract GhoStewardV2_Harness is GhoStewardV2 { + constructor( + address owner, + address addressesProvider, + address ghoToken, + address fixedRateStrategyFactory, + address riskCouncil + ) GhoStewardV2(owner, addressesProvider, ghoToken, fixedRateStrategyFactory, riskCouncil) {} + + function get_gsmFeeStrategiesByRates( + uint256 buyFee, + uint256 sellFee + ) external view returns (address) { + return _gsmFeeStrategiesByRates[buyFee][sellFee]; + } +} diff --git a/certora/steward/munged/.gitignore b/certora/steward/munged/.gitignore new file mode 100644 index 00000000..c96a04f0 --- /dev/null +++ b/certora/steward/munged/.gitignore @@ -0,0 +1,2 @@ +* +!.gitignore \ No newline at end of file diff --git a/certora/steward/specs/GhoAaveSteward.spec b/certora/steward/specs/GhoAaveSteward.spec new file mode 100644 index 00000000..15514470 --- /dev/null +++ b/certora/steward/specs/GhoAaveSteward.spec @@ -0,0 +1,258 @@ + +/*=========================================================================== + This is a specification file for the contract GhoAaveSteward. + The rules were written base on the following: + https://github.com/aave/gho-core/pull/388 + + We check the following aspects: + - Limitations due to timelocks. + - For the relevant functions, only autorized sender can call them. + - When setting new paramethers they are in the correct range. + - The new paramethers are indeed set. + =============================================================================*/ + +methods { + function _.getPool() external => NONDET; + function _.getConfiguration(address) external => NONDET; + function _.getPoolConfigurator() external => NONDET; + + function _.getBorrowCap(DataTypes.ReserveConfigurationMap memory) internal => + get_BORROW_CAP_cvl() expect uint256 ; + function _.setBorrowCap(address token, uint256 newCap) external => + set_BORROW_CAP_cvl(token,newCap) expect void ALL; + + function _.getSupplyCap(DataTypes.ReserveConfigurationMap memory) internal => + get_SUPPLY_CAP_cvl() expect uint256 ; + function _.setSupplyCap(address token, uint256 newCap) external => + set_SUPPLY_CAP_cvl(token,newCap) expect void ALL; + + function _._getInterestRatesForAsset(address) internal => + get_INTEREST_RATE_cvl() expect (uint256,uint256,uint256,uint256); + + + + function getGhoTimelocks() external returns (IGhoAaveSteward.GhoDebounce) envfree; + function GHO_BORROW_RATE_MAX() external returns uint32 envfree; + function MINIMUM_DELAY() external returns uint256 envfree; + function RISK_COUNCIL() external returns address envfree; + + function owner() external returns address envfree; +} + + +ghost uint256 BORROW_CAP { + axiom 1==1; +} +function get_BORROW_CAP_cvl() returns uint256 { + return BORROW_CAP; +} +function set_BORROW_CAP_cvl(address token, uint256 newCap) { + BORROW_CAP = newCap; +} + +ghost uint256 SUPPLY_CAP { + axiom 1==1; +} +function get_SUPPLY_CAP_cvl() returns uint256 { + return SUPPLY_CAP; +} +function set_SUPPLY_CAP_cvl(address token, uint256 newCap) { + SUPPLY_CAP = newCap; +} + + +ghost uint16 OPTIMAL_USAGE_RATIO; +ghost uint32 BASE_VARIABLE_BORROW_RATE; +ghost uint32 VARIABLE_RATE_SLOPE1; +ghost uint32 VARIABLE_RATE_SLOPE2; + +function get_INTEREST_RATE_cvl() returns (uint16, uint32, uint32, uint32) { + return (OPTIMAL_USAGE_RATIO,BASE_VARIABLE_BORROW_RATE,VARIABLE_RATE_SLOPE1,VARIABLE_RATE_SLOPE2); +} + + + + + +/* ================================================================================= + ================================================================================ + Part 1: validity of the timelocks + ================================================================================= + ==============================================================================*/ + +// FUNCTION: updateGhoBorrowRate +rule ghoBorrowRateLastUpdate__updated_only_by_updateGhoBorrowRate(method f) { + env e; calldataarg args; + + uint40 ghoBorrowRateLastUpdate_before = getGhoTimelocks().ghoBorrowRateLastUpdate; + f(e,args); + uint40 ghoBorrowRateLastUpdate_after = getGhoTimelocks().ghoBorrowRateLastUpdate; + + assert (ghoBorrowRateLastUpdate_after != ghoBorrowRateLastUpdate_before) => + f.selector == sig:updateGhoBorrowRate(uint16,uint32,uint32,uint32).selector; +} +rule updateGhoBorrowRate_update_correctly__ghoBorrowRateLastUpdate() { + env e; uint16 optimalUsageRatio; uint32 baseVariableBorrowRate; + uint32 variableRateSlope1; uint32 variableRateSlope2; + updateGhoBorrowRate(e,optimalUsageRatio, baseVariableBorrowRate, + variableRateSlope1, variableRateSlope2); + assert getGhoTimelocks().ghoBorrowRateLastUpdate == require_uint40(e.block.timestamp); +} +rule updateGhoBorrowRate_timelock() { + uint40 ghoBorrowRateLastUpdate_before = getGhoTimelocks().ghoBorrowRateLastUpdate; + env e; uint16 optimalUsageRatio; uint32 baseVariableBorrowRate; + uint32 variableRateSlope1; uint32 variableRateSlope2; + + updateGhoBorrowRate(e,optimalUsageRatio, baseVariableBorrowRate, + variableRateSlope1, variableRateSlope2); + + assert to_mathint(e.block.timestamp) > ghoBorrowRateLastUpdate_before + MINIMUM_DELAY(); +} + + +// FUNCTION: updateGhoBorrowCap +rule ghoBorrowCapLastUpdate__updated_only_by_updateGhoBorrowCap(method f) { + env e; calldataarg args; + + uint40 ghoBorrowCapLastUpdate_before = getGhoTimelocks().ghoBorrowCapLastUpdate; + f(e,args); + uint40 ghoBorrowCapLastUpdate_after = getGhoTimelocks().ghoBorrowCapLastUpdate; + + assert (ghoBorrowCapLastUpdate_after != ghoBorrowCapLastUpdate_before) => + f.selector == sig:updateGhoBorrowCap(uint256).selector; +} +rule updateGhoBorrowCap_update_correctly__ghoBorrowCapLastUpdate() { + env e; uint256 newBorrowCap; + updateGhoBorrowCap(e,newBorrowCap); + assert getGhoTimelocks().ghoBorrowCapLastUpdate == require_uint40(e.block.timestamp); +} +rule updateGhoBorrowCap_timelock() { + uint40 ghoBorrowCapLastUpdate_before = getGhoTimelocks().ghoBorrowCapLastUpdate; + env e; uint256 newBorrowCap; + updateGhoBorrowCap(e,newBorrowCap); + + assert to_mathint(e.block.timestamp) > ghoBorrowCapLastUpdate_before + MINIMUM_DELAY(); +} + + +// FUNCTION: updateGhoSupplyCap +rule ghoSupplyCapLastUpdate__updated_only_by_updateGhoSupplyCap(method f) { + env e; calldataarg args; + + uint40 ghoSupplyCapLastUpdate_before = getGhoTimelocks().ghoSupplyCapLastUpdate; + f(e,args); + uint40 ghoSupplyCapLastUpdate_after = getGhoTimelocks().ghoSupplyCapLastUpdate; + + assert (ghoSupplyCapLastUpdate_after != ghoSupplyCapLastUpdate_before) => + f.selector == sig:updateGhoSupplyCap(uint256).selector; +} +rule updateGhoSupplyCap_update_correctly__ghoSupplyCapLastUpdate() { + env e; uint256 newSupplyCap; + updateGhoSupplyCap(e,newSupplyCap); + assert getGhoTimelocks().ghoSupplyCapLastUpdate == require_uint40(e.block.timestamp); +} +rule updateGhoSupplyCap_timelock() { + uint40 ghoSupplyCapLastUpdate_before = getGhoTimelocks().ghoSupplyCapLastUpdate; + env e; uint256 newSupplyCap; + updateGhoSupplyCap(e,newSupplyCap); + + assert to_mathint(e.block.timestamp) > ghoSupplyCapLastUpdate_before + MINIMUM_DELAY(); +} + + +/* ================================================================================= + ================================================================================ + Part 2: autorized message sender + ================================================================================= + ==============================================================================*/ +rule only_RISK_COUNCIL_can_call__updateGhoBorrowCap() { + env e; uint256 newBorrowCap; + + updateGhoBorrowCap(e,newBorrowCap); + assert (e.msg.sender==RISK_COUNCIL()); +} +rule only_RISK_COUNCIL_can_call__updateGhoBorrowRate() { + env e; uint16 optimalUsageRatio; uint32 baseVariableBorrowRate; + uint32 variableRateSlope1; uint32 variableRateSlope2; + + updateGhoBorrowRate(e,optimalUsageRatio, baseVariableBorrowRate, + variableRateSlope1, variableRateSlope2); + assert (e.msg.sender==RISK_COUNCIL()); +} +rule only_RISK_COUNCIL_can_call__updateGhoSupplyCap() { + env e; uint256 newSupplyCap; + + updateGhoSupplyCap(e,newSupplyCap); + assert (e.msg.sender==RISK_COUNCIL()); +} +rule only_owner_can_call__setBorrowRateConfig() { + env e; + uint16 optimalUsageRatioMaxChange; + uint32 baseVariableBorrowRateMaxChange; + uint32 variableRateSlope1MaxChange; + uint32 variableRateSlope2MaxChange; + + setBorrowRateConfig(e,optimalUsageRatioMaxChange, baseVariableBorrowRateMaxChange, variableRateSlope1MaxChange, variableRateSlope2MaxChange); + assert (e.msg.sender==owner()); +} + + + +/* ================================================================================= + ================================================================================ + Part 3: correctness of the main functions. + We check the validity of the new paramethers values, and that are indeed set. + ================================================================================= + ==============================================================================*/ +rule updateGhoBorrowCap__correctness() { + env e; uint256 newBorrowCap; + uint256 borrow_cap_before = BORROW_CAP; + updateGhoBorrowCap(e,newBorrowCap); + assert BORROW_CAP==newBorrowCap; + + uint256 borrow_cap_after = BORROW_CAP; + assert to_mathint(borrow_cap_after) <= 2*borrow_cap_before; +} + +rule updateGhoSupplyCap__correctness() { + env e; uint256 newSupplyCap; + uint256 supply_cap_before = SUPPLY_CAP; + updateGhoSupplyCap(e,newSupplyCap); + assert SUPPLY_CAP==newSupplyCap; + + uint256 supply_cap_after = SUPPLY_CAP; + assert to_mathint(supply_cap_after) <= 2*supply_cap_before; +} + + +rule updateGhoBorrowRate__correctness() { + env e; uint16 optimalUsageRatio; uint32 baseVariableBorrowRate; + uint32 variableRateSlope1; uint32 variableRateSlope2; + + uint16 optimalUsageRatio_before = OPTIMAL_USAGE_RATIO; + uint32 baseVariableBorrowRate_before = BASE_VARIABLE_BORROW_RATE; + uint32 variableRateSlope1_before = VARIABLE_RATE_SLOPE1; + uint32 variableRateSlope2_before = VARIABLE_RATE_SLOPE2; + + updateGhoBorrowRate(e,optimalUsageRatio, baseVariableBorrowRate, variableRateSlope1, variableRateSlope2); + + + assert baseVariableBorrowRate + variableRateSlope1 + variableRateSlope2 <= to_mathint(GHO_BORROW_RATE_MAX()); +} + + + + + + + +/* ================================================================================= + Rule: sanity. + Status: PASS. + ================================================================================*/ +rule sanity(method f) { + env e; + calldataarg args; + f(e,args); + satisfy true; +} diff --git a/certora/steward/specs/GhoBucketSteward.spec b/certora/steward/specs/GhoBucketSteward.spec new file mode 100644 index 00000000..996945dc --- /dev/null +++ b/certora/steward/specs/GhoBucketSteward.spec @@ -0,0 +1,137 @@ +//using FixedRateStrategyFactory as FAC; + + +/*=========================================================================== + This is a specification file for the contract GhoStewardV2. + The rules were written base on the following: + https://github.com/aave/gho-core/pull/388 + + We check the following aspects: + - Limitations due to timelocks. + - For the relevant functions, only autorized sender can call them. + - When setting new paramethers they are in the correct range. + - The new paramethers are indeed set. + =============================================================================*/ + +methods { + function _.getPool() external => NONDET; + function _.getConfiguration(address) external => NONDET; + function _.getPoolConfigurator() external => NONDET; + + function _.getFacilitatorBucket(address facilitator) external => + get_BUCKET_CAPACITY_cvl() expect (uint256,uint256); + function _.setFacilitatorBucketCapacity(address,uint128 newBucketCapacity) external => + set_BUCKET_CAPACITY_cvl(newBucketCapacity) expect void; + + function owner() external returns (address) envfree; + function getFacilitatorBucketCapacityTimelock(address) external returns (uint40) envfree; + function MINIMUM_DELAY() external returns uint256 envfree; + function RISK_COUNCIL() external returns address envfree; +} + + + +ghost uint128 BUCKET_CAPACITY; +function get_BUCKET_CAPACITY_cvl() returns (uint256,uint256) { + uint256 ret; + return (BUCKET_CAPACITY,ret); +} +function set_BUCKET_CAPACITY_cvl(uint128 newBucketCapacity) { + BUCKET_CAPACITY = newBucketCapacity; +} + + + + +/* ================================================================================= + ================================================================================ + Part 1: validity of the timelocks + ================================================================================= + ==============================================================================*/ + +// FUNCTION: updateFacilitatorBucketCapacity +rule timestamp__updated_only_by_updateFacilitatorBucketCapacity(method f) { + env e; calldataarg args; + address facilitator; + + uint40 timestamp_before = getFacilitatorBucketCapacityTimelock(facilitator); + f(e,args); + uint40 timestamp_after = getFacilitatorBucketCapacityTimelock(facilitator); + + assert (timestamp_before != timestamp_after) => + f.selector == sig:updateFacilitatorBucketCapacity(address,uint128).selector; +} + +rule updateFacilitatorBucketCapacity_update_correctly__timestamp() { + env e; address facilitator; uint128 newBucketCapacity; + updateFacilitatorBucketCapacity(e,facilitator,newBucketCapacity); + assert getFacilitatorBucketCapacityTimelock(facilitator) == require_uint40(e.block.timestamp); +} + +rule updateFacilitatorBucketCapacity_timelock() { + env e; address facilitator; uint128 newBucketCapacity; + uint40 timestamp_before = getFacilitatorBucketCapacityTimelock(facilitator); + updateFacilitatorBucketCapacity(e,facilitator, newBucketCapacity); + + assert to_mathint(e.block.timestamp) > timestamp_before + MINIMUM_DELAY(); +} + + + + + + +/* ================================================================================= + ================================================================================ + Part 2: autorized message sender + ================================================================================= + ==============================================================================*/ +rule only_RISK_COUNCIL_can_call__updateFacilitatorBucketCapacity() { + env e; address facilitator; uint128 newBucketCapacity; + + updateFacilitatorBucketCapacity(e,facilitator,newBucketCapacity); + assert (e.msg.sender==RISK_COUNCIL()); +} +rule only_owner_can_call__setControlledFacilitator() { + env e; + address[] facilitatorList; + bool approve; + + setControlledFacilitator(e,facilitatorList,approve); + assert (e.msg.sender==owner()); +} + + + +/* ================================================================================= + ================================================================================ + Part 3: correctness of the main functions. + We check the validity of the new paramethers values, and that are indeed set. + ================================================================================= + ==============================================================================*/ + +rule updateFacilitatorBucketCapacity__correctness() { + env e; address facilitator; uint128 newBucketCapacity; + + uint256 bucket_capacity_before = BUCKET_CAPACITY; + updateFacilitatorBucketCapacity(e,facilitator,newBucketCapacity); + assert BUCKET_CAPACITY==newBucketCapacity; + + assert to_mathint(BUCKET_CAPACITY) <= 2*bucket_capacity_before; +} + + + + + + +/* ================================================================================= + Rule: sanity. + Status: PASS. + ================================================================================*/ +rule sanity(method f) { + env e; + calldataarg args; + f(e,args); + satisfy true; +} diff --git a/certora/steward/specs/GhoCcipSteward.spec b/certora/steward/specs/GhoCcipSteward.spec new file mode 100644 index 00000000..ccfaf076 --- /dev/null +++ b/certora/steward/specs/GhoCcipSteward.spec @@ -0,0 +1,214 @@ +//using FixedFeeStrategyFactory as FAC; + + +/*=========================================================================== + This is a specification file for the contract GhoStewardV2. + The rules were written base on the following: + https://github.com/aave/gho-core/pull/388 + + We check the following aspects: + - Limitations due to timelocks. + - For the relevant functions, only autorized sender can call them. + - When setting new paramethers they are in the correct range. + - The new paramethers are indeed set. + =============================================================================*/ + +methods { + function _.getPool() external => NONDET; + function _.getConfiguration(address) external => NONDET; + function _.getPoolConfigurator() external => NONDET; + + + function _.getCurrentOutboundRateLimiterState(uint64 remoteCS) external + => OutboundRate(remoteCS) expect RateLimiter.TokenBucket; + + function _.getCurrentInboundRateLimiterState(uint64 remoteCS) external + => InboundRate(remoteCS) expect RateLimiter.TokenBucket; + + function _.setChainRateLimiterConfig(uint64,RateLimiter.Config,RateLimiter.Config) + external => NONDET; + + function getCcipTimelocks() external returns (IGhoCcipSteward.CcipDebounce) envfree; + function MINIMUM_DELAY() external returns uint256 envfree; + function RISK_COUNCIL() external returns address envfree; +} + + +ghost uint128 CAPACITY_OUT; +ghost uint128 RATE_OUT; +function OutboundRate(uint64 remoteCS) returns RateLimiter.TokenBucket { + RateLimiter.TokenBucket ret; + + require ret.capacity == CAPACITY_OUT; + require ret.rate == RATE_OUT; + + return ret; +} + +ghost uint128 CAPACITY_IN; +ghost uint128 RATE_IN; +function InboundRate(uint64 remoteCS) returns RateLimiter.TokenBucket { + RateLimiter.TokenBucket ret; + + require ret.capacity == CAPACITY_IN; + require ret.rate == RATE_IN; + + return ret; +} + + + + + +ghost uint128 BUY_FEE { + axiom 1==1; +} +function get_BUY_FEE_cvl() returns uint128 { + return BUY_FEE; +} +ghost uint128 SELL_FEE { + axiom 1==1; +} +function get_SELL_FEE_cvl() returns uint128 { + return SELL_FEE; +} +ghost address FEE_STRATEGY { + axiom 1==1; +} +function set_FEE_STRATEGY(address strategy) { + FEE_STRATEGY = strategy; +} + + + +/* ================================================================================= + ================================================================================ + Part 1: validity of the timelocks + ================================================================================= + ==============================================================================*/ + +// FUNCTION: updateBridgeLimit +rule bridgeLimitLastUpdate__updated_only_by_updateBridgeLimit(method f) { + env e; calldataarg args; + + uint40 bridgeLimitLastUpdate_before = getCcipTimelocks().bridgeLimitLastUpdate; + f(e,args); + uint40 bridgeLimitLastUpdate_after = getCcipTimelocks().bridgeLimitLastUpdate; + + assert (bridgeLimitLastUpdate_before != bridgeLimitLastUpdate_after) => + f.selector == sig:updateBridgeLimit(uint256).selector; +} + +rule updateBridgeLimit_update_correctly__bridgeLimitLastUpdate() { + env e; uint256 newBridgeLimit; + updateBridgeLimit(e,newBridgeLimit); + assert getCcipTimelocks().bridgeLimitLastUpdate == require_uint40(e.block.timestamp); +} + +rule updateBridgeLimit_timelock() { + env e; uint128 newBridgeLimit; + uint40 before = getCcipTimelocks().bridgeLimitLastUpdate; + updateBridgeLimit(e,newBridgeLimit); + + assert to_mathint(e.block.timestamp) > before + MINIMUM_DELAY(); +} + + + +// FUNCTION: updateRateLimit +rule rateLimitLastUpdate__updated_only_by_updateRateLimit(method f) { + env e; calldataarg args; + + uint40 before = getCcipTimelocks().rateLimitLastUpdate; + f(e,args); + uint40 after = getCcipTimelocks().rateLimitLastUpdate; + + assert (before != after) => + f.selector == sig:updateRateLimit(uint64,bool,uint128,uint128,bool,uint128,uint128).selector; +} + +rule updateRateLimit_update_correctly__rateLimitLastUpdate() { + env e; calldataarg args; + updateRateLimit(e,args); + assert getCcipTimelocks().rateLimitLastUpdate == require_uint40(e.block.timestamp); +} + +rule updateRateLimit_timelock() { + env e; calldataarg args; + uint40 before = getCcipTimelocks().rateLimitLastUpdate; + updateRateLimit(e,args); + + assert to_mathint(e.block.timestamp) > before + MINIMUM_DELAY(); +} + + + + + +/* ================================================================================= + ================================================================================ + Part 2: autorized message sender + ================================================================================= + ==============================================================================*/ + +rule only_RISK_COUNCIL_can_call__updateBridgeLimit() { + env e; calldataarg args; + + updateBridgeLimit(e,args); + assert (e.msg.sender==RISK_COUNCIL()); +} + +rule only_RISK_COUNCIL_can_call__updateRateLimit() { + env e; calldataarg args; + + updateRateLimit(e,args); + assert (e.msg.sender==RISK_COUNCIL()); +} + + + +/* ================================================================================= + ================================================================================ + Part 3: correctness of the main functions. + We check the validity of the new paramethers values. + ================================================================================= + ==============================================================================*/ + +rule updateBridgeLimit__correctness() { + env e; + + uint64 remoteChainSelector; + bool outboundEnabled; + uint128 outboundCapacity; + uint128 outboundRate; + bool inboundEnabled; + uint128 inboundCapacity; + uint128 inboundRate; + + updateRateLimit(e, remoteChainSelector, + outboundEnabled, outboundCapacity, outboundRate, + inboundEnabled, inboundCapacity, inboundRate); + + assert to_mathint(outboundCapacity) <= 2*CAPACITY_OUT; + assert to_mathint(outboundRate) <= 2*RATE_OUT; + + assert to_mathint(inboundCapacity) <= 2*CAPACITY_IN; + assert to_mathint(inboundRate) <= 2*RATE_IN; +} + + + + + + + +/* ================================================================================= + Rule: sanity. + Status: PASS. + ================================================================================*/ +rule sanity(method f) { + env e; + calldataarg args; + f(e,args); + satisfy true; +} diff --git a/certora/steward/specs/rules.spec b/certora/steward/specs/GhoGsmSteward.spec similarity index 56% rename from certora/steward/specs/rules.spec rename to certora/steward/specs/GhoGsmSteward.spec index 7a49ab70..caf84390 100644 --- a/certora/steward/specs/rules.spec +++ b/certora/steward/specs/GhoGsmSteward.spec @@ -1,4 +1,4 @@ -using FixedRateStrategyFactory as FAC; +using FixedFeeStrategyFactory as FAC; /*=========================================================================== @@ -18,16 +18,6 @@ methods { function _.getConfiguration(address) external => NONDET; function _.getPoolConfigurator() external => NONDET; - function _.getBorrowCap(DataTypes.ReserveConfigurationMap memory) internal => - get_BORROW_CAP_cvl() expect uint256 ; - function _.setBorrowCap(address token, uint256 newCap) external => - set_BORROW_CAP_cvl(token,newCap) expect void ALL; - - function _.getBaseVariableBorrowRate() external => - get_BORROW_RATE_cvl() expect uint256; - function _.setReserveInterestRateStrategyAddress(address,address strategy) external => - set_STRATEGY(strategy) expect void ALL; - function _.getExposureCap() external => get_EXPOSURE_CAP_cvl() expect uint256 ; function _.updateExposureCap(uint128 newCap) external => set_EXPOSURE_CAP_cvl(newCap) expect void ALL; @@ -35,44 +25,14 @@ methods { function _.getBuyFee(uint256) external => get_BUY_FEE_cvl() expect uint256; function _.getSellFee(uint256) external => get_SELL_FEE_cvl() expect uint256; function _.updateFeeStrategy(address strategy) external => - set_FEE_STRATEGY(strategy) expect void ALL; + set_FEE_STRATEGY(strategy) expect void ALL; - function owner() external returns (address) envfree; - function getGhoTimelocks() external returns (IGhoStewardV2.GhoDebounce) envfree; - function getGsmTimelocks(address) external returns (IGhoStewardV2.GsmDebounce) envfree; - function GHO_BORROW_RATE_CHANGE_MAX() external returns uint256 envfree; + function getGsmTimelocks(address) external returns (IGhoGsmSteward.GsmDebounce) envfree; function GSM_FEE_RATE_CHANGE_MAX() external returns uint256 envfree; - function GHO_BORROW_RATE_MAX() external returns uint256 envfree; function MINIMUM_DELAY() external returns uint256 envfree; function RISK_COUNCIL() external returns address envfree; - function FAC.getStrategyByRate(uint256) external returns (address) envfree; - function get_gsmFeeStrategiesByRates(uint256,uint256) external returns(address) envfree; -} - - -ghost uint256 BORROW_CAP { - axiom 1==1; -} -function get_BORROW_CAP_cvl() returns uint256 { - return BORROW_CAP; -} -function set_BORROW_CAP_cvl(address token, uint256 newCap) { - BORROW_CAP = newCap; -} - -ghost uint256 BORROW_RATE { - axiom BORROW_RATE <= 10^27; -} -function get_BORROW_RATE_cvl() returns uint256 { - return BORROW_RATE; -} - -ghost address STRATEGY { - axiom 1==1; -} -function set_STRATEGY(address strategy) { - STRATEGY = strategy; + function FAC.getFixedFeeStrategy(uint256 buyFee, uint256 sellFee) external returns (address) envfree; } @@ -115,61 +75,6 @@ function set_FEE_STRATEGY(address strategy) { ================================================================================= ==============================================================================*/ -// FUNCTION: updateGhoBorrowCap -rule ghoBorrowCapLastUpdate__updated_only_by_updateGhoBorrowCap(method f) { - env e; calldataarg args; - - uint40 ghoBorrowCapLastUpdate_before = getGhoTimelocks().ghoBorrowCapLastUpdate; - f(e,args); - uint40 ghoBorrowCapLastUpdate_after = getGhoTimelocks().ghoBorrowCapLastUpdate; - - assert (ghoBorrowCapLastUpdate_after != ghoBorrowCapLastUpdate_before) => - f.selector == sig:updateGhoBorrowCap(uint256).selector; -} - -rule updateGhoBorrowCap_update_correctly__ghoBorrowCapLastUpdate() { - env e; uint256 newBorrowCap; - updateGhoBorrowCap(e,newBorrowCap); - assert getGhoTimelocks().ghoBorrowCapLastUpdate == require_uint40(e.block.timestamp); -} - -rule updateGhoBorrowCap_timelock() { - uint40 ghoBorrowCapLastUpdate_before = getGhoTimelocks().ghoBorrowCapLastUpdate; - env e; uint256 newBorrowCap; - updateGhoBorrowCap(e,newBorrowCap); - - assert to_mathint(e.block.timestamp) > ghoBorrowCapLastUpdate_before + MINIMUM_DELAY(); -} - - -// FUNCTION: updateGhoBorrowRate -rule ghoBorrowRateLastUpdate__updated_only_by_updateGhoBorrowRate(method f) { - env e; calldataarg args; - - uint40 ghoBorrowRateLastUpdate_before = getGhoTimelocks().ghoBorrowRateLastUpdate; - f(e,args); - uint40 ghoBorrowRateLastUpdate_after = getGhoTimelocks().ghoBorrowRateLastUpdate; - - assert (ghoBorrowRateLastUpdate_after != ghoBorrowRateLastUpdate_before) => - f.selector == sig:updateGhoBorrowRate(uint256).selector; -} - -rule updateGhoBorrowRate_update_correctly__ghoBorrowRateLastUpdate() { - env e; uint256 newBorrowRate; - updateGhoBorrowRate(e,newBorrowRate); - assert getGhoTimelocks().ghoBorrowRateLastUpdate == require_uint40(e.block.timestamp); -} - -rule updateGhoBorrowRate_timelock() { - uint40 ghoBorrowRateLastUpdate_before = getGhoTimelocks().ghoBorrowRateLastUpdate; - env e; uint256 newBorrowRate; - updateGhoBorrowRate(e,newBorrowRate); - - assert to_mathint(e.block.timestamp) > ghoBorrowRateLastUpdate_before + MINIMUM_DELAY(); -} - - - // FUNCTION: updateGsmExposureCap rule gsmExposureCapLastUpdated__updated_only_by_updateGsmExposureCap(method f) { env e; calldataarg args; @@ -234,24 +139,6 @@ rule updateGsmBuySellFees_timelock() { Part 2: autorized message sender ================================================================================= ==============================================================================*/ -rule only_RISK_COUNCIL_can_call__updateFacilitatorBucketCapacity() { - env e; address facilitator; uint128 newBucketCapacity; - - updateFacilitatorBucketCapacity(e,facilitator,newBucketCapacity); - assert (e.msg.sender==RISK_COUNCIL()); -} -rule only_RISK_COUNCIL_can_call__updateGhoBorrowCap() { - env e; uint256 newBorrowCap; - - updateGhoBorrowCap(e,newBorrowCap); - assert (e.msg.sender==RISK_COUNCIL()); -} -rule only_RISK_COUNCIL_can_call__updateGhoBorrowRate() { - env e; uint256 newBorrowRate; - - updateGhoBorrowRate(e,newBorrowRate); - assert (e.msg.sender==RISK_COUNCIL()); -} rule only_RISK_COUNCIL_can_call__updateGsmExposureCap() { env e; address gsm; uint128 newExposureCap; @@ -261,18 +148,9 @@ rule only_RISK_COUNCIL_can_call__updateGsmExposureCap() { rule only_RISK_COUNCIL_can_call__updateGsmBuySellFees() { env e; address gsm; uint256 buyFee; uint256 sellFee; - updateGsmBuySellFees(e,gsm,buyFee,sellFee); assert (e.msg.sender==RISK_COUNCIL()); } -rule only_owner_can_call__setControlledFacilitator() { - env e; - address[] facilitatorList; - bool approve; - - setControlledFacilitator(e,facilitatorList,approve); - assert (e.msg.sender==owner()); -} @@ -282,30 +160,6 @@ rule only_owner_can_call__setControlledFacilitator() { We check the validity of the new paramethers values, and that are indeed set. ================================================================================= ==============================================================================*/ -rule updateGhoBorrowCap__correctness() { - env e; uint256 newBorrowCap; - uint256 borrow_cap_before = BORROW_CAP; - updateGhoBorrowCap(e,newBorrowCap); - assert BORROW_CAP==newBorrowCap; - - uint256 borrow_cap_after = BORROW_CAP; - assert to_mathint(borrow_cap_after) <= 2*borrow_cap_before; -} - - -rule updateGhoBorrowRate__correctness() { - env e; uint256 newBorrowRate; - uint256 borrow_rate_before = BORROW_RATE; - updateGhoBorrowRate(e,newBorrowRate); - assert FAC.getStrategyByRate(newBorrowRate) == STRATEGY; - - assert (borrow_rate_before-GHO_BORROW_RATE_CHANGE_MAX() <= to_mathint(newBorrowRate) - && - to_mathint(newBorrowRate) <= borrow_rate_before+GHO_BORROW_RATE_CHANGE_MAX()); - assert (newBorrowRate <= GHO_BORROW_RATE_MAX()); -} - - rule updateGsmExposureCap__correctness() { env e; address gsm; uint128 newExposureCap; uint128 exposure_cap_before = EXPOSURE_CAP; @@ -322,7 +176,7 @@ rule updateGsmBuySellFees__correctness() { uint256 buyFee_before = BUY_FEE; uint256 sellFee_before = SELL_FEE; updateGsmBuySellFees(e,gsm,buyFee,sellFee); - assert get_gsmFeeStrategiesByRates(buyFee,sellFee)==FEE_STRATEGY; + assert FAC.getFixedFeeStrategy(buyFee,sellFee)==FEE_STRATEGY; assert to_mathint(buyFee) <= buyFee_before + GSM_FEE_RATE_CHANGE_MAX(); assert to_mathint(sellFee) <= sellFee_before + GSM_FEE_RATE_CHANGE_MAX();