L2 bridges audit - adding CI Integration for Certora's Formal Verification

.github/workflows/certora-arbitrum.yaml

@@ -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

.github/workflows/certora-optimism.yaml

@@ -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

.github/workflows/certora-polygon.yaml

@@ -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

.github/workflows/node.js.yml

@@ -0,0 +1,35 @@
+name: Build
+'on':
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - master
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    env:
+      ALCHEMY_KEY: '${{secrets.ALCHEMY_KEY}}'
+    strategy:
+      matrix:
+        node-version:
+          - 16.x
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Setup node
+        uses: actions/setup-node@v3
+        with:
+          node-version: 16.0.x
+          cache: npm
+      - name: Install Dependencies
+        run: npm ci
+      - name: Compilation
+        run: 'npm run compile'
+      - name: Tests
+        run: 'npm run test'
+      - name: Fork Tests
+        run: 'npm run test-fork'

.gitignore

@@ -22,4 +22,9 @@ coverage.json
 
 .DS_Store
 
-deployments/
+deployments/
+
+# Certora
+.certora*
+.last_confs
+certora_*

certora/Makefile

@@ -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)
+

certora/README.md

@@ -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>