Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix: Add resolution of GHO incident for 13/11/2023 report (#374)
* fix: Fixes self-transfer case in discount token hook * test: Update Certora FV and report
- Loading branch information
1 parent
16e45f2
commit 51be447
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,59 @@ | ||
| name: certora-latest | ||
|
|
||
| on: | ||
| push: | ||
| branches: | ||
| - main | ||
| pull_request: | ||
| branches: | ||
| - main | ||
|
|
||
| workflow_dispatch: | ||
|
|
||
| jobs: | ||
| verify: | ||
| runs-on: ubuntu-latest | ||
|
|
||
| steps: | ||
| - uses: actions/checkout@v2 | ||
| with: | ||
| submodules: recursive | ||
|
|
||
| - name: Install python | ||
| uses: actions/setup-python@v2 | ||
| with: { python-version: 3.9 } | ||
|
|
||
| - name: Install java | ||
| uses: actions/setup-java@v1 | ||
| with: { java-version: '11', java-package: jre } | ||
|
|
||
| - name: Install certora cli | ||
| run: pip install certora-cli==5.0.5 | ||
|
|
||
| - name: Install solc | ||
| run: | | ||
| 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 | ||
| - name: Install node dependencies | ||
| run: | | ||
| npm i | ||
| - name: Verify rule ${{ matrix.rule }} | ||
| run: | | ||
| cd certora | ||
| touch applyHarness.patch | ||
| make munged | ||
| cd .. | ||
| echo "key length" ${#CERTORAKEY} | ||
| certoraRun certora/conf/${{ matrix.rule }} | ||
| env: | ||
| CERTORAKEY: ${{ secrets.CERTORAKEY }} | ||
|
|
||
| strategy: | ||
| fail-fast: false | ||
| max-parallel: 16 | ||
| matrix: | ||
| rule: | ||
| - verifyGhoVariableDebtToken_specialBranch.conf --rule sendersDiscountPercentCannotIncrease |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| { | ||
| "files": [ | ||
| "certora/munged/contracts/facilitators/flashMinter/GhoFlashMinter.sol:GhoFlashMinter", | ||
| "certora/munged/contracts/facilitators/aave/tokens/GhoAToken.sol:GhoAToken", | ||
| "certora/munged/contracts/gho/GhoToken.sol", | ||
| "certora/harness/MockFlashBorrower.sol" | ||
| ], | ||
| "link": [ | ||
| "MockFlashBorrower:Gho=GhoToken", | ||
| "MockFlashBorrower:AGho=GhoAToken", | ||
| "GhoFlashMinter:GHO_TOKEN=GhoToken", | ||
| "MockFlashBorrower:minter=GhoFlashMinter" | ||
| ], | ||
| "msg": "flashMinter check, all rules", | ||
| "optimistic_loop": true, | ||
| "process": "emv", | ||
| "prover_args": [ | ||
| " -contractRecursionLimit 1" | ||
| ], | ||
| "solc": "solc8.10", | ||
| "verify": "GhoFlashMinter:certora/specs/flashMinter.spec" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,20 @@ | ||
| { | ||
| "files": [ | ||
| "certora/munged/contracts/facilitators/aave/tokens/GhoAToken.sol", | ||
| "certora/munged/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol", | ||
| "certora/munged/contracts/gho/GhoToken.sol", | ||
| "certora/harness/GhoTokenHarness.sol", | ||
| "certora/harness/DummyERC20A.sol", | ||
| "certora/harness/DummyERC20B.sol" | ||
| ], | ||
| "link": [ | ||
| "GhoAToken:_ghoVariableDebtToken=GhoVariableDebtToken", | ||
| "GhoVariableDebtToken:_ghoAToken=GhoAToken", | ||
| "GhoAToken:_underlyingAsset=GhoTokenHarness" | ||
| ], | ||
| "msg": "GhoAToken, all rules", | ||
| "optimistic_loop": true, | ||
| "process": "emv", | ||
| "solc": "solc8.10", | ||
| "verify": "GhoAToken:certora/specs/ghoAToken.spec" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,15 @@ | ||
| { | ||
| "files": [ | ||
| "certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStrategyHarness" | ||
| ], | ||
| "loop_iter": "2", | ||
| "msg": "GhoDiscountRateStrategy, all rules.", | ||
| "optimistic_loop": true, | ||
| "process": "emv", | ||
| "prover_args": [ | ||
| " -mediumTimeout 20 -depth 10" | ||
| ], | ||
| "smt_timeout": "500", | ||
| "solc": "solc8.10", | ||
| "verify": "GhoDiscountRateStrategyHarness:certora/specs/ghoDiscountRateStrategy.spec" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,12 @@ | ||
| { | ||
| "files": [ | ||
| "certora/harness/GhoTokenHarness.sol:GhoTokenHarness", | ||
| "certora/munged/contracts/gho/GhoToken.sol" | ||
| ], | ||
| "loop_iter": "3", | ||
| "msg": "GhoToken, all rules.", | ||
| "optimistic_loop": true, | ||
| "process": "emv", | ||
| "solc": "solc8.10", | ||
| "verify": "GhoTokenHarness:certora/specs/ghoToken.spec" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,26 @@ | ||
| { | ||
| "files": [ | ||
| "certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenHarness", | ||
| "certora/harness/DummyPool.sol", | ||
| "certora/harness/DummyERC20WithTimedBalanceOf.sol", | ||
| "certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol", | ||
| "certora/harness/DummyERC20A.sol", | ||
| "certora/harness/DummyERC20B.sol" | ||
| ], | ||
| "link": [ | ||
| "GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf", | ||
| "GhoVariableDebtTokenHarness:POOL=DummyPool", | ||
| "GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy" | ||
| ], | ||
| "loop_iter": "2", | ||
| "msg": " ", | ||
| "multi_assert_check": true, | ||
| "optimistic_loop": true, | ||
| "process": "emv", | ||
| "prover_args": [ | ||
| " -mediumTimeout 30 -depth 15" | ||
| ], | ||
| "smt_timeout": "900", | ||
| "solc": "solc8.10", | ||
| "verify": "GhoVariableDebtTokenHarness:certora/specs/ghoVariableDebtToken-rayMulDiv-summarization.spec" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,25 @@ | ||
| { | ||
| "files": [ | ||
| "certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenHarness", | ||
| "certora/harness/DummyPool.sol", | ||
| "certora/harness/DummyERC20WithTimedBalanceOf.sol", | ||
| "certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol", | ||
| "certora/harness/DummyERC20A.sol", | ||
| "certora/harness/DummyERC20B.sol" | ||
| ], | ||
| "link": [ | ||
| "GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy", | ||
| "GhoVariableDebtTokenHarness:POOL=DummyPool", | ||
| "GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf" | ||
| ], | ||
| "loop_iter": "2", | ||
| "msg": "GhoVariableDebtToken", | ||
| "optimistic_loop": true, | ||
| "process": "emv", | ||
| "prover_args": [ | ||
| " -mediumTimeout 30 -depth 15" | ||
| ], | ||
| "smt_timeout": "900", | ||
| "solc": "solc8.10", | ||
| "verify": "GhoVariableDebtTokenHarness:certora/specs/ghoVariableDebtToken.spec" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,16 @@ | ||
| { | ||
| "files": [ | ||
| "certora/harness/ghoVariableDebtTokenHarnessInternal.sol:GhoVariableDebtTokenHarnessInternal", | ||
| "certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol" | ||
| ], | ||
| "loop_iter": "2", | ||
| "msg": "GhoVariableDebtToken internal functions", | ||
| "optimistic_loop": true, | ||
| "process": "emv", | ||
| "prover_args": [ | ||
| " -mediumTimeout 30 -depth 15" | ||
| ], | ||
| "smt_timeout": "900", | ||
| "solc": "solc8.10", | ||
| "verify": "GhoVariableDebtTokenHarnessInternal:certora/specs/ghoVariableDebtTokenInternal.spec" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,25 @@ | ||
| { | ||
| "files": [ | ||
| "certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenHarness", | ||
| "certora/harness/DummyPool.sol", | ||
| "certora/harness/DummyERC20WithTimedBalanceOf.sol", | ||
| "certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol", | ||
| "certora/harness/DummyERC20A.sol", | ||
| "certora/harness/DummyERC20B.sol" | ||
| ], | ||
| "link": [ | ||
| "GhoVariableDebtTokenHarness:POOL=DummyPool", | ||
| "GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf", | ||
| "GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy" | ||
| ], | ||
| "loop_iter": "2", | ||
| "msg": "GhoVariableDebtToken", | ||
| "optimistic_loop": true, | ||
| "process": "emv", | ||
| "prover_args": [ | ||
| " -depth 0 -adaptiveSolverConfig false -smt_nonLinearArithmetic true" | ||
| ], | ||
| "prover_version": "shelly/z3-4-12-3-build", | ||
| "solc": "solc8.10", | ||
| "verify": "GhoVariableDebtTokenHarness:certora/specs/ghoVariableDebtToken.spec" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,25 @@ | ||
| { | ||
| "files": [ | ||
| "certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenHarness", | ||
| "certora/harness/DummyPool.sol", | ||
| "certora/harness/DummyERC20WithTimedBalanceOf.sol", | ||
| "certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol", | ||
| "certora/harness/DummyERC20A.sol", | ||
| "certora/harness/DummyERC20B.sol" | ||
| ], | ||
| "link": [ | ||
| "GhoVariableDebtTokenHarness:POOL=DummyPool", | ||
| "GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf", | ||
| "GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy" | ||
| ], | ||
| "loop_iter": "2", | ||
| "msg": "GhoVariableDebtToken", | ||
| "optimistic_loop": true, | ||
| "process": "emv", | ||
| "prover_args": [ | ||
| " -mediumTimeout 30 -depth 15" | ||
| ], | ||
| "smt_timeout": "900", | ||
| "solc": "solc8.10", | ||
| "verify": "GhoVariableDebtTokenHarness:certora/specs/ghoVariableDebtToken_summarized.spec" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,20 @@ | ||
| pragma solidity 0.8.10; | ||
|
|
||
| import {GhoVariableDebtTokenHarness} from './ghoVariableDebtTokenHarness.sol'; | ||
| import {GhoVariableDebtToken} from '../munged/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol'; | ||
| import {IPool} from '@aave/core-v3/contracts/interfaces/IPool.sol'; | ||
|
|
||
| contract GhoVariableDebtTokenHarnessInternal is GhoVariableDebtTokenHarness { | ||
| constructor(IPool pool) public GhoVariableDebtTokenHarness(pool) { | ||
| //nop | ||
| } | ||
|
|
||
| function accrueDebtOnAction( | ||
| address user, | ||
| uint256 previousScaledBalance, | ||
| uint256 discountPercent, | ||
| uint256 index | ||
| ) external returns (uint256, uint256) { | ||
| return _accrueDebtOnAction(user, previousScaledBalance, discountPercent, index); | ||
| } | ||
| } |
Binary file not shown.
Oops, something went wrong.
GrayFieth#