# The Easy Way To Quit (Concrete) Testing Author: [Palina Tolmach](https://twitter.com/palinatolmach) *This blog post serves as the second installment of a two-part series exploring the concept of symbolic execution for smart contracts. For background information on symbolic execution and an overview of existing tools for Ethereum smart contracts verification, be sure to check out [part one](https://hackmd.io/@SaferMaker/EVM-Sym-Exec)!* In this post, we will dive into the topic of *symbolic testing*. The first half of this post will provide a comprehensive review of existing tools that support symbolic testing for EVM smart contracts. In the second half, we'll share our own experience of integrating [EthBMC](https://github.com/RUB-SysSec/EthBMC)—one of the top-performing tools from part one—with the [Foundry](https://github.com/foundry-rs/foundry) development framework to enable symbolic testing. ## What is symbolic testing? [Symbolic execution](https://hackmd.io/@SaferMaker/EVM-Sym-Exec#What-is-symbolic-execution) provides an effective way to identify potential vulnerabilities in smart contracts by analyzing multiple execution paths simultaneously. However, it can also be limited by scalability and usability problems. *Symbolic testing* partially addresses these issues by analyzing *tests* using symbolic inputs rather than systematically examining all possible sequences of function calls made to the smart contract. Symbolic testing also allows [reusing existing unit or fuzz tests for formal analysis](https://a16zcrypto.com/content/article/symbolic-testing-with-halmos-leveraging-existing-tests-for-formal-verification/), removing the necessity to separately define specifications, a labor-intensive blocker for adoption. Last but not least, symbolic testing also takes advantage of the `setUp()` function that is usually supported by testing frameworks such as Foundry, which helps (concretely) set up the initial state for the analysis; this feature is particularly useful for symbolic execution tools like [hevm](https://github.com/ethereum/hevm) and [EthBMC](https://github.com/RUB-SysSec/EthBMC) that analyze runtime bytecode, which does not include constructor logic. Let's consider a simple smart contract example from [the previous post](https://hackmd.io/@SaferMaker/EVM-Sym-Exec#Symbolic-Execution-by-Example). The contract is based on the code included in an [issue](https://github.com/foundry-rs/foundry/issues/2851) from the Foundry repository titled `condition not caught by invariant/fuzzer`. We're interested in the assert on line 15, which should fail if the function is called with `x` being equal to 6912213124124532 (6912213124124531 + 1). ```solidity= pragma solidity ^0.8.17; contract PostExample { // https://github.com/foundry-rs/foundry/issues/2851 function backdoor(uint256 x) external pure { uint256 number = 99; unchecked { uint256 z = x - 1; if (z == 6912213124124531) { number = 0; } else { number = 1; } } assert(number != 0); } } ``` As indicated by the issue title, [Foundry](https://github.com/foundry-rs/foundry)---a popular Rust-based development framework---offers support for [fuzz testing](https://about.gitlab.com/topics/devsecops/what-is-fuzz-testing/). When given a test that takes an least one parameter, Foundry uses [fuzzing](https://owasp.org/www-community/Fuzzing) to analyze it, i.e., Foundry runs the test multiple times with different randomized concrete inputs; those are usually generated based on a set of heuristics. For instance, `testBackdoor(uint256 x)` in line 11 of the `PostExampleTest` contract below corresponds to a test that, in turn, calls the `backdoor(uint256 x)` function from `PostExample` with the same argument `x`. Running `forge test` will initiate the fuzzing of this test. In case the input generation strategy produces `6912213124124532` as input, the assert in line 15 of `PostExample` will fail and the test will not pass. ```solidity= import "forge-std/Test.sol"; import "../src/PostExample.sol"; contract PostExampleTest is Test { PostExample public example; function setUp() public { example = new PostExample(); } function testBackdoor(uint256 x) public view { example.backdoor(x); } } ``` However, Foundry's fuzzer cannot pinpoint the input that triggers this assert violation (this happens due to its restricted data-flow reasoning capabilities---if we change `z = x - 1` to `z = x` in line 8 of `PostExample`, Foundry's fuzzer will successfully identify the issue). ![](https://i.imgur.com/5mvqmvO.png) At the same time, as demonstrated in the previous post, symbolic execution tools successfully identify the `backdoor` function's assert violation in a few seconds at most, and can, therefore, be applied in this setting as well. ## What tools are there? In this post, we evaluate the tools based on their ability to symbolically analyze tests written as part of the Foundry project. We will briefly discuss the structure of Foundry projects in the [Setup](#Setup) section below; for more information on Foundry, please refer to [its documentation](https://book.getfoundry.sh/). To the best of our knowledge, symbolic testing of the Ethereum smart contracts is only supported by the following tools, which we evaluate in this post: [hevm](https://github.com/ethereum/hevm) A symbolic execution engine and equivalence checker for EVM bytecode, extensively analyzed in the previous post. Initially developed as part of the [dapptools](https://github.com/dapphub/dapptools) framework, hevm has been forked by the Ethereum Foundation and is currently under active development---we are using the newer Ethereum Foundation fork for our experiments. hevm is implemented in Haskell and supports Z3 and cvc5 as solvers. hevm was one of the earliest tools to support symbolic analysis of unit tests for EVM smart contracts via its integration with the [dapp-test](https://github.com/dapphub/dapptools/tree/master/src/dapp#dapp-test) framework; it has also [recently added](https://github.com/ethereum/hevm/commit/c66e8830cf1dfbcc64bea4659962f90daf4e22aa) support for symbolic testing of Foundry projects. <!-- that uses [ds-test](https://github.com/dapphub/ds-test/) (which is also partially reused by Foundry). --> [Halmos](https://github.com/a16z/halmos/) A [symbolic bounded model checker](https://a16zcrypto.com/content/article/symbolic-testing-with-halmos-leveraging-existing-tests-for-formal-verification/) designed for symbolic testing of Ethereum smart contract bytecode. Halmos is developed by a16z, is implemented in Python, and supports Z3 SMT solver through its Python API. [KEVM Foundry](https://github.com/runtimeverification/evm-semantics/blob/master/include/kframework/foundry.md) [KEVM](https://github.com/runtimeverification/evm-semantics) implements a formal semantics (i.e., a model) of the EVM defined with the [K Framework](https://kframework.org/), which, among other things, can be used to perform symbolic execution of smart contract bytecode. KEVM can symbolically execute Foundry tests, [supports an extensive list of Foundry cheatcodes](https://github.com/runtimeverification/evm-semantics/blob/3c3608af4134c4da4056b6b8046c53da08785c29/include/kframework/foundry.md#foundry-cheat-codes), and defines [several additional ones](https://github.com/runtimeverification/foundry-demo/blob/master/src/utils/KEVMCheats.sol). K, upon which KEVM is built, is a general framework for the development of formal semantics and verification, and, different from all other tools reviewed in this and the previous post, is not limited to EVM. Therefore, the same symbolic execution module that is applied to Ethereum smart contracts can also be used to analyze smart contracts running on other platforms, such as [Algorand](https://runtimeverification.com/blog/runtime-verification-brings-formal-verification-to-algorand), [WASM](https://github.com/runtimeverification/wasm-semantics), and some others. KEVM relies on Z3 as an SMT solver, with the underlying K framework implemented in several programming languages, including Python, Haskell, LLVM, C/C++, and Haskell. [EthBMC](https://github.com/baolean/EthBMC/tree/forge) A symbolic bounded model checker for EVM bytecode [developed in Ruhr-University Bochum](https://www.usenix.org/system/files/sec20-frank.pdf), EthBMC was thoroughly investigated in our previous post. This time, we examine its symbolic testing capabilities based on our own experimental integration of EthBMC with (an [instrumented version](https://github.com/baolean/foundry/tree/symexec) of) Foundry. EthBMC is implemented in Rust and supports several SMT solvers (Z3, Yices2, Boolector). Two other verification tools that are capable of analyzing Foundry projects are [Mythril](https://github.com/ConsenSys/mythril)---a symbolic execution-based security analysis tool for EVM bytecode---and [SMTChecker](https://docs.soliditylang.org/en/v0.8.17/smtchecker.html)---a Solidity smart contract verifier that is shipped together with the compiler. Both of these tools, however, analyze the source code of the smart contract implementation but not the tests defined for it, so we do not consider them today. <!-- Has a recent commit related to the support of Foundry analysis now too. However, it analyzes the contract (and not the test contract) itself; plus, it requires setting `out = 'artifacts/contracts` (instead of the default `out = 'out'` in `[profile.default]` of `foundry.toml` file). It can be run using `myth f` (or `myth foundry`). A security analysis tool for EVM bytecode that performs vulnerability detection using symbolic execution. Mythril is developed by ConsenSys. It’s implemented in Python and uses Z3 as an SMT solver through its Python API. --> ## What can they do? Let's take a look at how these tools can be used to analyze *tests* written for Ethereum smart contracts using Foundry. All experiments described in this post were performed on a DigitalOcean droplet with Ubuntu 22.04, 32 GB of RAM, and 4 CPUs. When run in Docker (as suggested in the "follow along" snippets), you *may* see degraded performance depending on the amount of resources allocated to your containers. ### Setup To follow along, you can pull pre-built Docker images using the following commands: ``` docker pull baolean/halmos:latest docker pull baolean/kevm:latest docker pull baolean/hevm-symtest:latest docker pull baolean/ethbmc-forge:latest ``` You can find these container images in [this Docker Hub registry](https://hub.docker.com/u/baolean). Since all symbolic testing tools that we evaluate support the analysis of tests written using Foundry, we will be using a Foundry project for the experiments throughout this post. The project that includes all code used for the evaluation is available in the `symtest` branch of the [`symexec-bench`](https://github.com/baolean/symexec-bench/tree/symtest) repository under the [`SymTest`](https://github.com/baolean/symexec-bench/tree/symtest/SymTest) folder. Most of the tools considered in this post rely on the compilation artifacts produced by Foundry---to generate the corresponding files, we should execute`forge build` in the project folder. To clone and build the project, run: ``` git clone https://github.com/baolean/symexec-bench.git && \ cd symexec-bench && \ git checkout symtest -- && \ cd SymTest && forge build ``` The `/src` folder contains the smart contract implementations that we will be examining, while `/test` includes the contracts defining tests that will be symbolically analyzed. Each test contract should be inherited from [`forge-std/src/Test.sol`](https://github.com/foundry-rs/forge-std/blob/master/src/Test.sol), which provides access to cheatcodes, an extended set of assertions, and other functionality that facilitates testing. Test contracts in Foundry also contain a `setUp()` function that is used to create smart contracts involved in the tests as well as to setup an initial state, from which the analysis will be performed. We expect that the examined tools should respect `setUp()` and use the result of its execution as the initial state; this functionality is particularly helpful for the tools that perform runtime bytecode analysis, such as hevm and EthBMC, as it provides a straightforward way to initialize the contract state in the absence of a constructor. <!-- That's a guide to creating a Foundry project: As an alternative to cloning the existing repository, you can set up a new Foundry project by running `forge init` in an empty directory. If you want to reproduce some of the experiments locally, create a Foundry project first with `mkdir ...`, `forge init`. Then add files that you want, and run `forge build`. You can run `forge test` to make sure it works. Tests should start with `test` or `invariant` (*todo: check that*); the ones that have parameters will be fuzzed. The project can be setup with `foundry.toml`. --> <!-- The project should be built with `forge build`. --> After you have cloned the `symexec-bench` repository and entered its `SymTest` directory, you can run the Docker containers with the current `SymTest` folder mounted in the `/SymTest` directory in the container. Assuming that your current directory (`pwd`) is the `symexec-bench/SymTest` folder, the command would look like this: ```shell docker run -it --rm --platform linux/amd64 \ -v $(pwd):/SymTest baolean/hevm-symtest:latest ``` Try running `hevm version` to verify that everything works. To exit the container, type `exit` and press enter. Thanks to `--rm` flag, the container (but not the image) will self-destruct upon exit, so you won't have to clean up afterwards. Detailed steps to install all the tools that we examine in this post can be found in the Dockerfiles we prepared for [Halmos](https://github.com/baolean/halmos/blob/bcae566a5801949f5fa55c06fe34c8c3e9673f23/Dockerfile), [hevm](https://github.com/baolean/hevm/blob/ffb24acb2cd96786e432468fae84d9f3aa05d460/Dockerfile), [EthBMC/Foundry](https://github.com/baolean/EthBMC/blob/5e8657d28b6c7b8218db46ec235058a1bc1afd34/Dockerfile), and [KEVM](https://github.com/baolean/evm-semantics/blob/cccf115d47f61cdfaee62887ca5636cea0df18ba/Dockerfile). If you prefer, you can build the images from scratch by running ```shell docker build -t IMAGE_NAME . ``` in the respective cloned repository, or just install the tools directly on your machine. All tools considered in this post perform symbolic analysis of test functions that follow a certain naming convention: hevm and EthBMC/Foundry symbolically execute functions that start with `prove`, while Halmos and KEVM target the ones beginning with `test`. ### Simple Example First, let’s compare the selected tools based on the `testBackdoor(uint256 x)` function that analyzes the behavior of the `PostExample` contract from the introduction: ```solidity function testBackdoor(uint256 x) public view { example.backdoor(x); } ``` The code of the `PostExample` smart contract is available in [`src/PostExample.sol`](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/src/PostExample.sol), while the tests are located in [`test/PostExample.t.sol`](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/test/PostExample.t.sol). **Halmos** symbolically executes functions that start with the`test` keyword and will, therefore, analyze `testBackdoor` symbolically. To follow along, enter the Docker container by running: ```shell docker run -it --rm --platform linux/amd64 \ -v $(pwd):/SymTest baolean/halmos:latest ``` In the container, run the following commands to enter the `SymTest` folder with the Foundry project we will be analyzing and, then, recompile its source files: ``` cd SymTest && forge build --force ``` Now, to run Halmos on the `PostExampleTest` smart contract that contains the definitions of test functions, run the following command in the project folder: ``` halmos --contract PostExampleTest ``` The analysis successfully completes in less than 5 seconds, with the output showing the correctly identified value of the input variable `x` leading to the assert violation: ![](https://i.imgur.com/J4OQGpf.png) The option `--contract` we used in the command above restricts the analysis performed in this run of Halmos to a specific test contract, `PostExampleTest`. Running `halmos` without `--contract` would initiate the analysis of all functions prefixed with `test`. In a similar fashion, we can use **hevm** to symbolically analyze test functions in a Foundry project by running `hevm test` in the project repository. In contrast to Halmos, hevm symbolically executes functions that are prefixed with `prove` instead of `test`---that is necessary to distinguish symbolic tests from the ones that should be analyzed concretely and using fuzzing; therefore, we have [added](https://github.com/baolean/symexec-bench/blob/5879dcc1fad23fd0d63478fc50dc6c09653aab7e/SymTest/test/PostExample.t.sol#L18) a `proveBackdoor` function to our test contract as well: ```solidity function proveBackdoor(uint256 x) public view { example.backdoor(x); } ``` To use hevm in a Docker container, run: ```shell docker run -it --rm --platform linux/amd64 \ -v $(pwd):/SymTest baolean/hevm-symtest:latest ``` Similar to how we set up the environment in the Halmos container, execute the following commands to enter the directory with the analyzed Foundry project and recompile it: ``` cd SymTest && forge build --force ``` `hevm test` uses the `--match` option to specify the test or the contract to be analyzed; the instructions on its usage are available in the [dapptools documentation](https://github.com/dapphub/dapptools/blob/master/src/dapp/README.md#dapp-test). To analyze `PostExampleTest`, we can run: ``` hevm test --match PostExampleTest ``` In just 1.5 seconds, hevm reports a revert that happens in `proveBackdoor` with the Panic code 1, which [corresponds to a failed assertion](https://docs.soliditylang.org/en/v0.8.19/control-structures.html#panic-via-assert-and-error-via-require) in Solidity versions >= 0.8: ![](https://i.imgur.com/2gA4bWa.png) The output shown on the screenshot above also reports on `testBackdoor(uint256)` analyzed using fuzzing (as can be seen from the results, 100 runs performed by hevm are insufficient to identify the input triggering the violation). Besides, you may notice that, different from the results produced by `hevm symbolic` in the previous post, `hevm test` returns concrete (decoded) calldata, and does not require a user to provide the runtime binary of the analyzed contract, which significantly improves the user experience. Driven by a similar motivation, we implemented an experimental integration of **EthBMC** with Foundry to support symbolic testing within the Foundry framework itself. Based on the findings of our previous post, EthBMC performs well on the experimental smart contracts, but its user-friendliness is hindered by the necessity for users to provide a runtime binary in a particular configuration file, and the requirement to decode the returned counterexample calldata. The integration of EthBMC with Foundry partially solves this usability issue: we leverage Foundry to automatically compile Solidity code of the analyzed smart contracts, send it to EthBMC for processing, and decode the results of the symbolic execution returned from it. EthBMC also uses the state of the test contract after `setUp()` as the initial state for the analysis. Symbolic testing performed by the EthBMC/Foundry integration can be configured in the [`foundry.toml`](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/foundry.toml#L14) file located in the root of a Foundry project in the following manner: ```yaml= [symbolic] symbolic_storage = false concrete_validation = true solver_timeout = 120_000 solver = 2 # 0: z3, 1: boolector, 2: yices2 loop_bound = 256 call_bound = 1 ``` We describe our experience of developing this integration in the [second part of this post](#Bonus-Section-The-Hitchhiker’s-Guide-to-Foundry-Integration). To evaluate EthBMC with respect to symbolic testing functionality, we run an instrumented version of Foundry available in [this repository](https://github.com/baolean/foundry/tree/symexec). The installation instructions are also provided [later in the post](#Bonus-Section-The-Hitchhiker’s-Guide-to-Foundry-Integration). To run EthBMC/Foundry using Docker, you can enter the container as well as the Foundry project directory by executing the following commands: ``` docker run -it --rm --platform linux/amd64 \ -v $(pwd):/SymTest baolean/ethbmc-forge:latest cd SymTest && forge build --force ``` Much like hevm, EthBMC/Foundry symbolically analyzes tests that start with the `prove` keyword---such tests are symbolically executed by EthBMC once the following command is run in the project folder: ``` forge test --match-contract PostExampleTest ``` where the optional `--match-contract` argument provides the name of the test contract that should be analyzed, similar to the `--match` option in hevm. In 1.1 seconds, this command returns the (decoded!) input leading to the assert violation that happens within `proveBackdoor`---note that this execution time also includes the fuzzing of the `testBackdoor` function performed by Foundry in the same run. For this evaluation, we reduce the number of fuzz runs to 100---the default value used by hevm. ![](https://i.imgur.com/2Y5kHdr.png) The fourth symbolic testing tool that we examined, **KEVM**, symbolically analyzes test functions that start with `test`, like Halmos. At the moment, KEVM does not automatically run `setUp()` at the beginning of the analysis, as other tools do---therefore, we manually invoke `setUp()` in body of the test function. The test contract analyzed by KEVM looks like this: ```solidity= contract PostExampleTest is Test { PostExample public example; function setUp() public { example = new PostExample(); } ... function testBackdoor_k(uint256 x) public { setUp(); example.backdoor(x); } } ``` For every test function we have defined in the `SymTest/test` repository, we have added [a counterpart](https://github.com/baolean/symexec-bench/blob/5879dcc1fad23fd0d63478fc50dc6c09653aab7e/SymTest/test/PostExample.t.sol#L23) containing a call to `setUp()`. Such tests are postfixed with `_k` (as they are meant to be analyzed with KEVM) and by default are commented out---otherwise, they would also be analyzed by other tools considered in this evaluation. To follow along using the Docker container, run: ``` docker run -it --rm --platform linux/amd64 \ -v $(pwd):/SymTest baolean/kevm:latest cd SymTest && forge build --force ``` The process of symbolic testing with KEVM consists of two steps. First, we need to build the K definition for the analyzed test suite by executing the following command in the project folder: ``` kevm foundry-kompile --require lemmas.k \ --module-import DEMO-LEMMAS ``` The command also makes use of some lemmas (`lemmas.k`) defined to facilitate the analysis; we have [included this file](https://github.com/baolean/symexec-bench/blob/5879dcc1fad23fd0d63478fc50dc6c09653aab7e/SymTest/lemmas.k) in the test project (it is also available [in this repository](https://github.com/runtimeverification/foundry-demo/blob/c02c0470729cad4d02e6c5cabcd20ad963132ee1/lemmas.k)). If the contracts are modified later on, execute `forge build` and use a `--regen` flag when building a K definition to update it, i.e., ```` forge build && \ kevm foundry-kompile --require lemmas.k \ --module-import DEMO-LEMMAS --regen ```` The compilation of our whole test project took a bit less than 3 minutes: ![](https://i.imgur.com/i1nCAuB.png) Note that `foundry-kompile` produces compilation artifacts that are added to the `/out` folder, which normally only contains the files generated by `forge build`. Other tools, such as hevm, perform the analysis based on the files present in this directory and might complain about the ones generated by KEVM or another tool. If that happens, the original contents of `/out` can be regenerated using `forge build --force` (however, please note that you would have to execute `foundry-kompile` again to use KEVM). In KEVM, symbolic testing is performed via the `kevm foundry-prove` command. Once the compilation is finished, run the following command to symbolically execute the `testBackdoor_k` function, which---different from the tests we analyzed before---includes an explicit call to `setUp()`. To reproduce: ``` kevm foundry-prove \ --test PostExampleTest.testBackdoor_k ``` The optional `--test` argument instructs KEVM on the test function that should be symbolically executed. The analysis of `testBackdoor_k` peformed by KEVM completes in 10 minutes and reports that the test has failed. ![](https://i.imgur.com/U4W8iRu.png) At the moment, KEVM takes a different approach to presenting the results of its analysis: in contrast to other symbolic testing tools, it does not currently demonstrate the concrete input leading to the assert violation. Instead, it lets the user visualize and explore the (symbolic) execution of the analyzed test either interactively using: ``` kevm foundry-view-kcfg PostExampleTest.testBackdoor_k ``` ![](https://i.imgur.com/WYP6IkN.jpg) or statically: ``` kevm foundry-show PostExampleTest.testBackdoor_k ``` ![](https://i.imgur.com/9eZdG0c.png) Note that if we don't add `setUp()` to the body of a test function, the test will pass, i.e., the failed assert will not be identified, as the `PostExample` contract called within a test in this case will not be instantiated prior to the analysis: ![](https://i.imgur.com/VAr8FCT.png) To reproduce: ``` kevm foundry-prove \ --test PostExampleTest.testBackdoor ``` Our initial evaluation shows that all tools considered in this post successfully identify a failed assert in the `PostExample` smart contract using symbolic testing! The best results reported by these four tools are as follows: | Tool | Language | Solvers | Time | --------- | -------- | ------- | -------- | | Halmos | Python | Z3 | 4.2 sec | hevm | Haskell | Z3, cvc5 | 1.5 sec | EthBMC | Rust | Z3, Boolector, Yices2 | 1.1 sec | KEVM | Haskell, Python, etc. | Z3 | 10 min 24 sec ### Simple Example with Two Transactions Following in the footsteps of our previous post, we will further analyze these four tools on the two-transaction version of the `PostExample` smart contract. In this contract, the assert violation happens as a result of two function calls: `setLive(true); backdoor(6912213124124532)`. By including the first `setLive(true)` call in the `setUp()` function, we can examine how well the analyzed symbolic testing tools support the corresponding setup functionality. This version of the `PostExample` contract is available in [`src/PostExample_2tx.sol`](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/src/PostExample_2tx.sol), while the tests are specified in [`test/PostExample_2tx.t.sol`](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/test/PostExample_2tx.t.sol). The test contract looks as follows: ```solidity= import "../src/PostExample_2tx.sol"; contract PostExampleTwoTest is Test { PostExample public example; function setUp() public { example = new PostExample(); example.setLive(true); } function testBackdoor(uint256 x) public { example.backdoor(x); } function proveBackdoor(uint256 x) public { example.backdoor(x); } } ``` When run on this contract, **Halmos**, **hevm**, and **EthBMC/Foundry** exhibit behavior comparable to the single-transaction example, completing the analysis in 4.4, 1.4, and 1.2 seconds, respectively, and returning identical counterexample information---this indicates that the `setUp()` function is handled correctly. To reproduce: ``` halmos --contract PostExampleTwoTest ``` ``` hevm test --match PostExampleTwoTest ``` ``` forge test --match-contract PostExampleTwoTest ``` <!-- Halmos: ![](https://i.imgur.com/75ho6e2.png) EthBMC: ![](https://i.imgur.com/hATT2sO.png) hevm: ![](https://i.imgur.com/U8V73hw.png) --> To analyze this test using **KEVM**, we again include the call to `setUp()` into the `testBackdoor(uint256 x)` function: ```solidity function testBackdoor_k(uint256 x) public { setUp(); example.backdoor(x); } ``` In a bit less than 15 minutes, KEVM is able to detect the failure of this test. To reproduce: ``` kevm foundry-prove \ --test PostExampleTwoTest.testBackdoor_k ``` <!-- ![](https://i.imgur.com/QPMy6qR.png) --> The difference in the tools' performance can be observed when running them on a [modification of the two-transaction test smart contract](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/test/PostExample_2tx_setLive.t.sol), which removes the `example.setLive(true)` function call from `setUp()`, and instead adds`example.setLive(bool isLive)` to the test function itself, with `isLive` being a symbolic argument taken by the test function: ```solidity function setUp() public { example = new PostExample(); } function testBackdoor(bool isLive, uint256 x) public { example.setLive(isLive); example.backdoor(x); } ``` **Halmos** demonstrates comparable performance by taking 4.5 seconds to detect and report the failure of the test: ![](https://i.imgur.com/vTiVdwY.png) To reproduce: ``` halmos --contract PostExampleTwoLiveTest ``` As seen on the screenshot above, Halmos reports a single counterexample that involves setting the value of `live` to `true` and calling the `backdoor` function with `x` being equal to `6912213124124532`. **EthBMC/Foundry** takes more time to analyze the test than it did before---it completes the analysis in 11.5 seconds. Interestingly, the best results for this test can be obtained with Boolector being used as the SMT solver, while Yices2 performed better on all previous examples from this post. ![](https://i.imgur.com/990MbVr.png) To reproduce: ``` forge test --match-contract PostExampleTwoLiveTest ``` EthBMC/Foundry identifies two failing tests in `PostExampleTwoLiveTest`. For `proveBackdoor`, which is analyzed symbolically, it returns a counterexample similar to the one reported by Halmos. In addition to it, Foundry's fuzzer also identifies the input that makes `testBackdoor` (analyzed concretely) fail---this happens due to a revert that occurs in the `require(live);` statement if the value of `live` has been set to `false` . If we comment out the content of the `testBackdoor` function, `forge test` will return a single counterexample corresponding to the `proveBackdoor` test. **hevm** also reports both `testBackdoor` and `proveBackdoor` as failing (in just 1.5 seconds!). However, different from EthBMC/Foundry and Halmos, it returns three counterexamples it total---one for `testBackdoor` and two for `proveBackdoor`: ![](https://i.imgur.com/gomgzDr.png) To reproduce: ``` hevm test --match PostExampleTwoLiveTest ``` The second counterexample returned for `proveBackdoor` is similar to the one that is (concretely) generated for `testBackdoor`, i.e., it corresponds to a revert that occurs due to a failed `require(live);` check if the value of `live` is `false`. By default, Foundry and hevm report reverted tests as failed; even though Halmos also reports a test failure if it gets reverted, Halmos returns a single counterexample as the output when run on the test smart contract considered in this section. <!-- If we move `setLive(bool isLive)` to the test function itself, with `isLive` being a symbolic argument, it will report two violations. ![](https://i.imgur.com/JbjWNWn.png) --> <!-- With two transactions in the test: ![](https://i.imgur.com/HWq4k7p.png) That takes considerably longer---probably due to an external function call; instead of simply using concrete initial storage. --> Interestingly, **KEVM** does not complete the analysis of this variation of the `testBackdoor` function within the timeout of one hour: ```solidity function testBackdoor_k(bool isLive, uint256 x) public { setUp(); example.setLive(isLive); example.backdoor(x); } ``` To reproduce: ``` kevm foundry-prove \ --test PostExampleTwoLiveTest.testBackdoor_k ``` The summary for the analysis performed in this post so far is shown in the table below: | Tool | Language |Best: 1tx | Best: sU+1tx | Best: 2tx | | -------- | -------- | -------- |-------- | -------- | | Halmos | Python | 4.2 sec | 4.4 sec | 4.5 sec | | hevm | Haskell | 1.5 sec | 1.4 sec | 1.5 sec | | EthBMC | Rust | 1.1 sec | 1.2 sec | 11.5 sec | | KEVM | Haskell, Python, etc. | 10 min 24 sec| 14 min 46 sec | x | *"sU+1tx" stands for "`setUp()` + 1tx", which corresponds to the earlier variation of the test, where `setLive` is called in the `setUp` function; 2tx corresponds to the latter variation, where `setLive` is called in the test function with a symbolic argument*. ### Examples from [Echidna VS Forge](https://github.com/clabby/echidna-vs-forge) Repository Similarly to the previous post, we further compare the tools based on the smart contracts from the [Echidna VS Forge repository by clabby](https://github.com/clabby/echidna-vs-forge). This repository contains two smart contracts: [Foo](https://github.com/clabby/echidna-vs-forge/blob/main/src/Foo.sol) (having `uint256` variables as function inputs) and [FooBytes](https://github.com/clabby/echidna-vs-forge/blob/main/src/FooBytes.sol) (having `bytes32` variables as function inputs); these contracts were originally intended to be used for fuzzer comparison. The objective is to find two inputs equal to the magic number `0x69` to supply to the contract's `foo(uint256/bytes32)` and `bar(uint256/bytes32)` functions. If both of these functions are called with an input of `0x69`, another function `revertIfCracked()` will fail with the assert violation. The inclusion of this repository into the evaluation performed in this post also helps showcase the usability improvements offered by symbolic testing compared to traditional symbolic execution: Echidna VS Forge is, in fact, a Foundry project that already contains two tests (one for each of the two analyzed smart contracts). Each test encodes three function calls that eventually lead to a revert when called with specifically crafted input; we can directly re-use these already-defined tests to evaluate the considered symbolic testing tools based on their ability to identify these revert-triggering inputs. In the scope of our previous post, we [modified the analyzed smart contracts](https://github.com/baolean/symexec-bench/blob/ff6c8304e07d7dcddb770ea64f4b96d27144064b/SymTest/src/Foo.sol#L34) (`Foo` and `FooBytes`) to use `assert` instead of a `revert` statement in order to make it detectable by all symbolic execution tools. For the analysis performed in this post, we also had to rename the test contracts (`Foo_Test` and `FooBytes_Test`) to eliminate the underscore in the contract name, which at the moment is considered [a forbidden character in KEVM](https://github.com/runtimeverification/evm-semantics/issues/1703). The analyzed smart contacts are available in [`src/Foo.sol`](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/src/Foo.sol) and [`src/FooBytes.sol`](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/src/FooBytes.sol); the tests are defined in [`test/Foo.t.sol`](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/test/Foo.t.sol) and [`test/FooBytes.t.sol`](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/test/FooBytes.t.sol). Two tests that we analyze in this section take the inputs to `foo` and `bar` as (in our case, symbolic) parameters and perform the following three functions calls to `Foo` and `FooBytes`, respectively: ```solidity Foo internal a; function setUp() public { a = new Foo(); } function testFuzz_cracked(uint256 x, uint256 y) public { a.foo(x); a.bar(y); a.revertIfCracked(); } ``` ```solidity FooBytes internal a; function setUp() public { a = new FooBytes(); } function testFuzz_cracked(bytes32 x, bytes32 y) public { a.foo(x); a.bar(y); a.revertIfCracked(); } ``` Untill now, we used the `--contract` option in Halmos, `--match-contract` in EthBMC/Foundry, and `--match` in hevm to specify the test contract that should be symbolically analyzed by these tools. In Echidna VS Forge, both `testFuzz_cracked` tests are named similarly but are located in two different test contracts. However, all the tools we are considering in this post provide the ability to symbolically execute test functions that match a certain regular expression. This helps us analyze both `testFuzz_cracked` tests in the same run, and can be done using `--function` in Halmos and `--match-test` in EthBMC/Foundry. In hevm, we can analyze specific test functions using the same `--match` option as before. **Halmos** takes 5.8 seconds to detect the assert violations happening in both the `uint256` and `bytes32` tests and output the identified counterexample data (note that 105 is the decimal representation of 0x69, which is the expected result): ![](https://i.imgur.com/Nu6imW0.png) To reproduce: ``` halmos --function testFuzz ``` **hevm** takes around 1.6 seconds to find both violations and the input that leads to them: ![](https://i.imgur.com/UlvgxXD.png) To reproduce: ``` hevm test --match 'proveFuzz' ``` While hevm and Halmos consistently demonstrate high performance, **EthBMC/Foundry** now takes around 1 minute 41 seconds to analyze both tests. Our empirical observations suggest that the performance decline is associated with an increase in the number of *external* function calls being analyzed within the test and needs further investigation. ![](https://i.imgur.com/KSeXAWG.png) To reproduce: ``` forge test --match-test 'proveFuzz' ``` **KEVM** takes 35 minutes to complete the analysis of both tests. In this example, we make use of the paralellization capability by supplying the `-j2` flag together with the `kevm foundry-prove` command, which instructs KEVM to analyze two tests in parallel (the analysis of the same two tests takes more than an hour if run without this flag): ``` kevm foundry-prove \ --test FooTest.testFuzz_cracked_k \ --test FooBytesTest.testFuzz_cracked_k -j2 ``` KEVM reports both of the tests as failed, indicating that it successfully identified the corresponding inputs: ![](https://i.imgur.com/QioWlZo.png) The following table shows the summary of the evaluation: | Tool | 1tx | sU+1tx | 2tx | Foo/FooBytes | -------- | -------- | -------- |-------- | -------- | | Halmos | 4.2 sec | 4.4 sec | 4.5 sec | 5.8 sec | hevm | 1.5 sec | 1.4 sec | 1.5 sec | 1.6 sec | EthBMC |1.1 sec | 1.2 sec | 11.5 sec | 1 min 41 sec | KEVM | 10 min 24 sec | 14 min 46 sec | x | 35 min 14 sec | ### MiniVat---A More Realistic Example Finally, following the structure of our previous post, let's run our tools on the [MiniVat](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/src/MiniVat.sol) smart contract, which represents [more realistic smart contract code](https://hackmd.io/@SaferMaker/EVM-Sym-Exec#A-More-Realistic-Example). The violation of an assert expressing the [fundamental equation of DAI invariant](https://hackmd.io/@SaferMaker/DAICertoraSurprise) occurs through a sequence of four function calls, which we include in a test function called `testInvariant`. We express the invariant using a DSTest/Foundry `assertEq` supplementary function, which checks an equality between two values. We discuss how this assertion functionality is implemented under the hood [later in the post](#Handling-DSTestForge-asserts). The analyzed smart contact can be found in [`src/MiniVat.sol`](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/src/MiniVat.sol); the tests are provided in [`test/MiniVat.t.sol`](https://github.com/baolean/symexec-bench/blob/symtest/SymTest/test/MiniVat.t.sol). The test function we are analyzing is shown below. All the arguments are concrete: ```solidity function testInvariant() public { vat.frob(10 ** 18); vat.fold(-10 ** 27); vat.init(); (uint Art, uint rate, uint debt) = vat.getValues(); assertEq(debt, Art * rate); } ``` This test contains several function calls to `MiniVat`, which are external to the test contract. As demonstrated by the previous example, the increased number of external calls introduces overhead to the analysis performed by tools such as EthBMC/Foundry and KEVM. This observation can be verified by comparing the performance of these tools on the test shown above with their performance on a [test](https://github.com/baolean/symexec-bench/blob/c79cbecb6fc9564332eb8693d1ff378425d9427d/SymTest/test/MiniVat.t.sol#L45) involving a single external call to the `counterexample()`function, which, in turn, invokes the same set of smart contract functions but within the `MiniVat` smart contract itself. The latter test will be analyzed much faster. ```solidity function testCounterexample() public { vat.counterexample(); } ``` <!-- *As a possible workaround, we can inherit the test contract from the contract under analysis and calling functions internally. We leave that as the experiment for the to the reader.* --> When run on a `proveInvariant/testInvariant` test that contains several external calls and an `assertEq` statement, **EthBMC/Foundry** correctly identifies a violation in 3 minutes 51 seconds: ![](https://i.imgur.com/bFobuYo.png) To reproduce: ``` forge test --match-contract MiniVatTest ``` It takes around 1.5 seconds for **hevm** to report the assert violation in the symbolic (`proveInvariant`) as well as the concrete tests (`testInvariant`): ![](https://i.imgur.com/YMSzHdj.png) To reproduce: ``` hevm test --match MiniVatTest ``` **Halmos** reports the `testInvariant` test as failing in a bit less than 3 minutes. However, it encounters some issues with processing and returning the counterexample as it outputs the `Counterexample: unknown` error message (even though there are no parameters in this test, Halmos normally returns `[]` as a counterexample in this case). ![](https://i.imgur.com/65htd66.png) To reproduce: ``` halmos --contract MiniVatTest ``` **KEVM** takes 32 minutes to finish the analysis and successfully identifies the violation happening within the test: ![](https://i.imgur.com/b5vzD7E.png) To reproduce: ``` kevm foundry-prove \ --test MiniVatTest.testInvariant_k ``` The summary of all results of the evaluation performed in this post is shown below: | Tool | 1tx | sU+1tx | 2tx | Foo/FooBytes | MiniVat | -------- | -------- | -------- |-------- | -------- | -------- | | Halmos | 4.2 sec | 4.4 sec | 4.5 sec | 5.8 sec | 2 min 48 sec | hevm | 1.5 sec | 1.4 sec | 1.5 sec | 1.6 sec | 1.5 sec | EthBMC |1.1 sec | 1.2 sec | 11.5 sec | 1 min 41 sec | 3 min 51 sec | KEVM | 10 min 24 sec | 14 min 46 sec | x | 35 min 14 sec | 32 min 12 sec| <!-- *Halmos has some issues with counterexample processing* --> ## tl;dr All four tools considered in this post---Halmos, hevm, KEVM, and EthBMC/Foundry---support symbolic execution of tests defined as part of a Foundry project. Most of the tools perform well on the majority of the experimental smart contracts and their corresponding tests, using only several seconds for the analysis. Based on the evaluation described in this post, hevm demonstrates the best performance, followed by Halmos and EthBMC, and, finally, KEVM. Most of the tools output the concrete counterexample corresponding to the test failure. KEVM informs the user on the status of the test verification, but takes a different approach to the representation of the results: it allows the user to step through the execution, thereby visualizing the analysis process. Apart from being able to analyze the compilation artifacts produced by Foundry, all tools support some of the DSTest/Foundry-specific functionality. For example, hevm, Halmos, and EthBMC support the state initialization via `setUp()`, and all four tools recognize Foundry's supplementary assert functions, such as `assertEq`, `assertTrue`, etc. In this post, we chose not to compare the tools based on their hevm/Foundry [cheatcode](https://book.getfoundry.sh/forge/cheatcodes) support as they seem to implement an almost non-intersecting sets of cheatcodes---however, all tools support at least one cheatcode. hevm supports a comperehensive set of cheatcodes including `warp`, `roll`, `store`, `load` etc. In fact, these cheatcodes are actively used in Foundry projects but were originally introduced by [hevm itself](https://github.com/dapphub/dapptools/blob/master/src/hevm/README.md#cheat-codes). KEVM supports arguably the most extensive list of cheatcodes at the moment, including [several cheatcodes](https://github.com/runtimeverification/foundry-demo/blob/master/src/utils/KEVMCheats.sol) that are specific to symbolic testing with KEVM. The `assume` cheatcode is [supported by EthBMC](https://github.com/baolean/EthBMC/commit/bdb9a7df1f711cf4a399bf28b816a5619cfb6144) and [Halmos](https://github.com/a16z/halmos/blob/0f694da2a277d8e444e5553efa09d38746cb8c53/src/halmos/utils.py#L12), with the latter also supporting `getCode`. <!-- - , which is known to be particularly slow when dealing with large bitvectors (that are extensively used in Mythril to model `uint` variables and more) --> <!-- - When analyzing more complex smart contracts, constraint solving causes the execution to hang. In general, constraint solving takes up a significant amount of execution time --> <!-- - . The hash processing strategy is not configurable (in contrast to Manticore). --> ### Summary In summary, symbolic testing is a rapidly developing technique that shows great promise in improving the usability and user-friendliness of symbolic execution for smart contracts, making it easier to integrate symbolic analysis into the smart contract development processes. All tools reviewed in this post support basic functionality related to symbolic testing of Foundry projects, which enables re-use of existing tests and properties defined for a smart contract. All these tools, however, are also undergoing active development, so we expect further improvements in their performance as well as extended support for Foundry's supplementary testing features, such as cheatcodes. <!-- symbolic execution is a promising technique when it comes to code security, with our experiments proving that it can find issues that some other techniques cannot. It is very exciting that there is active development in this area from many teams. At the same time, in their current state, symbolic execution tools often are fragile, cranky, and wayward. To get desired results and even get them to work at all, you often need to know their internals in and out. This post is the first in a series that documents our efforts on making symbolic execution more practical and accessible for wider audiences. --> <!-- Other benchmarks on which these tools can be evaluated include e.g., the one used in KEVM! --> <!-- The tools differ in - how they use/relation to Foundry - cheatcodes - performance --> ## Bonus Section: The Hitchhiker's Guide to Foundry Integration In this section, we document our experience of implementing the experimental integration of EthBMC with Foundry. The purpose of this integration is two-fold: first, we introduce symbolic testing into the Foundry development framework; and, second, it also helps improve the user experience for symbolic execution with EthBMC. For a more detailed discussion on the performance and usability of EthBMC, please refer to our previous post. In the evaluation described in this post, we used an instrumented version of Foundry that is available in the `symexec` branch of [our Foundry fork](https://github.com/baolean/foundry/tree/symexec). To carry out symbolic testing with EthBMC, our fork of Foundry uses a [local crate built from the EthBMC implementation](https://github.com/foundry-rs/foundry/blob/9c15eb7b2e1968dbe4070ffbc3beea7ef4207d0c/forge/Cargo.toml#L14) located in a folder in the same directory as one containing the Foundry source code. The version of EthBMC that supports Foundry integration is implemented in the `forge` branch of [our fork of EthBMC](https://github.com/baolean/EthBMC/tree/forge). To install the version of Foundry that supports symbolic testing based on EthBMC, run the following commands: ```shell git clone https://github.com/baolean/EthBMC.git && \ cd EthBMC && \ git checkout forge && \ cd .. git clone https://github.com/baolean/foundry.git && \ cd foundry && \ git checkout symexec && \ foundryup --path . ``` <!-- *None that these version of Foundry will become the default after running `foundryup --path .`.* --> With this version of Foundry installed, every run of `forge test` not only executes the concrete, fuzz, and invariant tests supported by Foundry, but also symbolically analyzes test functions that start with `prove`. The rest of this section will outline the necessary steps to successfully integrate a symbolic execution tool with Foundry to facilitate symbolic testing; these steps include input and output processing, symbolic analysis of test functions that follow a chosen naming convention, and support of supplementary testing features available in Foundry. ### Input Processing To symbolically execute a smart contract, EthBMC relies on a runtime binary of a smart contract that has to be provided by a user. The binary, together with other information such as contract addresses and initial storage state (the constructor code is not included in the runtime binary!), should be supplied in the format of a specific [YAML configuration file](https://github.com/RUB-SysSec/EthBMC#yaml-format). Integrating EthBMC with Foundry helps us streamline the process of source code compilation by using the build artifacts generated by Foundry (as a result of `forge build` or `forge test`) and supplying the resulting bytecode to EthBMC automatically. In our implementation, the symbolic execution functionality of EthBMC is invoked directly from Foundry based on the results of the test contract code pre-processing. This approach helps us leverage Foundry's compilation and calldata decoding capabilities, and output the result of the analysis in the format that is consistent with those for tests analyzed concretely. The obvious downside of this approach is the necessity to run a modified version of Foundry, which might be challenging to keep in sync with the original branch, as it is updated very actively. An alternative approach is taken by some other tools, such as hevm and KEVM, that also perform symbolic testing based on the compilation artifacts produced by Foundry, but are run independently from it. In addition to runtime binaries of the analyzed smart contracts, the information that should be supplied to EthBMC includes the initial states of the considered smart contracts; the address of the test contract that will be analyzed; function selectors corresponding to the tests that should be symbolically executed; and configuration information related to symbolic execution, if available. The initial states of the smart contracts that will be used for analysis correspond to their states after the execution of the `setUp()` function. As we mentioned earlier in this post, `setUp()` therefore provides a straightforward way to initialize the state in the absence of a constructor, which is not included in the runtime bytecode. For every smart contract that is present in the project, we extract the information about its bytecode and storage layout after the execution of `setUp()`---this data will then be used in EthBMC to define the initial state for the symbolic analysis. Foundry and EthBMC use different implementations of Ethereum types, so, for simplicity, we record the values in the form of hex strings. ```rust for (address, account) in db.accounts.iter() { let mut account_storage: HashMap<String, String> = HashMap::new(); // Recording the contract information: // address, bytecode, and initial storage let account_code: String = hex::encode(&account.info.code.as_ref() .unwrap().bytes()); // Recording storage values to set up symbolic tests for (slot, value) in &account.storage { account_storage.insert( hex::encode(utils::u256_to_h256_be(*slot)), hex::encode(utils::u256_to_h256_be(*value)), ); } setup_accounts.insert(hex::encode(address), (account_code, account_storage)); } ``` Similar to hevm, our EthBMC/Foundry integration symbolically executes tests that are prefixed with the keyword `prove`. To supply this information to EthBMC, we instruct Foundry to recognize tests that should be symbolically executed, and record the signatures for functions that follow this naming convention: ```rust fn is_symbolic_test(&self) -> bool { self.starts_with("prove") } ... pub fn run_symbolic_test(...) -> ... { ... // Recording `prove...` function selectors let signature: String = hex::encode(function.short_signature()); ... } ``` One other type of input we need to provide to EthBMC is the symbolic execution configuration. The cutomizable parameters should include the SMT solver used and the loop bound; we should also be able to enable or disable the usage of symbolic storage and concrete validation. We have [instrumented](https://github.com/baolean/foundry/blob/5c902d8a26dcf45dbf7121d55afeb2e827c0d8b9/config/src/symbolic.rs) Foundry with the ability to recognize the following configuration section that can be added to the `foundry.toml` file: ``` [symbolic] symbolic_storage = false concrete_validation = true solver_timeout = 120_000_000 # ms solver = 1 # 0: z3, 1: boolector, 2: yices2 loop_bound = 50 call_bound = 1 ``` We set the value of `call_bound`, which is the number of function calls to be analyzed, to 1 by default, as we are only interested in executing symbolic tests, and not sequences of function calls. The parsed configuration is recorded in the following structure: ```rust pub struct SymbolicConfig { /// ... whether to assume that default storage values are symbolic pub symbolic_storage: bool, /// ... whether to perform geth-based concrete validation pub concrete_validation: bool, /// SMT solver to be used /// {0: z3, 1: boolector, 2: yices2} pub solver: u8, /// The timeout (ms) for the solver pub solver_timeout: u32, /// The number of loops to be unrolled in a single execution pub loop_bound: u32, /// The number of calls symbolically analyzed in a sequence pub call_bound: u32, } ``` Finally, if the test contract contains symbolic tests, our version of Foundry [starts processing](https://github.com/baolean/foundry/blob/9c15eb7b2e1968dbe4070ffbc3beea7ef4207d0c/forge/src/runner.rs#L308) these tests using EthBMC one by one. Analyzing one transaction at a time (in contrast to passing a set of symbolic tests to EthBMC) helps decode the results corresponding to the analysis of each function properly, correctly measure the time used to analyze each test, and possibly prevent symbolic execution of all tests from being stalled if one of them cannot be processed. By doing so, we also take advantage of the very short startup time of EthBMC. For every symbolic test identified in a project, we run EthBMC while also supplying the collected input, which includes the address of the analyzed contract, runtime bytecode and storage setup of smart contracts involved in the analysis, symbolic test function selectors, and the configuration information related to the symbolic execution. ```rust pub fn run_symbolic_test(...) -> Result<TestResult> { ... // Running symbolic analysis in EthBMC let symbolic_result: Option<(String, String, String)> = esvm::forge_analysis( hex::encode(*analyzed_contract), signature, setup_accounts, serde_json::to_string(&test_options.symbolic).unwrap(), ); ... } ``` ### Symbolic Execution of Tests As we have discussed in the previous post, symbolic execution tools usually perform the analysis by issuing a transaction with symbolic calldata, which represents a call to any smart contract function with symbolic parameters. Since, in this case, we perform symbolic testing, we are interested in symbolically executing only a specific function that starts with `prove` and corresponds to a funciton selector supplied from Foundry. A straightforward way to make sure that the analysis is restricted to such functions is to impose a constraint on the function selector (i.e., the first four bytes) of the otherwise symbolic calldata: ```rust // Restricting the analysis to `prove_xxx` functions // Loading the calldata from memory let load = mload(&new_state.memory, new_state.input_tx().data, &const256("0")); // If the `prove` function selector is provided by Foundry, if let Some(selector) = env.get_selector() { let prove_selector = const_vec(&hexdecode::decode(selector.as_bytes()).unwrap()); // Selecting the first 4 bytes from the calldata let shiftval = const_u256(U256::from(224)); let shiftop = lshr(&load, &shiftval); // Forming a constraint that asserts that these 4 bytes == selector let prove_constraint = eql(&prove_selector, &shiftop); // Adding the constraint to the state new_state.push_constraint(prove_constraint); } ``` ### Supporting Supplementary Testing Functionality To facilitate testing, Foundry supports a set of supplementary features that should also be supported by the symbolic execution component of our integration. In this section, we consider two types of these features: DSTest/Foundry asserts and cheatcodes. #### Handling DSTest/Forge asserts [DSTest](https://github.com/dapphub/ds-test/blob/master/src/test.sol) and [Forge Standard Library](https://book.getfoundry.sh/reference/forge-std/) provide a smart contract developer with a set of functions that facilitate the specification of assertions. These functions include, for example, `assertTrue(bool)`, `assertEq(address a, address b)`, and many others. Different from regular asserts provided by Solidity, the violation of the condition expressed using these constructs does not immediately stop the execution of a smart contract; instead, the variable `_failed` in the `DSTest` smart contract [is set to `true`](https://github.com/dapphub/ds-test/blob/e282159d5170298eb2455a6c05280ab5a73a4ef0/src/test.sol#L75). In a Foundry test contract that inherits from `forge-std/Test.sol`, this variable is located at slot 0 with byte offset 1. To identify the violation of this type of an assert, we instrumented EthBMC with an additional check on the value located at this offset in the test smart contract storage during the symbolic execution process (and later during the concrete validation using Geth): ```rust // Detecting forge-std/Test assert failures // If the analysis is run in the Foundry symtest mode if potential_attack_state.env.func_selector.is_some() { // Clone the current smart contract state let mut check = potential_attack_state.clone(); // To identify failed `assertEq`, `assertTrue`, etc., // read the value located at slot 0, offset 1 let failed_val = byte_at( &sload(&check.memory, check.account().storage, &const_usize(0)), &one(), ); // Add constraint that requires this value to be 1 check.push_constraint(eql(&failed_val, &one())); // If it's possible--the assert might be violated if check.check_sat() { info!("Foundry's assert might be violated!"); // Use concrete validation to make sure it is a true positive // Or just return results if the validation is disabled ``` #### Cheatcodes Another feature provided by Foundry to facilitate smart contract analysis is *[cheatcodes](https://book.getfoundry.sh/forge/cheatcodes)*. While there are many cheatcodes supported by Foundry, we decided to start with the experimental support of the `assume` cheatcode. Cheatcodes are implemented as calls to a special [`Vm`](https://github.com/foundry-rs/forge-std/blob/master/src/Vm.sol) smart contract at address `0x7109709ecfa91a80626ff3989d68f67f5b1dd12d`; to process the cheatcode correctly, we need to intercept the calls to this hardcoded address, parse the calldata with which this call was performed to identify the exact cheatcode to be processed, and update the symbolically analyzed state accordingly. In EthBMC, support for the `assume` cheatcode is implemented in commits [one](https://github.com/baolean/EthBMC/commit/bdb9a7df1f711cf4a399bf28b816a5619cfb6144) and [two](https://github.com/baolean/EthBMC/commit/5a331eece80c500692d98bcca6dbef5a80f1c89a). `assume(bool)` is used to declare the assumptions on the values of some variables. During fuzzing, the inputs that don't satisfy the assumption have to be rejected (possibly leading to the corresponding issue); during symbolic execution, this assumptions can be accomodated in a straightfoward way: by adding a corresponding constraint to a set of path conditions (i.e., to the formula that comprises conditions that should be satisfied for a specific execution path to be taken). In our fork of EthBMC, we instruct it to recognize the calls performed to `0x7109709ecfa91a80626ff3989d68f67f5b1dd12d`, decode the calldata supplied with this call, and, if it is equal to that of the `assume` cheatcode, add the corresponding expression to the set of constraints corresponding to this execution path: ```rust let mut is_assume: bool = false; if *to == parse_hex_string( &String::from("0x7109709ecfa91a80626ff3989d68f67f5b1dd12d"))) { // Executing a call to the Vm smart contract is_vm = true; } // Loading the calldata from memory, // extracting a function selector from it let load = mload(&call.memory, call.mem, in_off); let shiftval = const_u256(U256::from(224)); let shiftop = lshr(&load, &shiftval); // If the selector is equal to if FVal::simplified(&shiftop) == // bytes4(keccak256("assume(bool)")) parse_hex_string(&String::from("0x4C63E562")) { // Executing an `assume` cheatcode is_assume = true; } // vm.assume if is_hevm && is_assume { // 128 + 4 == 132 let args = add(in_off, &const_usize(4)); // Getting the condition contained provided in `assume` let load_args = mload(&call.memory, call.mem, &args); call.push_constraint(load_args); ... // Adding this condition to path conditions (current constraints) call.push_constraint(eql(&callres, &one())); ... } ``` ### Output Processing Finally, after the analysis performed by EthBMC is completed, we need to output the results of the symbolic testing. EthBMC does not automatically decode the identified counterexample calldata; however, we can utilize the decoding capabilities of Foundry. For this, we return the result of symbolic testing back to the original `foundry test` process that had run EthBMC. The returned information includes the addresses of the sender, receiver, and the calldata that leads to the test failure identified using symbolic testing: ```rust // Returning the first identified counterexample to Foundry if let Some(counterexample) = counterexamples.get(0) { let sender = counterexample[0].sender.clone(); let receiver = counterexample[0].receiver.clone(); let input_data = counterexample[0].input_data.clone(); let result: (String, String, String) = (sender, receiver, input_data); return Some(result); } ``` This information is then used to generate a counterexample in Foundry; this counterexample will also be shown in the output produced by `forge test`: ```rust= if let Some(result) = symbolic_result { let counterexample = BaseCounterExample::create( H160::from_str(&result.0).unwrap(), H160::from_str(&result.1).unwrap(), &Bytes::from_str(&result.2).unwrap(), &identified_contracts, None, ) .wrap_err("Failed to create counterexample")?; } ``` This approach also helps us return the results in the same format as Foundry does, as well as to execute symbolic tests in the same run as other concrete and fuzz tests. Some of the code excerpts of our integration project between EthBMC and Foundry that were given in this post are, admittedly, crude hacks (e.g., primitive string marshalling in the example above). Please keep in mind that in this rough proof-of-concept we optimized for time-to-functioning-prototype rather than anything else, and any contributions are extremely welcome!