-
Notifications
You must be signed in to change notification settings - Fork 100
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Certora Formal Verification for aave L2 bridges (#56) * certora folder added * Added spec and script for OptimismExecutor Created harnesses version of BridgeExecutorBase.sol Added windows script, Created spec file for ExecutorBase. Modified the import file for L2Bridge * Created munged direcotry Restored original code, Added munged directory, Some modifications in munged and added a harness version. * Updated bridge spec and harnessed files. * Updated Harness and Spec * Verified rules in spec. Changed target calls mocks. * Updated OptimisimBridge spec * Updated optimism executor spec * Added a target call mock contract. Removed targetCall from the Optimism contract and created a mock contract instead. Added links to the script. * Added verification for Polygon Bridge Created: PolygonHarness.sol - bridge harness verifyPolygon.sh - script mockTargetPoly.sol - target mock contract PolygonBridge.spec - spec file * Updated Polygon and Optimism specs * splitting certora's gitignore from main gitignore * Updated Polygon & Optimism spec (after review) Changed specs for both Optimism and Polygon "Removed" queue function, replaced by queue2 Harnessed executeDelegateCall, without delegates. * Update PolygonBridge.spec * Added Arbitrum verficiation Combined Arbitrum & Optimism spec. Added script for Arbitrum. Added links for full verification reports. * adding certora files to gitignore * deleting json file * adding the verification report * Create README.md * Update README.md * Updated independentQueuedActions rule * Update Formal Verification Report of AAVE L2 Bridge.pdf * Updated noIncarnations rule. Co-authored-by: Roy-Certora <[email protected]> * fix: Update certora scripts * L2 bridges audit - adding CI Integration for Certora's Formal Verification (#61) * certora folder added * fix: Fix natspec typo * Added spec and script for OptimismExecutor Created harnesses version of BridgeExecutorBase.sol Added windows script, Created spec file for ExecutorBase. Modified the import file for L2Bridge * Created munged direcotry Restored original code, Added munged directory, Some modifications in munged and added a harness version. * Updated bridge spec and harnessed files. * Updated Harness and Spec * Verified rules in spec. Changed target calls mocks. * Updated OptimisimBridge spec * Updated optimism executor spec * Added a target call mock contract. Removed targetCall from the Optimism contract and created a mock contract instead. Added links to the script. * Added verification for Polygon Bridge Created: PolygonHarness.sol - bridge harness verifyPolygon.sh - script mockTargetPoly.sol - target mock contract PolygonBridge.spec - spec file * Updated Polygon and Optimism specs * splitting certora's gitignore from main gitignore * Updated Polygon & Optimism spec (after review) Changed specs for both Optimism and Polygon "Removed" queue function, replaced by queue2 Harnessed executeDelegateCall, without delegates. * Update PolygonBridge.spec * Added Arbitrum verficiation Combined Arbitrum & Optimism spec. Added script for Arbitrum. Added links for full verification reports. * adding certora files to gitignore * deleting json file * adding the verification report * Create README.md * Update README.md * Updated independentQueuedActions rule * updated report * Update Formal Verification Report of AAVE L2 Bridge.pdf * Updated noIncarnations rule. * Update AddressAliasHelper library to work with solidity 0.8 version (#58) * test: Add test that bricks the executor with an underflowing address * fix: Updates the AddressAliasHelper library with 0.8 solidity version * feat: Add CI setup * adding mocks to munged + updating arbitrum dependency * created harness patch and munged directory * adding git action * fixing yaml * adding ls checks for munged * fixing yaml * adding optimism and polygon yamls * testing git action on staging * changing the yaml back to cloud * removing complexity check * fixing error in line 105 * installing certora-cli-alpha-master instead of certora-cli * adding debug * removing debug * returning to certora-clo * going back to regular cli * removing munged content * updating python version to 3.9 * removing non existing rule in polygon * adding mocks to munged + updating arbitrum dependency * setting CI integration for formal verification by Certora Co-authored-by: miguelmtzinf <[email protected]> Co-authored-by: miguelmtz <[email protected]> Co-authored-by: Roy-Certora <[email protected]> * docs: Add audit report for L2 bridge contracts Co-authored-by: Michael Morami <[email protected]> Co-authored-by: Roy-Certora <[email protected]>
- Loading branch information
1 parent
e895877
commit 93c39de
Showing
43 changed files
with
3,963 additions
and
2 deletions.
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,74 @@ | ||
name: certora-arbitrum | ||
|
||
on: | ||
push: | ||
branches: | ||
- main | ||
- l2-bridges-audit | ||
pull_request: | ||
branches: | ||
- main | ||
|
||
workflow_dispatch: | ||
|
||
jobs: | ||
verify: | ||
runs-on: ubuntu-latest | ||
|
||
steps: | ||
- uses: actions/checkout@v2 | ||
|
||
- name: Check key | ||
env: | ||
CERTORAKEY: ${{ secrets.CERTORAKEY }} | ||
run: echo "key length" ${#CERTORAKEY} | ||
|
||
- 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 | ||
|
||
- 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: Verify rule ${{ matrix.rule }} | ||
run: | | ||
cd certora | ||
touch applyHarness.patch | ||
make munged | ||
cd .. | ||
echo "key length" ${#CERTORAKEY} | ||
sh certora/scripts/${{ matrix.rule }} | ||
env: | ||
CERTORAKEY: ${{ secrets.CERTORAKEY }} | ||
|
||
strategy: | ||
fail-fast: false | ||
max-parallel: 16 | ||
matrix: | ||
rule: | ||
- verifyArbitrum.sh executedValidTransition2 | ||
- verifyArbitrum.sh onlyCancelCanCancel | ||
- verifyArbitrum.sh onlyQueuedAreExecuted | ||
- verifyArbitrum.sh expiredForever | ||
- verifyArbitrum.sh actionNotCanceledAndExecuted | ||
- verifyArbitrum.sh properDelay | ||
- verifyArbitrum.sh notCanceledNotExecuted | ||
- verifyArbitrum.sh minDelayLtMaxDelay | ||
- verifyArbitrum.sh whoChangedStateVariables | ||
- verifyArbitrum.sh executeCannotCancel | ||
- verifyArbitrum.sh whoChangesActionsSetState | ||
- verifyArbitrum.sh canceledForever | ||
- verifyArbitrum.sh executedForever | ||
- verifyArbitrum.sh executeRevertsBeforeDelay | ||
- verifyArbitrum.sh noIncarnations1 noIncarnations2 noIncarnations3 | ||
- verifyArbitrum.sh actionDuplicate holdYourHorses executeFailsIfExpired executedValidTransition1 queuePriviliged afterQueueHashQueued queue2Reachability cancelPriviliged independentQueuedActions queueCannotCancel queueDoesntModifyStateVariables queuedStateConsistency queuedChangedCounter sameExecutionTimesReverts cancelExclusive |
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,74 @@ | ||
name: certora-optimism | ||
|
||
on: | ||
push: | ||
branches: | ||
- main | ||
- l2-bridges-audit | ||
pull_request: | ||
branches: | ||
- main | ||
|
||
workflow_dispatch: | ||
|
||
jobs: | ||
verify: | ||
runs-on: ubuntu-latest | ||
|
||
steps: | ||
- uses: actions/checkout@v2 | ||
|
||
- name: Check key | ||
env: | ||
CERTORAKEY: ${{ secrets.CERTORAKEY }} | ||
run: echo "key length" ${#CERTORAKEY} | ||
|
||
- 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 | ||
|
||
- 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: Verify rule ${{ matrix.rule }} | ||
run: | | ||
cd certora | ||
touch applyHarness.patch | ||
make munged | ||
cd .. | ||
echo "key length" ${#CERTORAKEY} | ||
sh certora/scripts/${{ matrix.rule }} | ||
env: | ||
CERTORAKEY: ${{ secrets.CERTORAKEY }} | ||
|
||
strategy: | ||
fail-fast: false | ||
max-parallel: 16 | ||
matrix: | ||
rule: | ||
- verifyOptimism.sh executedValidTransition2 | ||
- verifyOptimism.sh onlyCancelCanCancel | ||
- verifyOptimism.sh onlyQueuedAreExecuted | ||
- verifyOptimism.sh expiredForever | ||
- verifyOptimism.sh actionNotCanceledAndExecuted | ||
- verifyOptimism.sh properDelay | ||
- verifyOptimism.sh notCanceledNotExecuted | ||
- verifyOptimism.sh minDelayLtMaxDelay | ||
- verifyOptimism.sh whoChangedStateVariables | ||
- verifyOptimism.sh executeCannotCancel | ||
- verifyOptimism.sh whoChangesActionsSetState | ||
- verifyOptimism.sh canceledForever | ||
- verifyOptimism.sh executedForever | ||
- verifyOptimism.sh executeRevertsBeforeDelay | ||
- verifyOptimism.sh noIncarnations1 noIncarnations2 noIncarnations3 | ||
- verifyOptimism.sh actionDuplicate holdYourHorses executeFailsIfExpired executedValidTransition1 queuePriviliged afterQueueHashQueued queue2Reachability cancelPriviliged independentQueuedActions queueCannotCancel queueDoesntModifyStateVariables queuedStateConsistency queuedChangedCounter sameExecutionTimesReverts cancelExclusive |
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,74 @@ | ||
name: certora-polygon | ||
|
||
on: | ||
push: | ||
branches: | ||
- main | ||
- l2-bridges-audit | ||
pull_request: | ||
branches: | ||
- main | ||
|
||
workflow_dispatch: | ||
|
||
jobs: | ||
verify: | ||
runs-on: ubuntu-latest | ||
|
||
steps: | ||
- uses: actions/checkout@v2 | ||
|
||
- name: Check key | ||
env: | ||
CERTORAKEY: ${{ secrets.CERTORAKEY }} | ||
run: echo "key length" ${#CERTORAKEY} | ||
|
||
- 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 | ||
|
||
- 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: Verify rule ${{ matrix.rule }} | ||
run: | | ||
cd certora | ||
touch applyHarness.patch | ||
make munged | ||
cd .. | ||
echo "key length" ${#CERTORAKEY} | ||
sh certora/scripts/${{ matrix.rule }} | ||
env: | ||
CERTORAKEY: ${{ secrets.CERTORAKEY }} | ||
|
||
strategy: | ||
fail-fast: false | ||
max-parallel: 16 | ||
matrix: | ||
rule: | ||
- verifyPolygon.sh executedValidTransition2 | ||
- verifyPolygon.sh onlyCancelCanCancel | ||
- verifyPolygon.sh onlyQueuedAreExecuted | ||
- verifyPolygon.sh expiredForever | ||
- verifyPolygon.sh actionNotCanceledAndExecuted | ||
- verifyPolygon.sh properDelay | ||
- verifyPolygon.sh notCanceledNotExecuted | ||
- verifyPolygon.sh minDelayLtMaxDelay | ||
- verifyPolygon.sh whoChangedStateVariables | ||
- verifyPolygon.sh executeCannotCancel | ||
- verifyPolygon.sh whoChangesActionsSetState | ||
- verifyPolygon.sh canceledForever | ||
- verifyPolygon.sh executedForever | ||
- verifyPolygon.sh executeRevertsBeforeDelay | ||
- verifyPolygon.sh noIncarnations1 noIncarnations2 noIncarnations3 | ||
- verifyPolygon.sh actionDuplicate holdYourHorses executeFailsIfExpired executedValidTransition1 queuePriviliged afterQueueHashQueued cancelPriviliged independentQueuedActions queueCannotCancel queueDoesntModifyStateVariables queuedStateConsistency queuedChangedCounter sameExecutionTimesReverts cancelExclusive |
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 |
---|---|---|
|
@@ -22,4 +22,9 @@ coverage.json | |
|
||
.DS_Store | ||
|
||
deployments/ | ||
deployments/ | ||
|
||
# Certora | ||
.certora* | ||
.last_confs | ||
certora_* |
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
Binary file not shown.
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,5 @@ | ||
# certora | ||
.certora* | ||
.certora*.json | ||
**.last_conf* | ||
certora-logs |
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,24 @@ | ||
default: help | ||
|
||
PATCH = applyHarness.patch | ||
CONTRACTS_DIR = ../contracts | ||
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 $@ | ||
cp -r $(CONTRACTS_DIR) $@ | ||
patch -p0 -d $@ < $(PATCH) | ||
|
||
record: | ||
diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+\.\./contracts/++g' | sed 's+munged/++g' > $(PATCH) | ||
|
||
clean: | ||
git clean -fdX | ||
touch $(PATCH) | ||
|
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,28 @@ | ||
## Verification Overview | ||
The current directory contains Certora's formal verification of AAVE's L2 bridge protocol. | ||
In this directory you will find three subdirectories: | ||
|
||
1. specs - Contains all the specification files that were written by Certora for the bridge protocol. We have created two spec files, `Optimism_ArbitrumBridge.spec`, `PolygonBridge.spec`, the first is used to verify Optimism and Arbitrum executors and the second for Polygon. The choice for this separation relies on the contracts inhertiance of these three bridges protocols. | ||
We emphasize that essentially the rules in both specs are the same (by context, name and logical idea), but the implementation might be a bit different due to implementation differences (for example the name given to the 'external queue' function.) | ||
|
||
2. scripts - Contains all the necessary run scripts to execute the spec files on the Certora Prover. These scripts composed of a run command of Certora Prover, contracts to take into account in the verification context, declaration of the compiler and a set of additional settings. Each script is named after the bridge type it verifies. Note that the Optimism and Arbitrum bridges are verified by the same spec file, but have separate scripts. | ||
|
||
3. harness - Contains all the inheriting contracts that add/simplify functionalities to the original contract. You will also find a set of symbolic and dummy implementations of external contracts on which the executors rely. | ||
These harnesses, i.e. extensions/simplifications, are necessary to run the verifications. Assumptions and under-approximations are also done in a few places, in order to supply partial coverage where full coverage is not achievable. | ||
One harness worth explaining is the mockTarget and mockTargetPoly contracts that were created in order to simualte the low-level calls of the executed transactions. | ||
|
||
</br> | ||
|
||
--- | ||
|
||
## Running Instructions | ||
To run a verification job: | ||
|
||
1. Open terminal and `cd` your way to the main AAVE L2 repository. | ||
|
||
2. Run the script you'd like to get results for: | ||
``` | ||
sh certora/scripts/verifyOptimism.sh | ||
``` | ||
|
||
</br> |
Oops, something went wrong.