Skip to content

Commit 773453b

Browse files
kasperpawlowskikasperpawlowski
authored
Merge pull request #32 from euler-xyz/enigma-dark-invariants
Enigma dark invariant suite
2 parents 9ea1e96 + 71d006c commit 773453b

File tree

61 files changed

+6211
-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.

61 files changed

+6211
-1
lines changed

‎.github/workflows/enigma-dark-invariants.yml‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
name: Enigma Dark Invariants - Echidna Workflow
2+
3+
on:
4+
push:
5+
branches:
6+
- master
7+
pull_request:
8+
9+
env:
10+
FOUNDRY_PROFILE: ci
11+
12+
concurrency:
13+
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
14+
cancel-in-progress: true
15+
16+
jobs:
17+
echidna:
18+
runs-on: ubuntu-latest
19+
20+
strategy:
21+
matrix:
22+
mode: [property, assertion] # Define the modes here
23+
24+
steps:
25+
- name: Checkout repository
26+
uses: actions/checkout@v3
27+
with:
28+
submodules: recursive
29+
30+
- name: Install Foundry
31+
uses: foundry-rs/foundry-toolchain@v1
32+
with:
33+
version: nightly
34+
35+
- name: Compile contracts
36+
run: |
37+
forge build test/enigma-dark-invariants/Tester.t.sol --build-info
38+
39+
- name: Run Echidna ${{ matrix.mode == 'property' && 'Property' || 'Assertion' }} Mode
40+
uses: crytic/echidna-action@v2
41+
with:
42+
files: .
43+
contract: Tester
44+
config: test/enigma-dark-invariants/_config/echidna_config_ci.yaml
45+
crytic-args: --ignore-compile
46+
test-mode: ${{ matrix.mode == 'assertion' && 'assertion' || '' }}

‎.gitignore‎

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,5 +14,14 @@ broadcast/
1414
# System Files
1515
.DS_Store
1616

17+
18+
# Invariant testing files
19+
crytic-export/
20+
_corpus/
21+
22+
# Coverage directory
23+
coverage/
24+
*.info
25+
1726
# certora generated files
18-
.certora_internal
27+
.certora_internal

‎Makefile‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
# Invariants
2+
echidna:
3+
echidna test/enigma-dark-invariants/Tester.t.sol --contract Tester --config ./test/enigma-dark-invariants/_config/echidna_config.yaml --corpus-dir ./test/enigma-dark-invariants/_corpus/echidna/default/_data/corpus
4+
5+
echidna-assert:
6+
echidna test/enigma-dark-invariants/Tester.t.sol --contract Tester --test-mode assertion --config ./test/enigma-dark-invariants/_config/echidna_config.yaml --corpus-dir ./test/enigma-dark-invariants/_corpus/echidna/default/_data/corpus
7+
8+
echidna-explore:
9+
echidna test/enigma-dark-invariants/Tester.t.sol --contract Tester --test-mode exploration --config ./test/enigma-dark-invariants/_config/echidna_config.yaml --corpus-dir ./test/enigma-dark-invariants/_corpus/echidna/default/_data/corpus
10+
11+
# Medusa
12+
medusa:
13+
medusa fuzz --config ./medusa.json
14+
15+
# Echidna Results
16+
runes:
17+
runes convert ./test/enigma-dark-invariants/_corpus/echidna/default/_data/corpus/reproducers --output ./test/enigma-dark-invariants/replays

‎medusa.json‎

Lines changed: 87 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,87 @@
1+
{
2+
"fuzzing": {
3+
"workers": 10,
4+
"workerResetLimit": 50,
5+
"timeout": 0,
6+
"testLimit": 0,
7+
"callSequenceLength": 200,
8+
"corpusDirectory": "test/enigma-dark-invariants/_corpus/medusa",
9+
"coverageEnabled": true,
10+
"deploymentOrder": [
11+
"Tester"
12+
],
13+
"targetContracts": [
14+
"Tester"
15+
],
16+
"targetContractsBalances": [
17+
"1e35"
18+
],
19+
"constructorArgs": {},
20+
"deployerAddress": "0x30000",
21+
"senderAddresses": [
22+
"0x10000",
23+
"0x20000",
24+
"0x30000"
25+
],
26+
"blockNumberDelayMax": 60480,
27+
"blockTimestampDelayMax": 604800,
28+
"blockGasLimit": 12500000000,
29+
"transactionGasLimit": 1250000000,
30+
"testing": {
31+
"stopOnFailedTest": false,
32+
"stopOnFailedContractMatching": false,
33+
"stopOnNoTests": true,
34+
"testAllContracts": false,
35+
"traceAll": false,
36+
"assertionTesting": {
37+
"enabled": true,
38+
"testViewMethods": true,
39+
"assertionModes": {
40+
"failOnCompilerInsertedPanic": false,
41+
"failOnAssertion": true,
42+
"failOnArithmeticUnderflow": false,
43+
"failOnDivideByZero": false,
44+
"failOnEnumTypeConversionOutOfBounds": false,
45+
"failOnIncorrectStorageAccess": false,
46+
"failOnPopEmptyArray": false,
47+
"failOnOutOfBoundsArrayAccess": false,
48+
"failOnAllocateTooMuchMemory": false,
49+
"failOnCallUninitializedVariable": false
50+
}
51+
},
52+
"propertyTesting": {
53+
"enabled": true,
54+
"testPrefixes": [
55+
"fuzz_",
56+
"echidna_"
57+
]
58+
},
59+
"optimizationTesting": {
60+
"enabled": false,
61+
"testPrefixes": [
62+
"optimize_"
63+
]
64+
}
65+
},
66+
"chainConfig": {
67+
"codeSizeCheckDisabled": true,
68+
"cheatCodes": {
69+
"cheatCodesEnabled": true,
70+
"enableFFI": false
71+
}
72+
}
73+
},
74+
"compilation": {
75+
"platform": "crytic-compile",
76+
"platformConfig": {
77+
"target": "test/enigma-dark-invariants/Tester.t.sol",
78+
"solcVersion": "",
79+
"exportDirectory": "",
80+
"args": []
81+
}
82+
},
83+
"logging": {
84+
"level": "info",
85+
"logDirectory": ""
86+
}
87+
}

‎test/enigma-dark-invariants/HandlerAggregator.t.sol‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
// SPDX-License-Identifier: MIT
2+
pragma solidity ^0.8.19;
3+
4+
// Admin Handler contracts
5+
import {EulerEarnAdminHandler} from "./handlers/admin/EulerEarnAdminHandler.t.sol";
6+
import {PublicAllocatorAdminHandler} from "./handlers/admin/PublicAllocatorAdminHandler.t.sol";
7+
8+
// EVC Handler contracts
9+
import {EVCHandler} from "./handlers/evc/EVCHandler.t.sol";
10+
11+
// EVK Modules Handler contracts
12+
import {BorrowingModuleHandler} from "./handlers/evk/BorrowingModuleHandler.t.sol";
13+
import {LiquidationModuleHandler} from "./handlers/evk/LiquidationModuleHandler.t.sol";
14+
import {GovernanceModuleHandler} from "./handlers/evk/GovernanceModuleHandler.t.sol";
15+
16+
// User Handler contracts,
17+
import {EulerEarnHandler} from "./handlers/user/EulerEarnHandler.t.sol";
18+
import {PublicAllocatorHandler} from "./handlers/user/PublicAllocatorHandler.t.sol";
19+
20+
// Standard Handler contracts
21+
import {ERC20Handler} from "./handlers/standard/ERC20Handler.t.sol";
22+
import {ERC4626Handler} from "./handlers/standard/ERC4626Handler.t.sol";
23+
24+
// Simulator Handler contracts
25+
import {DonationAttackHandler} from "./handlers/simulators/DonationAttackHandler.t.sol";
26+
import {PriceOracleHandler} from "./handlers/simulators/PriceOracleHandler.t.sol";
27+
28+
// Postcondition Handler contracts
29+
import {ERC4626PostconditionsHandler} from "./handlers/postconditions/ERC4626PostconditionsHandler.t.sol";
30+
31+
/// @notice Helper contract to aggregate all handler contracts, inherited in BaseInvariants
32+
abstract contract HandlerAggregator is
33+
EulerEarnAdminHandler, // Admin handlers
34+
PublicAllocatorAdminHandler,
35+
EulerEarnHandler, // User handlers
36+
PublicAllocatorHandler,
37+
EVCHandler, // EVC handlers
38+
BorrowingModuleHandler, // EVK handlers
39+
LiquidationModuleHandler,
40+
GovernanceModuleHandler,
41+
ERC20Handler, // Standard handlers
42+
ERC4626Handler,
43+
DonationAttackHandler, // Simulator handlers
44+
PriceOracleHandler,
45+
ERC4626PostconditionsHandler // Postcondition handlers
46+
{
47+
/// @notice Helper function in case any handler requires additional setup
48+
function _setUpHandlers() internal {}
49+
}

‎test/enigma-dark-invariants/Invariants.t.sol‎

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
// SPDX-License-Identifier: MIT
2+
pragma solidity ^0.8.19;
3+
4+
// Interfaces
5+
import {IERC4626, IERC20} from "lib/openzeppelin-contracts/contracts/interfaces/IERC4626.sol";
6+
7+
// Invariant Contracts
8+
import {BaseInvariants} from "./invariants/BaseInvariants.t.sol";
9+
import {ERC4626Invariants} from "./invariants/ERC4626Invariants.t.sol";
10+
11+
/// @title Invariants
12+
/// @notice Wrappers for the protocol invariants implemented in each invariants contract
13+
/// @dev recognised by Echidna when property mode is activated
14+
/// @dev Inherits BaseInvariants
15+
abstract contract Invariants is BaseInvariants, ERC4626Invariants {
16+
///////////////////////////////////////////////////////////////////////////////////////////////
17+
// BASE INVARIANTS //
18+
///////////////////////////////////////////////////////////////////////////////////////////////
19+
20+
function echidna_INV_BASE() public returns (bool) {
21+
for (uint256 i; i < eulerEarnVaults.length; i++) {
22+
address eulerEarn_ = eulerEarnVaults[i];
23+
for (uint256 j; j < allMarkets[eulerEarn_].length; j++) {
24+
IERC4626 market = allMarkets[eulerEarn_][j];
25+
assert_INV_BASE_A(market, eulerEarn_);
26+
assert_INV_BASE_C(market, eulerEarn_);
27+
assert_INV_BASE_D(market, eulerEarn_);
28+
assert_INV_BASE_E(market, eulerEarn_);
29+
}
30+
31+
assert_INV_BASE_F(eulerEarn_);
32+
}
33+
34+
return true;
35+
}
36+
37+
function echidna_INV_QUEUES() public returns (bool) {
38+
for (uint256 i; i < eulerEarnVaults.length; i++) {
39+
address eulerEarn_ = eulerEarnVaults[i];
40+
assert_INV_QUEUES_AE(eulerEarn_);
41+
assert_INV_QUEUES_B(eulerEarn_);
42+
}
43+
44+
return true;
45+
}
46+
47+
function echidna_INV_TIMELOCK() public returns (bool) {
48+
for (uint256 i; i < eulerEarnVaults.length; i++) {
49+
address eulerEarn_ = eulerEarnVaults[i];
50+
assert_INV_TIMELOCK_A(eulerEarn_);
51+
assert_INV_TIMELOCK_D(eulerEarn_);
52+
assert_INV_TIMELOCK_E(eulerEarn_);
53+
assert_INV_TIMELOCK_F(eulerEarn_);
54+
}
55+
56+
return true;
57+
}
58+
59+
function echidna_INV_MARKETS() public returns (bool) {
60+
for (uint256 i; i < eulerEarnVaults.length; i++) {
61+
address eulerEarn_ = eulerEarnVaults[i];
62+
for (uint256 j; j < allMarkets[eulerEarn_].length; j++) {
63+
assert_INV_MARKETS_AB(allMarkets[eulerEarn_][j], eulerEarn_);
64+
}
65+
}
66+
67+
return true;
68+
}
69+
70+
function echidna_INV_FEES() public returns (bool) {
71+
for (uint256 i; i < eulerEarnVaults.length; i++) {
72+
assert_INV_FEES_A(eulerEarnVaults[i]);
73+
}
74+
75+
return true;
76+
}
77+
78+
function echidna_INV_ACCOUNTING() public returns (bool) {
79+
for (uint256 i; i < eulerEarnVaults.length; i++) {
80+
address eulerEarn_ = eulerEarnVaults[i];
81+
assert_INV_ACCOUNTING_A(eulerEarn_);
82+
}
83+
84+
return true;
85+
}
86+
87+
///////////////////////////////////////////////////////////////////////////////////////////////
88+
// ERC4626 INVARIANTS //
89+
///////////////////////////////////////////////////////////////////////////////////////////////
90+
91+
function echidna_ERC4626_ASSETS_INVARIANTS() public returns (bool) {
92+
for (uint256 i; i < eulerEarnVaults.length; i++) {
93+
address eulerEarn_ = eulerEarnVaults[i];
94+
assert_ERC4626_ASSETS_INVARIANT_A(eulerEarn_);
95+
assert_ERC4626_ASSETS_INVARIANT_B(eulerEarn_);
96+
assert_ERC4626_ASSETS_INVARIANT_C(eulerEarn_);
97+
assert_ERC4626_ASSETS_INVARIANT_D(eulerEarn_);
98+
}
99+
100+
return true;
101+
}
102+
103+
function echidna_ERC4626_USERS() public returns (bool) {
104+
for (uint256 i; i < eulerEarnVaults.length; i++) {
105+
address eulerEarn_ = eulerEarnVaults[i];
106+
for (uint256 j; j < actorAddresses.length; j++) {
107+
assert_ERC4626_DEPOSIT_INVARIANT_A(actorAddresses[j], eulerEarn_);
108+
assert_ERC4626_MINT_INVARIANT_A(actorAddresses[j], eulerEarn_);
109+
assert_ERC4626_WITHDRAW_INVARIANT_A(actorAddresses[j], eulerEarn_);
110+
assert_ERC4626_REDEEM_INVARIANT_A(actorAddresses[j], eulerEarn_);
111+
}
112+
}
113+
114+
return true;
115+
}
116+
}

‎test/enigma-dark-invariants/README.md‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
# Actor Based Invariant Testing Suite
2+
3+
<img src="./docs/invariant-suite-overview.png" alt="Enigma Dark suite" width="90%" height="75%">
4+
5+
<br/>
6+
7+
Developed by [vnmrtz.eth](https://x.com/vn_martinez_) from [Enigma Dark](https://www.enigmadark.com/).
8+
9+
<br/>
10+
11+
The Actor Based Invariant Testing Suite is a framework for performing comprehensive invariant testing of the Silo Vaults protocol. Using an actor-based model, it simulates realistic scenarios with various entities interacting with the system, ensuring that protocol invariants and postconditions hold under an extensive range of conditions.
12+
13+
The suite is designed to support multi-actor tooling, randomizing actions, parameters, actor roles, and asset selection to explore edge cases and ensure the robustness of a protocol.
14+
15+
# Specifications
16+
17+
Extensive documentation regarding the architecture and design of the suite can be found [HERE](./docs/overview.md).
18+
19+
Further documentation outlining the properties of the system (both invariants and postconditions) can be found [HERE](./specs/).
20+
21+
# Tooling
22+
23+
The suite has been developed and tested using the following tools:
24+
25+
- [Echidna](https://github.com/crytic/echidna): A battle tested property-based testing tool for Ethereum smart contracts.
26+
27+
# Setup Instructions:
28+
29+
Instructions for setting up the project and running the testing suite with echidna are available [HERE](./docs/internal-docs.md).
30+
31+
## Additional notes
32+
33+
- Ensure you have the latest version of dependencies both tooling and protocol dependencies installed before running the tests.
34+
- The suite is designed to be modular and extensible, allowing for easy integration of new properties and actors.
35+
- The suite supports integration with github actions, allowing for automated testing as part of the development workflow.
36+
37+
This suite was developed by Enigma Dark after being engaged by Silo Labs to provide security services for the silo v2 vaults protocol, ensuring that best practices in security and testing are satisfied.

0 commit comments

Comments
 (0)