Skip to content

Commit 8aa230b

Browse files
christiane-certoraaehyvari
christiane-certora
authored and
aehyvari
committed
Certora formal verification rules
1 parent 1c0b329 commit 8aa230b

File tree

76 files changed

+4795
-1
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

76 files changed

+4795
-1
lines changed

‎.github/workflows/certora-prover.yml‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
name: Certora Prover Submission Workflow
2+
description: |-
3+
This workflow submits Certora Prover jobs on the specified configurations. Once all
4+
jobs are successfully submitted, it will add a pending commit status to the commit.
5+
This status will be periodically updated with verification results of the jobs, along
6+
with the verification summary comment on the pull request.
7+
8+
For more information, please visit https://github.com/certora/certora-run-action.
9+
10+
on:
11+
pull_request:
12+
branches:
13+
- master
14+
- certora/specs
15+
workflow_dispatch:
16+
17+
jobs:
18+
certora_run_submission:
19+
runs-on: ubuntu-latest
20+
permissions:
21+
contents: read
22+
statuses: write
23+
pull-requests: write
24+
id-token: write
25+
steps:
26+
- name: Checkout repository
27+
uses: actions/checkout@v4
28+
with:
29+
submodules: recursive
30+
31+
# Run Certora munge script
32+
- name: Certora munge
33+
run: ./certora/scripts/patch.sh
34+
35+
# Submit verification jobs to Certora Prover
36+
- name: Submit verification jobs to Certora Prover
37+
uses: Certora/certora-run-action@v2
38+
with:
39+
# Add your configurations as lines, each line is separated.
40+
# Specify additional options for each configuration by adding them after the configuration.
41+
configurations: |-
42+
certora/confs/Balances.conf
43+
certora/confs/ConsistentState.conf
44+
certora/confs/ConsistentStateExtras.conf
45+
certora/confs/ConsistentStateExtras2.conf
46+
certora/confs/ConsistentStateExtras3Sanity.conf
47+
certora/confs/Enabled.conf
48+
certora/confs/Immutability.conf
49+
certora/confs/Liveness.conf
50+
certora/confs/PendingValues.conf
51+
certora/confs/Range.conf
52+
certora/confs/Reentrancy.conf
53+
certora/confs/Reverts.conf
54+
certora/confs/Roles.conf
55+
certora/confs/Timelock.conf
56+
certora/confs/TimelockRemovableTime.conf
57+
certora/confs/LostAssets.conf
58+
certora/confs/Conversions.conf
59+
certora/confs/ERC4626.conf
60+
certora/confs/Solvency.conf
61+
certora/confs/SolvencyInternal.conf
62+
solc-versions: 0.8.17 0.8.26
63+
job-name: "Verified Rules"
64+
certora-key: ${{ secrets.CERTORAKEY }}
65+
env:
66+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

‎.gitignore‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,4 +12,7 @@ broadcast/
1212
.env
1313

1414
# System Files
15-
.DS_Store
15+
.DS_Store
16+
17+
# certora generated files
18+
.certora_internal

‎certora/README.md‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
This folder contains the verification of EulerEarn using the Certora Prover.
2+
3+
The verification was inspired by the previous verification projects for Metamorpho and SiloVault (see https://github.com/morpho-org/metamorpho/tree/main/certora)
4+
5+
## Getting started
6+
7+
The code is compiled using 2 versions of solidity, which must be installed to run the verification as:
8+
9+
- `solc-0.8.17` for solidity compiler version 0.8.17 which is used for compiling Permit2
10+
- `solc-0.8.19` for solidity compiler version 0.8.26 which is used for compiling the rest of the solidity files.
11+
12+
Follow Certora installation instructions: https://docs.certora.com/en/latest/docs/user-guide/install.html and the repository build installation for EulerEarn.
13+
14+
## Folders and file structure
15+
16+
The [`certora/specs`](specs) folder contains the following files:
17+
18+
- [`ConsistentState.spec`](specs/ConsistentState.spec) checks various properties specifying what is the consistent state of EulerEarn, what are the reachable setting configurations (such as caps and fee).
19+
- [`Balances.spec`](specs/Balances.spec) checks that tokens are not kept on the EulerEarn contract. Any deposit ends up in the underlying vaults and any withdrawal is forwarded to the user.
20+
- [`Enabled.spec`](specs/Enabled.spec) checks properties about enabled flag of market, notably that it correctly tracks the fact that the market is in the withdraw queue.
21+
- [`Immutability.spec`](specs/Immutability.spec) checks that EulerEarn is immutable.
22+
- [`Liveness.spec`](specs/Liveness.spec) checks some liveness properties of EulerEarn, notably that some emergency procedures are always available.
23+
- [`PendingValues.spec`](specs/PendingValues.spec) checks properties on the values that are still under timelock. Those properties are notably useful to prove that actual storage variables, when set to the pending value, use a consistent value.
24+
- [`Range.spec`](specs/Range.spec) checks the bounds (if any) of storage variables.
25+
- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that EulerEarn is reentrancy safe by making sure that there are no untrusted external calls.
26+
- [`Reverts.spec`](specs/Reverts.spec) checks the revert conditions on entrypoints.
27+
- [`Roles.spec`](specs/Roles.spec) checks the access control and authorization granted by the respective EulerEarn roles. In particular it checks the hierarchy of roles.
28+
- [`Timelock.spec`](specs/Timelock.spec) verifies computations for periods during which we know the values are under timelock.
29+
30+
The [`certora/specs/summaries`](specs/summaries) folder contains summaries for different functions that simplify the behavior of different functions, namely mathematical functions in [`Math.spec`], and dispatching summaries that allow the prover to recognize the appropriate function to resolve to when we have external calls to underlying vaults.
31+
32+
The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
33+
34+
The [`certora/harnesses`](harnesses) folder contains harness contracts that enable the verification of EulerEarn, by exposing internal functions and fields.
35+
36+
The [`certora/mocks`](mocks) folder contains mock contracts that simplify the verification of EulerEarn, by fixing reference implementations for the underlying token and vaults.
37+
38+
The [`certora/scripts`](mocks) folder contains a patch that applies a simple modification to the EulerEarn contract that introduces ghost variables that simplify verification, and the `PatchAndCertoraRun.sh` script that is used to run rules after the patch is applied.
39+
40+
The [`certora/gambit`](gambit) folder contains mutation testing - modified versions of the EulerEarn contract that have been injected with bugs and configuration files to run different rules on EulerEarn and the mutations to show that these bugs can be found by the given rules.
41+
42+
## Specification imports graph
43+
44+
Most rules follow the same setup starting with `Range.spec`, with the exception of Roles, Reentrancy, Immutability, Balances, and MarketInteractions that require a different setup with non-standard summaries that have assertions or modifications to rule-specific flags.
45+
46+
```mermaid
47+
graph
48+
Liveness --> Reverts
49+
Reverts --> ConsistentState
50+
ConsistentState --> Timelock
51+
Timelock --> Enabled
52+
Enabled --> PendingValues
53+
PendingValues --> Range
54+
Roles
55+
Reentrancy
56+
Immutability
57+
Balances
58+
LostAssets --> Range
59+
```

‎certora/confs/Balances.conf‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
{
2+
"override_base_config": "certora/confs/BaseConfForInheritance.conf",
3+
"verify": "EulerEarnHarness:certora/specs/Balances.spec",
4+
"msg": "Euler Earn - Rules about Balances",
5+
"loop_iter": 2
6+
}

‎certora/confs/BaseConfForInheritance.conf‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
{
2+
"optimistic_loop": true,
3+
"global_timeout": "7200",
4+
"parametric_contracts": "EulerEarnHarness",
5+
"rule_sanity": "basic",
6+
"files": [
7+
"certora/harnesses/EulerEarnHarness.sol",
8+
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
9+
"lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
10+
"src/EulerEarnFactory.sol",
11+
"test/mocks/PerspectiveMock.sol",
12+
"certora/mocks/VaultMock0.sol",
13+
"certora/mocks/VaultMock1.sol",
14+
"certora/mocks/Token0.sol",
15+
"certora/harnesses/ERC20Helper.sol"
16+
],
17+
"link": [
18+
"EulerEarnHarness:evc=EthereumVaultConnector",
19+
"EulerEarnHarness:permit2Address=Permit2",
20+
"EulerEarnFactory:permit2Address=Permit2",
21+
"EulerEarnFactory:perspective=PerspectiveMock",
22+
"VaultMock0:_asset=Token0",
23+
"VaultMock1:_asset=Token0",
24+
"EulerEarnHarness:_asset=Token0"
25+
],
26+
"packages": [
27+
"ethereum-vault-connector=lib/ethereum-vault-connector/src",
28+
"euler-vault-kit=lib/euler-vault-kit/src",
29+
"forge-std=lib/forge-std/src",
30+
"solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
31+
],
32+
"compiler_map": {
33+
"EulerEarnHarness": "solc-0.8.26",
34+
"EthereumVaultConnector": "solc-0.8.26",
35+
"Permit2": "solc-0.8.17",
36+
"EulerEarnFactory": "solc-0.8.26",
37+
"PerspectiveMock": "solc-0.8.26",
38+
"IRMLinearKink": "solc-0.8.26",
39+
"VaultMock0": "solc-0.8.26",
40+
"VaultMock1": "solc-0.8.26",
41+
"Token0": "solc-0.8.26",
42+
"ERC20Helper": "solc-0.8.26"
43+
},
44+
"solc_optimize": "200",
45+
"solc_via_ir": true,
46+
"assert_autofinder_success": true,
47+
"contract_recursion_limit": "1",
48+
"process": "emv",
49+
"prover_args": [
50+
"-cvlFunctionRevert true"
51+
],
52+
"build_cache": true,
53+
"smt_timeout": "6000"
54+
}

‎certora/confs/ConsistentState.conf‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
{
2+
"verify": "EulerEarnHarness:certora/specs/ConsistentState.spec",
3+
"msg": "Euler Earn - Rules about Consistency of State",
4+
"loop_iter": "2",
5+
"exclude_rule" :
6+
[
7+
"notInWithdrawQThenNoApproval",
8+
"addedToSupplyQThenIsInWithdrawQ",
9+
"sanity_notInWithdrawQThenNoApproval"
10+
],
11+
"override_base_config": "certora/confs/BaseConfForInheritance.conf"
12+
}

‎certora/confs/ConsistentStateExtras.conf‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
{
2+
"override_base_config": "certora/confs/BaseConfForInheritance.conf",
3+
"verify": "EulerEarnHarness:certora/specs/ConsistentState.spec",
4+
"msg": "Euler Earn - Rules about Consistency of State",
5+
"loop_iter": "2",
6+
"rule" : [
7+
"addedToSupplyQThenIsInWithdrawQ"
8+
],
9+
"prover_args": [
10+
"-cvlFunctionRevert true",
11+
"-split false"
12+
]
13+
}

‎certora/confs/ConsistentStateExtras2.conf‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
{
2+
"override_base_config": "certora/confs/BaseConfForInheritance.conf",
3+
"verify": "EulerEarnHarness:certora/specs/ConsistentState.spec",
4+
"msg": "Euler Earn - Rules about Consistency of State",
5+
"loop_iter": "2",
6+
"rule" : [
7+
"notInWithdrawQThenNoApproval",
8+
],
9+
"prover_args": [
10+
"-cvlFunctionRevert true",
11+
"-destructiveOptimizations twostage",
12+
"-depth 0"
13+
],
14+
"rule_sanity": "none"
15+
}

‎certora/confs/ConsistentStateExtras3Sanity.conf‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
{
2+
"override_base_config": "certora/confs/BaseConfForInheritance.conf",
3+
"verify": "EulerEarnHarness:certora/specs/ConsistentState.spec",
4+
"msg": "Euler Earn - Rules about Consistency of State",
5+
"loop_iter": "2",
6+
"rule" : [
7+
"sanity_notInWithdrawQThenNoApproval"
8+
],
9+
"prover_args": [
10+
"-cvlFunctionRevert true",
11+
"-destructiveOptimizations twostage",
12+
"-mediumTimeout 20 -lowTimeout 20 -tinyTimeout 20 -depth 20"
13+
],
14+
"rule_sanity": "none"
15+
}

‎certora/confs/Conversions.conf‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
{
2+
"verify": "EulerEarnHarness:certora/specs/ConversionRules.spec",
3+
"msg": "conversion rules",
4+
"rule": [
5+
"conversionOfZero",
6+
"convertToAssetsWeakAdditivity",
7+
"convertToSharesWeakAdditivity",
8+
"conversionWeakMonotonicity",
9+
"conversionWeakIntegrity"
10+
],
11+
"loop_iter": "1",
12+
"optimistic_summary_recursion": true,
13+
"prover_args": [
14+
"-depth 20",
15+
"-cvlFunctionRevert true"
16+
],
17+
"override_base_config": "certora/confs/BaseConfForInheritance.conf"
18+
}

0 commit comments

Comments
 (0)