Byth

<p align="center"> <img src="public/byth.jpg" alt="Byth is the symbolic indexer for Ethereum."/> </p>

Byth is an EVM indexer which uses halmos to formally verify bytecode using detectors written in Solidity. It helps you to discover vulnerable contracts using customizable detectors.

[!IMPORTANT] Byth is experimental! Use at your own risk.

Configuration

To compile and run this project, you'll need to install the Rust Toolchain:

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh

You also need Foundry installed:

curl -L https://foundry.paradigm.xyz | bash

Finally, install Halmos:

pip3 install halmos

Discovering Vulnerabilities

You can plug in your own custom detector logic to Byth easily. Just install the Byth Bindings to your Foundry tests:

forge install cawfree/byth --no-commit

Then add the remapping:

@byth/=byth/bindings/src/

Finally, inherit from BythTest.sol:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;

import {Test} from "forge-std/Test.sol";
import {SymTest} from "@halmos-cheatcodes/SymTest.sol";
import {BythTest} from "@byth/BythTest.sol";

contract MyCustomDetector is Test, SymTest, BythTest {

    address internal _hook /* contract_under_test */;

    /// @notice Setup phase. Here Byth will inject deployment bytecode
    ///         via the `_createBythHook()` call, so you don't want to
    ///         do this frequently.
    function setUp() public {
        _hook = _createBythHook() /* initalize_contract_under_test */;
    }

    /// @notice Then write your symbolic detectors! The convention is if your
    ///         test passes, it is considered vulnerable. Failures or timeouts
    ///         are considered as immune to the detector vulnerability.
    function check_stealTheMoney(bytes memory someSymbolicFunctionCall) public {
        assert(address(this).balance == 0);
        (bool success,) = _hook.call(someSymbolicFunctionCall);
        assert(success);
        assert(address(this).balance > 0);
    }

}

Then you can start discovering vulnerabilities!

cargo run observe \
  --rpc-url $ETH_RPC_URL \
  --project ../custom_detector_project \ # your_project_name
  --debug \
  --block-number $ETH_BLOCK_NUMBER

[!TIP] For a real-world example, check out this detector for the ThirdWeb vulnerability!

You can also use --project detectors_default to access the built-in detectors.