Feat/phase 3 #117
Workflow file for this run
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
| name: certora-review-receiver | |
| on: | |
| push: | |
| branches: | |
| - main | |
| pull_request: | |
| branches: | |
| - main | |
| workflow_dispatch: | |
| jobs: | |
| verify: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v2 | |
| with: | |
| submodules: recursive | |
| - 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: pip3 install certora-cli==4.13.1 | |
| - name: Install solc | |
| run: | | |
| wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux | |
| chmod +x solc-static-linux | |
| sudo mv solc-static-linux /usr/local/bin/solc8.19 | |
| - name: Verify rule ${{ matrix.rule }} | |
| run: | | |
| cd security/certora | |
| touch applyHarness.patch | |
| make munged | |
| cd ../.. | |
| certoraRun security/certora/confs/${{ matrix.rule }} | |
| env: | |
| CERTORAKEY: ${{ secrets.CERTORAKEY }} | |
| strategy: | |
| fail-fast: false | |
| max-parallel: 16 | |
| matrix: | |
| rule: | |
| - verifyCrossChainControllerWithEmergency.conf | |
| #- verifyCrossChainReceiver.conf --rule receive_more_than__requiredConfirmations_diff_2 # TODO: uncomment when moving to cli 5.0.2 or higher | |
| #- verifyCrossChainReceiver.conf --rule receive_more_than__requiredConfirmations_diff_3 # TODO: uncomment when moving to cli 5.0.2 or higher | |
| - verifyCrossChainReceiver.conf --rule transaction_received_only_from_authorized_bridge_adapter only_owner_can_change_bridge_adapters only_owner_can_change_bridge_adapters_witness_consequent only_owner_can_change_required_confirmations only_owner_can_change_required_confirmations_witness_consequent cannot_call_IBaseReceiverPortal_receiveCrossChainMessage_twice cannot_call_IBaseReceiverPortal_receiveCrossChainMessage_twice_witness_tight_bound state_transition_to_deliver_iff_IBaseReceiverPortal_receiveCrossChainMessage_called | |
| - verifyCrossChainReceiver.conf --rule state_transition_to_deliver_iff_IBaseReceiverPortal_receiveCrossChainMessage_called_witness_antecedent call_deliverEnvelope_once_witness_antecedent anyone_can_call_deliverEnvelope invalidate_previous_unconfirmed_envelopes_after_updateMessagesValidityTimestamp_witness_antecedent receiveCrossChainMessage_cannot_change_state_if_requiredConfirmation_is_zero envelope_state envelope_state_witness_none_to_delivered only_single_bridge_adapter_added only_single_bridge_adapter_removed | |
| - verifyCrossChainReceiver.conf --rule envelope_state_witness_confirmed_to_delivered envelope_state_witness_none_to_confirmed envelope_state_witness_none_none_confirmed envelope_state_witness_none_confirmed_confirmed envelope_state_witness_confirmed_confirmed_confirmed confirmations_increments_if_received_from_msg_sender confirmations_increments_if_received_from_msg_sender_witness allowReceiverBridgeAdapters_cannot_disallow allowReceiverBridgeAdapters_cannot_disallow_witness | |
| - verifyCrossChainReceiver.conf --rule disallowReceiverBridgeAdapters_cannot_allow disallowReceiverBridgeAdapters_cannot_allow_witness_antecedent disallowReceiverBridgeAdapters_cannot_allow_witness_consequent requiredConfirmation_is_positive_after_updateConfirmations receive_increments_confirmations | |
| - verifyCrossChainReceiver.conf --rule reachability encodeDecodeWorks encodeDecodeWorks_witness encodeDecodeWorks_witness_2 | |
| - verifyCrossChainReceiver.conf --rule firstBridgedAt_happened_in_the_past | |
| - verifyCrossChainReceiver.conf --rule no_deliverEnvelope_after_receiveCrossChainMessage | |
| #- verifyCrossChainReceiver.conf --rule call_deliverEnvelope_once # TODO: uncomment when moving to cli 5.0.2 or higher | |
| #- verifyCrossChainReceiver.conf --rule invalidate_previous_unconfirmed_envelopes_after_updateMessagesValidityTimestamp # TODO: uncomment when moving to cli 5.0.2 or higher | |
| #- verifyCrossChainReceiver.conf --rule addressSetInvariant # TODO: uncomment when moving to cli 5.0.2 or higher | |
| #- verifyCrossChainReceiver.conf --rule cannot_call_BaseReceiverPortal_receiveCrossChainMessage_twice # TODO: uncomment when moving to cli 5.0.2 or higher | |
| - verifyCrossChainReceiver.conf --rule zero_firstBridgedAt_iff_not_received_from_msg_sender |