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.