Skip to content

Commit 95d1cc3

Browse files
sakulstrasakulstra
authored
Merge pull request #129 from bgd-labs/v3.4.0
V3.4.0
2 parents 496c6ea + 2f25963 commit 95d1cc3

File tree

267 files changed

+12282
-5720
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

267 files changed

+12282
-5720
lines changed

‎.changeset/tricky-doodles-knock.md‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
---
2+
"@aave-dao/aave-v3-origin": minor
3+
---
4+
5+
Release of Aave v3.4.0

‎.github/workflows/certora-ATokenWithDelegation.yml‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
name: certora-ATokenWithDelegation
2+
3+
concurrency:
4+
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
5+
cancel-in-progress: true
6+
7+
on:
8+
pull_request:
9+
branches:
10+
- main
11+
- certora
12+
push:
13+
branches:
14+
- main
15+
16+
workflow_dispatch:
17+
18+
jobs:
19+
verify:
20+
runs-on: ubuntu-latest
21+
if:
22+
github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' &&
23+
github.ref == format('refs/heads/{0}', github.event.repository.default_branch))
24+
permissions:
25+
contents: read
26+
statuses: write
27+
pull-requests: write
28+
steps:
29+
- uses: actions/checkout@v4
30+
with:
31+
submodules: recursive
32+
33+
- name: Munged
34+
run: |
35+
cd certora/atoken-with-delegation
36+
touch applyHarness.patch
37+
make munged
38+
39+
- uses: Certora/certora-run-action@v1
40+
with:
41+
cli-version: 7.28.0
42+
configurations: |-
43+
certora/atoken-with-delegation/conf/AToken.conf
44+
certora/atoken-with-delegation/conf/AToken-problematic-rules.conf --rule totalSupplyEqualsSumAllBalance additiveBurn additiveTransfer
45+
certora/atoken-with-delegation/conf/token-v3-general.conf
46+
certora/atoken-with-delegation/conf/token-v3-erc20.conf
47+
certora/atoken-with-delegation/conf/token-v3-delegate-basic.conf
48+
certora/atoken-with-delegation/conf/token-v3-delegate-invariants.conf --rule mirror_votingDelegatee_correct mirror_propositionDelegatee_correct mirror_delegationMode_correct mirror_balance_correct --rule_sanity "none"
49+
certora/atoken-with-delegation/conf/token-v3-delegate-invariants.conf --exclude_rule mirror_votingDelegatee_correct mirror_propositionDelegatee_correct mirror_delegationMode_correct mirror_balance_correct
50+
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule vp_change_in_balance_affect_power_DELEGATEE
51+
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule vp_change_of_balance_affect_power_NON_DELEGATEE
52+
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule pp_change_in_balance_affect_power_DELEGATEE
53+
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule pp_change_of_balance_affect_power_NON_DELEGATEE
54+
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule no_function_changes_both_balance_and_delegation_state
55+
solc-versions: 0.8.27
56+
comment-fail-only: false
57+
solc-remove-version-prefix: "0."
58+
job-name: "Certora Prover Run"
59+
certora-key: ${{ secrets.CERTORAKEY }}
60+
install-java: true
61+
env:
62+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

‎.github/workflows/certora-basic.yml‎

Lines changed: 37 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@ concurrency:
77
on:
88
pull_request:
99
branches:
10-
- certora
1110
- main
11+
- certora
1212
push:
1313
branches:
1414
- main
@@ -21,56 +21,48 @@ jobs:
2121
if:
2222
github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' &&
2323
github.ref == format('refs/heads/{0}', github.event.repository.default_branch))
24-
24+
permissions:
25+
contents: read
26+
statuses: write
27+
pull-requests: write
2528
steps:
2629
- uses: actions/checkout@v4
30+
with:
31+
submodules: recursive
2732

28-
- name: Install python
29-
uses: actions/setup-python@v5
30-
with: { python-version: 3.9 }
31-
32-
- name: Install java
33-
uses: actions/setup-java@v4
34-
with: { distribution: "zulu", java-version: "11", java-package: jre }
35-
36-
- name: Install certora cli
37-
run: pip install certora-cli==7.20.3
38-
39-
- name: Install solc
40-
run: |
41-
wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
42-
chmod +x solc-static-linux
43-
sudo mv solc-static-linux /usr/local/bin/solc8.19
44-
45-
- name: Verify rule ${{ matrix.rule }}
33+
- name: Munged
4634
run: |
4735
cd certora/basic
4836
touch applyHarness.patch
4937
make munged
50-
cd ../..
51-
echo "key length" ${#CERTORAKEY}
52-
certoraRun certora/basic/conf/${{ matrix.rule }} --wait_for_results
38+
39+
- uses: Certora/certora-run-action@v1
40+
with:
41+
cli-version: 7.28.0
42+
configurations: |-
43+
certora/basic/conf/AToken.conf
44+
certora/basic/conf/ReserveConfiguration.conf
45+
certora/basic/conf/UserConfiguration.conf
46+
certora/basic/conf/VariableDebtToken.conf
47+
certora/basic/conf/stableRemoved.conf
48+
certora/basic/conf/EModeConfiguration.conf
49+
certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve
50+
certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotDepositInFrozenReserve
51+
certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotDepositZeroAmount
52+
certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotWithdrawZeroAmount
53+
certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotWithdrawFromInactiveReserve
54+
certora/basic/conf/NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowZeroAmount
55+
certora/basic/conf/NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnInactiveReserve
56+
certora/basic/conf/NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnReserveDisabledForBorrowing
57+
certora/basic/conf/NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnFrozenReserve
58+
solc-versions: 0.8.27
59+
comment-fail-only: false
60+
solc-remove-version-prefix: "0."
61+
job-name: "Certora Prover Run"
62+
certora-key: ${{ secrets.CERTORAKEY }}
63+
install-java: true
5364
env:
54-
CERTORAKEY: ${{ secrets.CERTORAKEY }}
65+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
66+
# Put back the following rule after ticket 8889 is closed
67+
# certora/basic/conf/NEW-pool-no-summarizations.conf ##### waiting for
5568

56-
strategy:
57-
fail-fast: false
58-
max-parallel: 16
59-
matrix:
60-
rule:
61-
- AToken.conf
62-
- ReserveConfiguration.conf
63-
- UserConfiguration.conf
64-
- VariableDebtToken.conf
65-
- NEW-pool-no-summarizations.conf
66-
- stableRemoved.conf
67-
- EModeConfiguration.conf
68-
- NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve --msg "cannotDepositInInactiveReserve"
69-
- NEW-pool-simple-properties.conf --rule cannotDepositInFrozenReserve --msg "cannotDepositInFrozenReserve"
70-
- NEW-pool-simple-properties.conf --rule cannotDepositZeroAmount --msg "cannotDepositZeroAmount"
71-
- NEW-pool-simple-properties.conf --rule cannotWithdrawZeroAmount --msg "cannotWithdrawZeroAmount"
72-
- NEW-pool-simple-properties.conf --rule cannotWithdrawFromInactiveReserve --msg "cannotWithdrawFromInactiveReserve"
73-
- NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowZeroAmount --msg "cannotBorrowZeroAmount"
74-
- NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnInactiveReserve --msg "cannotBorrowOnInactiveReserve"
75-
- NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnReserveDisabledForBorrowing --msg "cannotBorrowOnReserveDisabledForBorrowing"
76-
- NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnFrozenReserve --msg "cannotBorrowOnFrozenReserve"

‎.github/workflows/certora-stata.yml‎

Lines changed: 47 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,15 @@
11
name: certora-stata
22

3+
concurrency:
4+
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
5+
cancel-in-progress: true
6+
37
on:
4-
push:
8+
pull_request:
59
branches:
610
- main
7-
pull_request:
11+
- certora
12+
push:
813
branches:
914
- main
1015

@@ -16,65 +21,53 @@ jobs:
1621
if:
1722
github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' &&
1823
github.ref == format('refs/heads/{0}', github.event.repository.default_branch))
19-
24+
permissions:
25+
contents: read
26+
statuses: write
27+
pull-requests: write
2028
steps:
2129
- uses: actions/checkout@v4
2230
with:
2331
submodules: recursive
2432

25-
- name: Install python
26-
uses: actions/setup-python@v5
27-
with: { python-version: 3.9 }
28-
29-
- name: Install java
30-
uses: actions/setup-java@v4
31-
with: { distribution: "zulu", java-version: "11", java-package: jre }
32-
33-
- name: Install certora cli
34-
run: pip install certora-cli==7.20.3
35-
- name: Install solc
36-
run: |
37-
wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux
38-
chmod +x solc-static-linux
39-
sudo mv solc-static-linux /usr/local/bin/solc8.20
40-
41-
- name: Verify rule ${{ matrix.rule }}
33+
- name: Munged
4234
run: |
4335
cd certora/stata
4436
touch applyHarness.patch
4537
make munged
46-
cd ../..
47-
certoraRun certora/stata/conf/${{ matrix.rule }}
48-
env:
49-
CERTORAKEY: ${{ secrets.CERTORAKEY }}
5038
51-
strategy:
52-
fail-fast: false
53-
max-parallel: 16
54-
matrix:
55-
rule:
56-
- verifyERC4626.conf --rule previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance previewMintIndependentOfAllowance
57-
- verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert
58-
# Timeout
59-
# - verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw
60-
- verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
61-
- verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1
62-
- verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint maxDepositConstant
63-
- verifyERC4626Extended.conf --rule redeemSum
64-
- verifyERC4626Extended.conf --rule redeemATokensSum
65-
- verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf
66-
- verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf
67-
- verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist
68-
- verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards
69-
- verifyStataToken.conf --rule totalClaimableRewards_stable
70-
- verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset
71-
- verifyStataToken.conf --rule solvency_total_asset_geq_total_supply
72-
- verifyStataToken.conf --rule singleAssetAccruedRewards
73-
- verifyStataToken.conf --rule totalAssets_stable
74-
- verifyStataToken.conf --rule getClaimableRewards_stable
75-
- verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit
76-
- verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens
77-
- verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf
78-
- verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim
79-
- verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient
80-
- verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient
39+
- uses: Certora/certora-run-action@v1
40+
with:
41+
cli-version: 7.28.0
42+
configurations: |-
43+
certora/stata/conf/verifyERC4626.conf --rule previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance previewMintIndependentOfAllowance
44+
certora/stata/conf/verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert
45+
certora/stata/conf/verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
46+
certora/stata/conf/verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1
47+
certora/stata/conf/verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint maxDepositConstant
48+
certora/stata/conf/verifyERC4626Extended.conf --rule redeemSum
49+
certora/stata/conf/verifyERC4626Extended.conf --rule redeemATokensSum
50+
certora/stata/conf/verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf
51+
certora/stata/conf/verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf
52+
certora/stata/conf/verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist
53+
certora/stata/conf/verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards
54+
certora/stata/conf/verifyStataToken.conf --rule totalClaimableRewards_stable
55+
certora/stata/conf/verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset
56+
certora/stata/conf/verifyStataToken.conf --rule solvency_total_asset_geq_total_supply
57+
certora/stata/conf/verifyStataToken.conf --rule singleAssetAccruedRewards
58+
certora/stata/conf/verifyStataToken.conf --rule totalAssets_stable
59+
certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable
60+
certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit
61+
certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens
62+
certora/stata/conf/verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf
63+
certora/stata/conf/verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim
64+
certora/stata/conf/verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient
65+
certora/stata/conf/verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient
66+
solc-versions: 0.8.27
67+
comment-fail-only: false
68+
solc-remove-version-prefix: "0."
69+
job-name: "Certora Prover Run"
70+
certora-key: ${{ secrets.CERTORAKEY }}
71+
install-java: true
72+
env:
73+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

‎.gitignore‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
# build and cache
22
cache/
33
out/
4+
zkout/
45

56
# general
67
.env
@@ -36,4 +37,5 @@ resource_errors.json
3637

3738
# invariants
3839
_corpus/
39-
crytic-export/
40+
crytic-export/
41+
slither_results.json

‎Makefile‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -43,15 +43,13 @@ git-diff :
4343

4444
# Deploy
4545
deploy-libs-one :;
46-
FOUNDRY_PROFILE=${chain} forge script scripts/misc/LibraryPreCompileOne.sol --rpc-url ${chain} --ledger --mnemonic-indexes ${MNEMONIC_INDEX} --sender ${LEDGER_SENDER} --slow --broadcast
46+
FOUNDRY_PROFILE=${chain} forge script scripts/misc/LibraryPreCompileOne.sol --rpc-url ${chain} --ledger --mnemonic-indexes ${MNEMONIC_INDEX} --sender ${LEDGER_SENDER} --slow --broadcast --verify
4747
deploy-libs-two :;
48-
FOUNDRY_PROFILE=${chain} forge script scripts/misc/LibraryPreCompileTwo.sol --rpc-url ${chain} --ledger --mnemonic-indexes ${MNEMONIC_INDEX} --sender ${LEDGER_SENDER} --slow --broadcast
48+
FOUNDRY_PROFILE=${chain} forge script scripts/misc/LibraryPreCompileTwo.sol --rpc-url ${chain} --ledger --mnemonic-indexes ${MNEMONIC_INDEX} --sender ${LEDGER_SENDER} --slow --broadcast --verify
4949

5050
deploy-libs :
5151
make deploy-libs-one chain=${chain}
52-
npx catapulta-verify -b broadcast/LibraryPreCompileOne.sol/${chainId}/run-latest.json
5352
make deploy-libs-two chain=${chain}
54-
npx catapulta-verify -b broadcast/LibraryPreCompileTwo.sol/${chainId}/run-latest.json
5553

5654

5755
# Invariants

‎README.md‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,17 @@ In addition, Enigma Dark has adapted the Foundry-based fuzzing [invariant suite]
9595

9696
<br>
9797

98+
**-> Aave v3.4 - June 2025**
99+
100+
#### Removal of custom GHO. Addition of Multicall & Position manager
101+
102+
- [Certora v3.4](./audits/2025-06-11_Certora_Aave-v3.4_Report.pdf), [Certora v3.4 AIP](./audits/2025-06-11_Certora_Aave-v3.4_AIP_Report.pdf)
103+
- [StErMi v3.4](./audits/2025-06-11_Stermi_Aave-v3.4_Report.pdf), [StErMi v3.4 AIP](./audits/2025-06-11_Stermi_Aave-v3.4_AIP_Report.pdf)
104+
- [Blackthorn](./audits/2025-06-12_Blackthorn-v3.4_Report.pdf)
105+
- [Enigma](./audits/2025-05-13_Enigma_Aave-v3.4.pdf)
106+
107+
<br>
108+
98109
### Bug bounty
99110

100111
This repository will be subjected to [this bug bounty](https://immunefi.com/bounty/aave/) once the Aave Governance upgrades the smart contracts in the applicable production instances.

‎audits/2025-05-13_Enigma_Aave-v3.4.pdf‎

286 KB
Binary file not shown.

‎audits/2025-06-11_Certora_Aave-v3.4_AIP_Report.pdf‎

302 KB
Binary file not shown.

‎audits/2025-06-11_Certora_Aave-v3.4_Report.pdf‎

375 KB
Binary file not shown.

0 commit comments

Comments
 (0)