Certora Prover Integration

contracts/bridge/certora/.gitignore

@@ -0,0 +1,7 @@
+#certora
+.certora*
+.certora*.json
+**.last_conf*
+certora-logs
+resource_errors.json
+.zip-output-url.txt

contracts/bridge/certora/Makefile

@@ -0,0 +1,25 @@
+default: help
+
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../flat
+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+\.\./flat/++g' | sed 's+munged/++g' > $(PATCH)
+
+clean:
+	git clean -fdX
+	touch $(PATCH)
+
+.PHONY: help munged record clean

contracts/bridge/certora/README.md

@@ -0,0 +1,14 @@
+## Running Instructions
+To run a verification job:
+
+1. Open terminal and `cd` your way to the `certora` directory in the bridge repository.
+
+2. Execute the `munged` command in the make file to copy the contracts to the munged directory and apply the changes in the patch:
+    ```sh
+    make munged
+    ```
+
+3. Run the script you'd like to get results for:
+    ```sh
+    sh scripts/BeaconLightClient.sh
+    ```

contracts/bridge/certora/applyHarness.patch

@@ -0,0 +1,76 @@
+diff -ruN .gitignore .gitignore
+--- .gitignore	1970-01-01 08:00:00
++++ .gitignore	2022-11-15 10:21:37
+@@ -0,0 +1,2 @@
++*
++!.gitignore
+diff -ruN BeaconLightClient.f.sol BeaconLightClient.f.sol
+--- BeaconLightClient.f.sol	2022-10-31 15:23:14
++++ BeaconLightClient.f.sol	2022-11-15 10:25:07
+@@ -955,9 +955,9 @@
+
+     // follow beacon api: /beacon/light_client/updates/?start_period={period}&count={count}
+     function import_next_sync_committee(
+-        FinalizedHeaderUpdate calldata header_update,
+-        SyncCommitteePeriodUpdate calldata sc_update
+-    ) external {
++        FinalizedHeaderUpdate memory header_update,
++        SyncCommitteePeriodUpdate memory sc_update
++    ) internal {
+         require(is_supermajority(header_update.sync_aggregate.sync_committee_bits), "!supermajor");
+         require(header_update.signature_slot > header_update.attested_header.slot &&
+                 header_update.attested_header.slot >= header_update.finalized_header.slot,
+@@ -1004,7 +1004,7 @@
+     }
+
+     // follow beacon api: /eth/v1/beacon/light_client/finality_update/
+-    function import_finalized_header(FinalizedHeaderUpdate calldata update) external {
++    function import_finalized_header(FinalizedHeaderUpdate memory update) internal {
+         require(is_supermajority(update.sync_aggregate.sync_committee_bits), "!supermajor");
+         require(update.signature_slot > update.attested_header.slot &&
+                 update.attested_header.slot >= update.finalized_header.slot,
+@@ -1039,10 +1039,10 @@
+     }
+
+     function verify_signed_header(
+-        SyncAggregate calldata sync_aggregate,
+-        SyncCommittee calldata sync_committee,
++        SyncAggregate memory sync_aggregate,
++        SyncCommittee memory sync_committee,
+         bytes4 fork_version,
+-        BeaconBlockHeader calldata header
++        BeaconBlockHeader memory header
+     ) internal view returns (bool) {
+         // Verify sync committee aggregate signature
+         uint participants = sum(sync_aggregate.sync_committee_bits);
+@@ -1066,8 +1066,8 @@
+     }
+
+     function verify_finalized_header(
+-        BeaconBlockHeader calldata header,
+-        bytes32[] calldata finality_branch,
++        BeaconBlockHeader memory header,
++        bytes32[] memory finality_branch,
+         bytes32 attested_header_root
+     ) internal pure returns (bool) {
+         require(finality_branch.length == FINALIZED_CHECKPOINT_ROOT_DEPTH, "!finality_branch");
+@@ -1082,8 +1082,8 @@
+     }
+
+     function verify_next_sync_committee(
+-        SyncCommittee calldata next_sync_committee,
+-        bytes32[] calldata next_sync_committee_branch,
++        SyncCommittee memory next_sync_committee,
++        bytes32[] memory next_sync_committee_branch,
+         bytes32 header_state_root
+     ) internal pure returns (bool) {
+         require(next_sync_committee_branch.length == NEXT_SYNC_COMMITTEE_DEPTH, "!next_sync_committee_branch");
+@@ -1097,7 +1097,7 @@
+         );
+     }
+
+-    function is_supermajority(bytes32[2] calldata sync_committee_bits) internal pure returns (bool) {
++    function is_supermajority(bytes32[2] memory sync_committee_bits) internal pure returns (bool) {
+         return sum(sync_committee_bits) * 3 >= SYNC_COMMITTEE_SIZE * 2;
+     }
+

contracts/bridge/certora/harness/BeaconLightClientHarness.sol

@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity =0.7.6;
+pragma abicoder v2;
+
+import "../munged/BeaconLightClient.f.sol";
+
+contract BeaconLightClientHarness is BeaconLightClient {
+    constructor(
+        address _bls,
+        uint64 _slot,
+        uint64 _proposer_index,
+        bytes32 _parent_root,
+        bytes32 _state_root,
+        bytes32 _body_root,
+        bytes32 _current_sync_committee_hash,
+        bytes32 _genesis_validators_root
+    ) BeaconLightClient(
+        _bls,
+        _slot,
+        _proposer_index,
+        _parent_root,
+        _state_root,
+        _body_root,
+        _current_sync_committee_hash,
+        _genesis_validators_root
+    ){}
+
+    FinalizedHeaderUpdate finalized_header_update;
+    // SyncCommitteePeriodUpdate sync_committee_update;
+    // function call_ip_next_sync_committee() external {
+    //     import_next_sync_committee(
+    //         finalized_header_update,
+    //         sync_committee_update
+    //     );
+    // }
+
+    function call_ip_finalized_header() external {
+        import_finalized_header(finalized_header_update);
+    }
+}

contracts/bridge/certora/harness/OutboundLaneHarness.sol

@@ -0,0 +1,30 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity =0.7.6;
+pragma abicoder v2;
+
+import "../munged/OutboundLane.f.sol";
+
+contract OutboundLaneHarness is OutboundLane {
+
+    constructor(
+        address _lightClientBridge,
+        address _feeMarket,
+        uint32 _thisChainPosition,
+        uint32 _thisLanePosition,
+        uint32 _bridgedChainPosition,
+        uint32 _bridgedLanePosition,
+        uint64 _oldest_unpruned_nonce,
+        uint64 _latest_received_nonce,
+        uint64 _latest_generated_nonce
+    ) OutboundLane (
+        _lightClientBridge,
+        _feeMarket,
+        _thisChainPosition,
+        _thisLanePosition,
+        _bridgedChainPosition,
+        _bridgedLanePosition,
+        _oldest_unpruned_nonce,
+        _latest_received_nonce,
+        _latest_generated_nonce
+    ) {}
+}

contracts/bridge/certora/harness/SimpleFeeMarketHarness.sol

@@ -0,0 +1,24 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity =0.7.6;
+pragma abicoder v2;
+
+import "../munged/SimpleFeeMarket.f.sol";
+
+contract SimpleFeeMarketHarness is SimpleFeeMarket {
+
+    constructor(
+        uint256 _collateral_perorder,
+        uint256 _slash_time,
+        uint256 _relay_time,
+        uint256 _price_ratio_numerator,
+        uint256 _duty_reward_ratio
+    ) SimpleFeeMarket(
+        _collateral_perorder,
+        _slash_time,
+        _relay_time,
+        _price_ratio_numerator,
+        _duty_reward_ratio
+    ) {
+        initialize();
+    }
+}

contracts/bridge/certora/munged/.gitignore

@@ -0,0 +1,2 @@
+*
+!.gitignore

contracts/bridge/certora/scripts/BeaconLightClient.sh

@@ -0,0 +1,21 @@
+#!/bin/bash
+
+set -ex
+
+if [[ "$1" ]]
+then
+    RULE="--rule $1"
+fi
+
+certoraRun harness/BeaconLightClientHarness.sol:BeaconLightClientHarness \
+    --verify BeaconLightClientHarness:specs/BeaconLightClient.spec \
+    --solc solc-0.7.6 \
+    --rule_sanity basic \
+    $RULE \
+    --optimistic_loop \
+    --include_empty_fallback \
+    --msg "BeaconLightClient"
+
+    # --debug \
+    # --typecheck_only \
+    # --multi_assert_check \

contracts/bridge/certora/scripts/OutboundLane.sh

@@ -0,0 +1,21 @@
+#!/bin/bash
+
+set -ex
+
+if [[ "$1" ]]
+then
+    RULE="--rule $1"
+fi
+
+certoraRun harness/OutboundLaneHarness.sol:OutboundLaneHarness \
+    --verify OutboundLaneHarness:specs/OutboundLane.spec \
+    --solc solc-0.7.6 \
+    --rule_sanity basic \
+    $RULE \
+    --optimistic_loop \
+    --include_empty_fallback \
+    --msg "OutboundLane"
+
+    # --debug \
+    # --typecheck_only \
+    # --multi_assert_check \

contracts/bridge/certora/scripts/SimpleFeeMarket.sh

@@ -0,0 +1,19 @@
+#!/bin/bash
+
+set -ex
+
+if [[ "$1" ]]
+then
+    RULE="--rule $1"
+fi
+
+certoraRun harness/SimpleFeeMarketHarness.sol:SimpleFeeMarketHarness \
+    --verify SimpleFeeMarketHarness:specs/SimpleFeeMarket.spec \
+    --solc solc-0.7.6 \
+    $RULE \
+    --msg "SimpleFeeMarket"
+
+    # --rule_sanity basic \
+    # --optimistic_loop \
+    # --typecheck_only \
+    # --multi_assert_check \

contracts/bridge/certora/specs/BeaconLightClient.spec

@@ -0,0 +1,57 @@
+// BeaconLightClient.spec
+
+methods {
+    finalized_header() returns (uint64,uint64,bytes32,bytes32,bytes32) envfree
+    sync_committee_roots(uint64) returns bytes32 envfree
+
+//    call_ip_next_sync_committee()
+    call_ip_finalized_header()
+}
+
+definition SLOTS_PER_EPOCH() returns uint64 = 32;
+definition EPOCHS_PER_SYNC_COMMITTEE_PERIOD() returns uint64 = 256;
+
+function get_finalized_header_slot() returns uint64 {
+    uint64 slot;
+    uint64 proposer_index;
+    bytes32 parent_root;
+    bytes32 state_root;
+    bytes32 body_root;
+    slot, proposer_index, parent_root, state_root, body_root = finalized_header();
+    return slot;
+}
+
+// Verify fallback always reverts
+rule fallback_revert(method f) filtered { f -> f.isFallback } {
+    env e;
+    calldataarg arg;
+    f@withrevert(e, arg);
+    assert(lastReverted, "Fallback did not revert");
+}
+
+rule ip_finalized_header() {
+    uint64 slot0 = get_finalized_header_slot();
+
+    env e;
+    call_ip_finalized_header(e);
+
+    uint64 slot1 = get_finalized_header_slot();
+    assert(slot1 > slot0, "import new block header");
+}
+
+// rule ip_next_sync_committee() {
+//     uint64 slot0 = get_finalized_header_slot();
+//     uint64 period0 = slot0 / SLOTS_PER_EPOCH() / EPOCHS_PER_SYNC_COMMITTEE_PERIOD();
+//     bytes32 root0 = sync_committee_roots(period0);
+
+//     env e;
+//     call_ip_next_sync_committee(e);
+
+//     uint64 period1 = period0 + 1;
+//     bytes32 root1 = sync_committee_roots(period1);
+
+//     uint64 slot1 = get_finalized_header_slot();
+//     assert(slot1 >= slot0, "import new block header or not");
+//     bytes32 zero = 0x0000000000000000000000000000000000000000000000000000000000000000;
+//     assert(root0 != zero && root1 == zero => (root1 != zero), "import new synccommittee");
+// }

contracts/bridge/certora/specs/OutboundLane.spec

@@ -0,0 +1,28 @@
+// OutboundLane.spec
+
+methods {
+    outboundLaneNonce() returns (uint64,uint64,uint64) envfree
+    messages(uint64) returns bytes32 envfree
+    commitment() returns bytes32 envfree
+    message_size() returns uint64 envfree
+
+    send_message(address,bytes) returns (uint64) => DISPATCHER(true)
+}
+
+// Verify fallback always reverts
+rule fallback_revert(method f) filtered { f -> f.isFallback } {
+    env e;
+    calldataarg arg;
+    f@withrevert(e, arg);
+    assert(lastReverted, "Fallback did not revert");
+}
+
+rule send_message_noauth() {
+    uint64 size0 = message_size();
+    require(size0 == 0);
+    env e;
+    calldataarg arg;
+    send_message(e, arg);
+    uint64 size1 = message_size();
+    assert(size1 == 1, "!send");
+}

contracts/bridge/certora/specs/SimpleFeeMarket.spec

@@ -0,0 +1,20 @@
+// SimpleFeeMarket.spec
+
+methods {
+    setter()           returns address envfree
+    outbounds(address) returns uint256    envfree
+    balanceOf(address) returns uint256 envfree
+    lockedOf(address)  returns uint256 envfree
+    relayers(address)  returns address envfree
+    relayerCount()     returns uint256 envfree
+    feeOf(address)     returns uint256 envfree
+    orderOf(uint256)   returns (uint32,address,uint256,uint256) envfree
+}
+
+// Verify fallback always reverts
+rule fallback_revert(method f) filtered { f -> f.isFallback } {
+    env e;
+    calldataarg arg;
+    f@withrevert(e, arg);
+    assert(lastReverted, "Fallback did not revert");
+}