Skip to content

Commit

Permalink
Merge branch 'main' into feat/gsm-buidl
Browse files Browse the repository at this point in the history
  • Loading branch information
yan-man committed Sep 18, 2024
2 parents 8a47c39 + facd478 commit 6e208a2
Show file tree
Hide file tree
Showing 61 changed files with 5,994 additions and 2,543 deletions.
9 changes: 8 additions & 1 deletion .github/workflows/certora-steward.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -48,4 +52,7 @@ jobs:
max-parallel: 16
matrix:
rule:
- rules.conf
- GhoAaveSteward.conf
- GhoBucketSteward.conf
- GhoCcipSteward.conf
- GhoGsmSteward.conf
2 changes: 2 additions & 0 deletions .github/workflows/node.js.yml
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@ jobs:
env:
ALCHEMY_KEY: '${{secrets.ALCHEMY_KEY}}'
ETH_RPC_URL: 'https://eth-mainnet.g.alchemy.com/v2/${{secrets.ALCHEMY_KEY}}'
RPC_MAINNET: 'https://eth-mainnet.g.alchemy.com/v2/${{secrets.ALCHEMY_KEY}}'
RPC_ARBITRUM: 'https://arb-mainnet.g.alchemy.com/v2/${{secrets.ALCHEMY_KEY}}'
strategy:
matrix:
node-version:
Expand Down
1 change: 1 addition & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ You can find all audit reports under the [audits](./audits/) folder
- [2023-12-07 - Certora Formal Verification (GHO Stability Module)](./certora/reports/Formal_Verification_Report_of_GHO_Stability_Module.pdf)
- [2024-03-14 - Certora Formal Verification (GhoStewardV2)](./audits/2024-03-14_GhoStewardV2_Certora.pdf)
- [2024-06-11 - Certora Formal Verification (UpgradeableGHO)](./audits/2024-06-11_UpgradeableGHO_Certora.pdf)
- [2024-06-11 - Certora Formal Verification (Modular Gho Stewards)](./audits/2024-09-15_ModularGhoStewards_Certora.pdf)

## Getting Started

Expand Down
Binary file added audits/2024-09-15_ModularGhoStewards_Certora.pdf
Binary file not shown.
28 changes: 28 additions & 0 deletions certora/steward/Makefile
Original file line number Diff line number Diff line change
@@ -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)

7 changes: 7 additions & 0 deletions certora/steward/applyHarness.patch
Original file line number Diff line number Diff line change
@@ -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
27 changes: 27 additions & 0 deletions certora/steward/conf/GhoAaveSteward.conf
Original file line number Diff line number Diff line change
@@ -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"
}
Original file line number Diff line number Diff line change
@@ -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",
Expand All @@ -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"
}
27 changes: 27 additions & 0 deletions certora/steward/conf/GhoCcipSteward.conf
Original file line number Diff line number Diff line change
@@ -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"
}
Original file line number Diff line number Diff line change
@@ -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",
Expand All @@ -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"
}
24 changes: 24 additions & 0 deletions certora/steward/harness/GhoAaveSteward_Harness.sol
Original file line number Diff line number Diff line change
@@ -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
)
{}
}
17 changes: 17 additions & 0 deletions certora/steward/harness/GhoCcipSteward_Harness.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
// 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;
}
}
11 changes: 11 additions & 0 deletions certora/steward/harness/GhoGsmSteward_Harness.sol
Original file line number Diff line number Diff line change
@@ -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) {}
}
2 changes: 2 additions & 0 deletions certora/steward/munged/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
*
!.gitignore
Loading

0 comments on commit 6e208a2

Please sign in to comment.