Skip to content

Certora formal verification specifications and CI #1638

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
aehyvari wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Certora formal verification specifications and CI #1638

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
116 changes: 29 additions & 87 deletions .github/workflows/certora-prover.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,37 +6,43 @@ on:
types: [closed]
branches:
- main

# Run on any pushes to certora/* branches
push:
branches:
- 'certora/**'

# Biweekly schedule (1st and 15th of each month at midnight UTC)
schedule:
- cron: '0 0 1,15 * *'

# Manual trigger
workflow_dispatch:

jobs:
# First job: Compile the contracts for Certora verification
compile:
name: Compile
# Compile the contracts and run verification
compile_and_verify:
name: Compile and verify
# Run if it meets one of these conditions:
# 1. It's a merged PR from a feat/* branch to dev
# 2. It's a push to a certora/* branch
# 3. It's a scheduled run
# 4. It's a manually triggered run
if: >
(github.event_name == 'pull_request' &&
github.event.pull_request.merged == true &&
startsWith(github.head_ref, 'feat/')) ||
(github.event_name == 'push' &&
(github.event_name == 'pull_request' &&
github.event.pull_request.merged == true &&
startsWith(github.head_ref, 'feat/')) ||
(github.event_name == 'push' &&
startsWith(github.ref, 'refs/heads/certora/')) ||
github.event_name == 'schedule' ||
github.event_name == 'schedule' ||
github.event_name == 'workflow_dispatch'
runs-on: protocol-x64-16core
runs-on: ubuntu-latest
# runs-on: protocol-x64-16core
permissions:
contents: read
statuses: write
pull-requests: write
id-token: write
steps:
- uses: step-security/harden-runner@ec9f2d5744a09debf3a187a3f4f675c53b671911
with:
Expand All @@ -49,93 +55,29 @@ jobs:
# Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow
ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }}

# Install the Foundry toolchain
- name: Install Foundry
uses: foundry-rs/foundry-toolchain@82dee4ba654bd2146511f85f0d013af94670c4de
with:
version: stable

# Install dependencies using Forge
- name: Install forge dependencies
run: forge install

# Run Certora compilation step only
- uses: Certora/certora-run-action@56c6a98e84eee5cd3a135967a9a4bc06ef6d38cc
with:
# List of configuration files for different contracts to verify
configurations: |-
certora/confs/core/AllocationManager.conf
certora/confs/core/AllocationManagerSanity.conf
certora/confs/core/DelegationManager.conf
certora/confs/core/DelegationManagerValidState.conf
certora/confs/core/StrategyManager.conf
certora/confs/permissions/Pausable.conf
certora/confs/pods/EigenPodManagerRules.conf
certora/confs/strategies/StrategyBase.conf
use-beta: true
solc-versions: 0.8.27
solc-remove-version-prefix: "0."
job-name: "Eigenlayer Contracts"
certora-key: ${{ secrets.CERTORAKEY }}
# Only compile, don't run verification yet
compilation-steps-only: true
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

# Second job: Run the actual verification after compilation succeeds
verify:
name: Verify
runs-on: protocol-x64-16core
# This job depends on the compile job
needs: compile
# Same conditions as the compile job
if: >
(github.event_name == 'pull_request' &&
github.event.pull_request.merged == true &&
startsWith(github.head_ref, 'feat/')) ||
(github.event_name == 'push' &&
startsWith(github.ref, 'refs/heads/certora/')) ||
github.event_name == 'schedule' ||
github.event_name == 'workflow_dispatch'
steps:
- uses: step-security/harden-runner@ec9f2d5744a09debf3a187a3f4f675c53b671911
with:
egress-policy: audit

# Checkout the repository with submodules
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
with:
submodules: recursive
# Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow
ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }}

# Install the Foundry toolchain.
- name: Install Foundry
uses: foundry-rs/foundry-toolchain@82dee4ba654bd2146511f85f0d013af94670c4de
with:
version: stable

# Install dependencies using Forge
- name: Install forge dependencies
run: forge install

# Run Certora verification with the same configurations
- uses: Certora/certora-run-action@56c6a98e84eee5cd3a135967a9a4bc06ef6d38cc
# Run Certora compilation and verification
- name: Run Certora compilation and verification
uses: Certora/certora-run-action@11979c68d2ffab0b1b2fe6c72ec9d7a38855822d
with:
# List of configuration files for different contracts to verify
configurations: |-
certora/confs/multichain/CrossChainRegistry.conf
certora/confs/multichain/KeyRegistrar.conf
certora/confs/multichain/OperatorTableUpdater.conf
certora/confs/multichain/ECDSACertificateVerifier.conf
certora/confs/multichain/BN254CertificateVerifier.conf
certora/confs/core/AllocationManager.conf
certora/confs/core/AllocationManagerOverslashing.conf
certora/confs/core/AllocationManagerValidState.conf
certora/confs/core/AllocationManagerSanity.conf
certora/confs/core/DelegationManager.conf
certora/confs/core/DelegationManagerValidState.conf
certora/confs/core/StrategyManager.conf
certora/confs/permissions/Pausable.conf
certora/confs/pods/EigenPodManagerRules.conf
certora/confs/strategies/StrategyBase.conf
use-beta: true
solc-versions: 0.8.27
solc-remove-version-prefix: "0."
job-name: "Eigenlayer Contracts"
job-name: "Verified Rules"
certora-key: ${{ secrets.CERTORAKEY }}
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
62 changes: 0 additions & 62 deletions .github/workflows/certora.yml
View file
Open in desktop

This file was deleted.

97 changes: 54 additions & 43 deletions certora/confs/core/AllocationManager.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,45 +1,56 @@
{
"assert_autofinder_success": true,
"files": [
"src/contracts/core/AllocationManager.sol",
"src/contracts/permissions/PauserRegistry.sol",
"src/contracts/permissions/PermissionController.sol",
"src/contracts/core/DelegationManager.sol",
"src/contracts/pods/EigenPodManager.sol",
"src/contracts/core/StrategyManager.sol",
"src/contracts/strategies/StrategyBase.sol",
"certora/mocks/CertoraAVSRegistrar.sol",
"lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
"src/contracts/libraries/OperatorSetLib.sol"
"assert_autofinder_success": true,
// "build_cache": true,
"files": [
"certora/harnesses/AllocationManagerHarness.sol",
"src/contracts/permissions/PauserRegistry.sol",
"src/contracts/permissions/PermissionController.sol",
"src/contracts/core/DelegationManager.sol",
"src/contracts/pods/EigenPodManager.sol",
"src/contracts/core/StrategyManager.sol",
"src/contracts/strategies/StrategyBase.sol",
"certora/mocks/CertoraAVSRegistrar.sol",
"lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
"src/contracts/libraries/OperatorSetLib.sol",
"certora/harnesses/ShortStringsUpgradeableHarness.sol"
],
"java_args": [],
"link": [
"AllocationManagerHarness:pauserRegistry=PauserRegistry",
"DelegationManager:permissionController=PermissionController",
"DelegationManager:allocationManager=AllocationManagerHarness",
"AllocationManagerHarness:permissionController=PermissionController",
"DelegationManager:strategyManager=StrategyManager",
"AllocationManagerHarness:delegation=DelegationManager",
"EigenPodManager:delegationManager=DelegationManager",
"DelegationManager:eigenPodManager=EigenPodManager"
],
"loop_iter": "1",
"msg": "AllocationManager",
"optimistic_fallback": true,
"optimistic_loop": true,
"packages": [
"@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
],
"parametric_contracts": [
"AllocationManagerHarness"
],
"rule": [
"pendingDiffStateTransitions",
"pendingDiffStateTransitionModifyAllocations",
"redistributionRecipientCannotBeDeadAddress"
],
"java_args": [
],
"link": [
"AllocationManager:pauserRegistry=PauserRegistry",
"DelegationManager:permissionController=PermissionController",
"DelegationManager:allocationManager=AllocationManager",
"AllocationManager:permissionController=PermissionController",
"DelegationManager:strategyManager=StrategyManager",
"AllocationManager:delegation=DelegationManager",
"EigenPodManager:delegationManager=DelegationManager",
"DelegationManager:eigenPodManager=EigenPodManager"
],
"loop_iter": "1",
"optimistic_fallback": true,
"optimistic_loop": true,
"packages": [
"@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
],
"parametric_contracts": [
"AllocationManager"
],
"process": "emv",
"prover_args": [
" -recursionErrorAsAssert false -recursionEntryLimit 3"
],
"solc": "solc8.27",
"solc_optimize": "1",
"verify": "AllocationManager:certora/specs/core/AllocationManagerRules.spec",
"server": "production",
}
"process": "emv",
"prover_args": [
"-recursionErrorAsAssert false -recursionEntryLimit 3",
"-splitParallel true",
"-dontStopAtFirstSplitTimeout true"
],
"rule_sanity": "basic",
"server": "production",
// "solc_via_ir": true,
"solc_optimize": "1",
"verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerRules.spec",
"wait_for_results": "none"
}
62 changes: 62 additions & 0 deletions certora/confs/core/AllocationManagerOverslashing.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
{
// "build_cache": true,
"files": [
"certora/harnesses/AllocationManagerHarness.sol",
"src/contracts/permissions/PauserRegistry.sol",
"src/contracts/permissions/PermissionController.sol",
"src/contracts/core/DelegationManager.sol",
"src/contracts/pods/EigenPodManager.sol",
"src/contracts/core/StrategyManager.sol",
"src/contracts/strategies/StrategyBase.sol",
"certora/mocks/CertoraAVSRegistrar.sol",
"lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
"src/contracts/libraries/OperatorSetLib.sol",
"certora/harnesses/ShortStringsUpgradeableHarness.sol"
],
"java_args": [],
"link": [
"AllocationManagerHarness:pauserRegistry=PauserRegistry",
"DelegationManager:permissionController=PermissionController",
"DelegationManager:allocationManager=AllocationManagerHarness",
"AllocationManagerHarness:permissionController=PermissionController",
"DelegationManager:strategyManager=StrategyManager",
"AllocationManagerHarness:delegation=DelegationManager",
"EigenPodManager:delegationManager=DelegationManager",
"DelegationManager:eigenPodManager=EigenPodManager"
],
"loop_iter": "1",
"msg": "AllocationManager No Overslashing",
"optimistic_fallback": true,
"optimistic_loop": true,
"packages": [
"@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
],
"parametric_contracts": [
"AllocationManagerHarness"
],
"rule": [
"noOverslashingOfShares",
"noOverslashingOfOperatorShares",
"overslashingOfSharesAtMostOne",
],
"process": "emv",
"prover_args": [
"-recursionErrorAsAssert",
"false",
"-recursionEntryLimit",
"3",
"-dontStopAtFirstSplitTimeout",
"true",
"-split",
"false"
],
"smt_timeout": "7200",
"rule_sanity": "basic",
"server": "production",
"solc_via_ir": true,
"solc_optimize": "1",
"disable_solc_optimizers": ["cse" , "peephole"],
"verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerRules.spec",
"wait_for_results": "none"
}
Loading