Enigmadark invariant suite

.github/workflows/echidna-enigma-invariants.yml

@@ -0,0 +1,46 @@
+name: Echidna Enigma Invariants
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+
+env:
+  FOUNDRY_PROFILE: ci
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  echidna:
+    runs-on: ubuntu-latest
+
+    strategy:
+      matrix:
+        mode: [property, assertion] # Define the modes here
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+
+      - name: Compile contracts
+        run: |
+          forge build --build-info
+
+      - name: Run Echidna ${{ matrix.mode == 'property' && 'Property' || 'Assertion' }} Mode
+        uses: crytic/echidna-action@v2
+        with:
+          files: .
+          contract: Tester
+          config: test/enigma-dark-invariants/_config/echidna_config_ci.yaml
+          crytic-args: --ignore-compile
+          test-mode: ${{ matrix.mode == 'assertion' && 'assertion' || '' }}

.github/workflows/test.yml

@@ -2,8 +2,9 @@ name: CI
 
 on:
   push:
+    branches:
+      - master
   pull_request:
-  workflow_dispatch:
 
 env:
   FOUNDRY_PROFILE: ci

.gitignore

@@ -11,4 +11,11 @@ out/
 .env
 
 # Coverage file
-lcov.info
+lcov.info
+
+# echidna
+_corpus/
+crytic-export/
+
+.DS_Store
+.vscode

Makefile

@@ -0,0 +1,13 @@
+# Invariants
+echidna:
+	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
+
+echidna-assert:
+	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
+
+echidna-explore:
+	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
+
+# Medusa
+medusa:
+	medusa fuzz --config ./medusa.json

test/enigma-dark-invariants/CryticToFoundry.t.sol

@@ -0,0 +1,110 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Libraries
+import "forge-std/Test.sol";
+import "forge-std/console.sol";
+
+// Contracts
+import {Invariants} from "./Invariants.t.sol";
+import {Setup} from "./Setup.t.sol";
+
+/*
+ * Test suite that converts from  "fuzz tests" to foundry "unit tests"
+ * The objective is to go from random values to hardcoded values that can be analyzed more easily
+ */
+contract CryticToFoundry is Invariants, Setup {
+    CryticToFoundry Tester = this;
+
+    modifier setup() override {
+        _;
+    }
+
+    function setUp() public {
+        // Deploy protocol contracts
+        _setUp(Curve.EULER_SWAP);
+
+        // Initialize handler contracts
+        _setUpHandlers();
+
+        // Initialize hook contracts
+        _setUpHooks();
+
+        /// @dev fixes the actor to the first user
+        actor = actors[USER1];
+
+        vm.warp(101007);
+    }
+
+    ///////////////////////////////////////////////////////////////////////////////////////////////
+    //                                  POSTCONDITIONS REPLAY                                    //
+    ///////////////////////////////////////////////////////////////////////////////////////////////
+
+    function test_replaySwap() public {
+        Tester.mint(2000000, 0, 0);
+        Tester.swap(1, 0, 0, 0, 0); //@audit-issue is possible to extract value from the protocol 1 wei of value
+    }
+
+    function test_replay_swap() public {
+        Tester.swap(0, 1, 0, 0, 0); //@audit-issue is possible to extract value from the protocol 1 wei of value -> rounding down on fx and fy functions fx(y) == fx(y-1) -> HSPOST_SWAP_A
+    }
+
+    function test_replay_nav() public {
+        //@audit-issue when price changes user lp looses nav after a trade
+        Tester.setPrice(1, 0.1 ether);
+        Tester.swap(10, 0, 0, 10, 0);
+    }
+
+    function test_replay_roundtripswap() public {
+        Tester.donateUnderlying(300000000000, 0);
+        Tester.roundtripSwap(100000000, 0); // @audit-issue user receives the amount donated -> HSPOST_SWAP_B
+    }
+
+    function test_replay_swap_roundtripswap() public {
+        //@audit-issue user gets 1 wei more one the swap back -> HSPOST_SWAP_B
+        Tester.swap(15167520363383348756138763841789458381, 16455119106352766170018672268887607023990, 2, 0, 0);
+        Tester.roundtripSwap(200000000, 0);
+    }
+
+    ///////////////////////////////////////////////////////////////////////////////////////////////
+    //                                     INVARIANTS REPLAY                                     //
+    ///////////////////////////////////////////////////////////////////////////////////////////////
+
+    ///////////////////////////////////////////////////////////////////////////////////////////////
+    //                                 BROKEN INVARIANTS REPLAY                                  //
+    ///////////////////////////////////////////////////////////////////////////////////////////////
+
+    ///////////////////////////////////////////////////////////////////////////////////////////////
+    //                                           HELPERS                                         //
+    ///////////////////////////////////////////////////////////////////////////////////////////////
+
+    /// @notice Fast forward the time and set up an actor,
+    /// @dev Use for ECHIDNA call-traces
+    function _delay(uint256 _seconds) internal {
+        vm.warp(block.timestamp + _seconds);
+    }
+
+    /// @notice Set up an actor
+    function _setUpActor(address _origin) internal {
+        actor = actors[_origin];
+    }
+
+    /// @notice Set up an actor and fast forward the time
+    /// @dev Use for ECHIDNA call-traces
+    function _setUpActorAndDelay(address _origin, uint256 _seconds) internal {
+        actor = actors[_origin];
+        vm.warp(block.timestamp + _seconds);
+    }
+
+    /// @notice Set up a specific block and actor
+    function _setUpBlockAndActor(uint256 _block, address _user) internal {
+        vm.roll(_block);
+        actor = actors[_user];
+    }
+
+    /// @notice Set up a specific timestamp and actor
+    function _setUpTimestampAndActor(uint256 _timestamp, address _user) internal {
+        vm.warp(_timestamp);
+        actor = actors[_user];
+    }
+}

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

@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// modules Actions Handler contracts,
+import {EVCHandler} from "./handlers/euler/EVCHandler.t.sol";
+import {ERC20Handler} from "./handlers/standard/ERC20Handler.t.sol";
+import {ERC4626Handler} from "./handlers/standard/ERC4626Handler.t.sol";
+import {MaglevHandler} from "./handlers/swap/MaglevHandler.t.sol";
+
+// Simulator Handler contracts,
+import {DonationAttackHandler} from "./handlers/simulators/DonationAttackHandler.t.sol";
+import {PriceOracleHandler} from "./handlers/simulators/PriceOracleHandler.t.sol";
+
+/// @notice Helper contract to aggregate all handler contracts, inherited in BaseInvariants
+abstract contract HandlerAggregator is
+    EVCHandler, // Euler handlers
+    ERC20Handler, // Module handlers
+    ERC4626Handler,
+    MaglevHandler,
+    DonationAttackHandler, // Simulator handlers
+    PriceOracleHandler
+{
+    /// @notice Helper function in case any handler requires additional setup
+    function _setUpHandlers() internal {}
+}

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

@@ -0,0 +1,24 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Interfaces
+import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+
+// Invariant Contracts
+import {BaseInvariants} from "./invariants/BaseInvariants.t.sol";
+
+/// @title Invariants
+/// @notice Wrappers for the protocol invariants implemented in each invariants contract
+/// @dev recognised by Echidna when property mode is activated
+/// @dev Inherits BaseInvariants
+abstract contract Invariants is BaseInvariants {
+    ///////////////////////////////////////////////////////////////////////////////////////////////
+    //                                     BASE INVARIANTS                                       //
+    ///////////////////////////////////////////////////////////////////////////////////////////////
+
+    function echidna_BASE_ASSETS_INVARIANTS() public returns (bool) {
+        assert_INV_BASE_A();
+
+        return true;
+    }
+}

test/enigma-dark-invariants/README.md

@@ -0,0 +1,37 @@
+# Actor Based Invariant Testing Suite
+
+<img src="./docs/invariant-suite-overview.png" alt="Enigma Dark suite" width="90%" height="75%">
+
+<br/>
+
+Developed by [vnmrtz.eth](https://x.com/vn_martinez_) from [Enigma Dark](https://www.enigmadark.com/).
+
+<br/>
+
+The Actor Based Invariant Testing Suite is a framework for performing comprehensive invariant testing of the Euler Maglev 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.
+
+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.
+
+# Specifications
+
+Extensive documentation regarding the architecture and design of the suite can be found [HERE](./docs/overview.md).
+
+Further documentation outlining the properties of the system (both invariants and postconditions) can be found [HERE](./specs/).
+
+# Tooling
+
+The suite has been developed and tested using the following tools:
+
+- [Echidna](https://github.com/crytic/echidna): A battle tested property-based testing tool for Ethereum smart contracts.
+
+# Setup Instructions:
+
+Instructions for setting up the project and running the testing suite with echidna are available [HERE](./docs/internal-docs.md).
+
+## Additional notes
+
+- Ensure you have the latest version of dependencies both tooling and protocol dependencies installed before running the tests.
+- The suite is designed to be modular and extensible, allowing for easy integration of new properties and actors.
+- The suite supports integration with github actions, allowing for automated testing as part of the development workflow.
+
+This suite was developed by Enigma Dark after being engaged by Euler Labs to provide security services for the Euler v2 protocol, ensuring that best practices in security and testing are satisfied.