L2 bridges audit #63
Merged
L2 bridges audit #63
Conversation
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
* 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]>
…ation (#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]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.