Add symbolic execution

[samalws-tob]

This PR is a continuation of #1030 and #1175. It adds a symExec configuration option which enables an extra symbolic execution worker, which runs alongside the existing fuzzing workers. This should allow for bugs which require very specific inputs to be caught more easily (see tests/solidity/symbolic/sym.sol for a fairly contrived example). Symbolic execution is mostly implemented by hevm; the bulk of this PR has to do with calling hevm's symbolic executor in the right way, and spawning a new worker to do this.
The sym exec worker runs at startup using the initial corpus, and also runs whenever a fuzz worker finds new coverage. It uses a queue to keep track of this. When the queue is empty, the worker is in a sleep mode waiting for more events to come in.
This PR also adds symExecTimeout and symExecNSolvers configuration options which allow for choosing the timeout and number of sym exec solvers (i.e. Z3 instances, I think). It's unclear what a good default value for these would be, so I just picked something that looks right (30 and 1, respectively).

This is meant to be an experimental feature, and this PR shouldn't affect users unless they explicitly enable symExec. It is turned off by default.

[ggrieco-tob]

This is great!. I have some suggestions, but this first needs some testing. Btw, I think this code will not work as expected when allContracts is enabled, right?

[ggrieco-tob]

Some UI improvements we need (as simple textual events):

• Show when a new coverage is result from using symbolic execution (or fuzzing)
• Show when a worker is hitting a solver timeout
• Show when a solver is returning unfeasible
• Show when a worker has finished and has nothing else to do
• Show a message when the campaign is terminated because there is no concrete workers and all the symbolic workers are waiting.

[samalws-tob]

This is great!. I have some suggestions, but this first needs some testing. Btw, I think this code will not work as expected when allContracts is enabled, right?

Yeah, it won't be able to call any contracts aside from the "main one"

[ggrieco-tob]

A few small additional improvements:

• Allow to set symExec., symExecTimeout and symExecNSolvers from command line. This will allow a quick experimentation without having to change the base config file
• (If it is not too hard): Allow to select the number of symboilc transactions to execution. This will usually take a very small positive number, by default is 1, but it can be 2 or 3 as well. I believe this will impact here: mapM_ (\symTx -> void $ callseq vm (txs ++ [symTx])) symTxs

[samalws-tob]

• I added @ggrieco-tob 's suggestions, with one exception: I didn't add an event for when a symbolic worker is idle, since this would require peeking from a channel, which as far as I can tell isn't possible.
• I disabled windows tests for symbolic execution, since these were failing. We can ship this as an experimental feature with linux and mac support for now, and fix windows later.
• I’m unsure about the ToJSON implementation for SymNoNewCoverage, someone please check that this is fine.

[samalws-tob]

Also added config options for setting the maxIters and askSMTIters variables passed to hevm

[rappie]

Also added config options for setting the maxIters and askSMTIters variables passed to hevm

Could this be used to lower the memory consumption?

[samalws-tob]

Yep, although it only affects memory consumption of symbolic execution, not the fuzz workers

[elopez]

This PR on hevm may resolve the issues on Windows ethereum/hevm#484

[rappie]

Yep, although it only affects memory consumption of symbolic execution, not the fuzz workers

I've ran some tests and it is using a LOT less memory with the default config now.

    function testSymExec(uint256 magicNumber) public {
        if (magicNumber == 1256984789498465878979846549849854654984)
            t(false, "you found the magic number");
    }

What is a good approach to test the symexec itself? I've tried the above code but it does not break this in a couple of minutes.

Update: I should have been a bit more patient. It breaks both with and without symexec enabled in ~10 minutes.

[samalws-tob]

Related note here: I'm working on implementing concolic execution, which should significantly lower the memory usage & runtime when executing on functions with a lot of branches (I kept running into this issue when testing this PR). I should have a proof-of-concept available in a day or two. Most of the code for concolic execution will be shared with the code from this PR, so any bug you find here will probably also be a bug in the concolic version.

[samalws-tob]

@ your test example: It shouldn't take that long to find the test case, unless there's other functions in the contract that it tries executing first

[samalws-tob]

This PR on hevm may resolve the issues on Windows ethereum/hevm#484

Thanks @elopez !

[samalws-tob]

Just pushed a commit adding support for concolic execution. It works, but:

• We need to add some tests for it
• There's a few minor TODOs to work out
  ...so I'm going to convert this PR back to a draft PR

Any testing done on both the symexec and concolic execution features is appreciated :)

[samalws-tob]

@elopez confirmed that your hevm PR fixes tests on windows

[samalws-tob]

Fixed up the todos, now all that's left is:

• Adding tests
• Reverting stack.yaml (I have it set to a fork of hevm, awaiting my & Emilio's PRs getting merged)
• Review

[ggrieco-tob]

I think this looks almost ready to go. We need to:

• Add additional debug information to show what the worker is doing. This is very useful to see why some result is taking too much time. Some suggestions to include:

   flip runReaderT defaultEnv $ withSolvers Z3 (fromIntegral conf.campaignConf.symExecNSolvers) timeout $ \solvers -> do
     threadId <- liftIO $ forkIO $ flip runReaderT defaultEnv $ do
       res <- forM methods $ \method -> do
+        liftIO $ print method
         let
           fetcher = concOrSymFetcher tx solvers rpcInfo
           dst = conf.solConf.contractAddr
@@ -92,8 +93,11 @@ exploreContract conf contract tx vm = do
                           & #env % #contracts .~ (Map.union vmSym'.env.contracts vm.env.contracts)
         -- TODO we might want to switch vm's state.baseState value to to AbstractBase eventually.
         -- Doing so might mess up concolic execution.
+        liftIO $ putStrLn $ "Building path conditions"
         exprInter <- interpret fetcher maxIters askSmtIters Naive vm' runExpr
-        models <- liftIO $ mapConcurrently (checkSat solvers) $ manipulateExprInter isConc exprInter
+        let sats = manipulateExprInter isConc exprInter
+        liftIO $ putStrLn $ "Number of expressions:" ++ show (length sats)
+        models <- liftIO $ mapConcurrently (checkSat solvers) sats

It is very useful to know which transaction is explored, but let's make sure the printing looks correct since it is ugly here 😅

• Restrict methods to state changing ones or the ones that contain assertions. There is little point in exploring view/pure functions.
• symExecTimeout is actually per query in Z3 (but global in other solvers, afaik), I think it is better to clarify that.
• Randomize the list of corpus transactions before sending it to the solver. This will help to discover a more variety of paths in different runs.

[m4k2]

Hi, I want to try out the new features, I'm currently using Echidna version 2.2.3 and encountering issues. It seems that some options are not supported yet ?

Warning: unused option: symExec
Warning: unused option: symExecAskSMTIters
Warning: unused option: symExecConcolic
Warning: unused option: symExecMaxIters
Warning: unused option: symExecNSolvers
Warning: unused option: symExecTargets
Warning: unused option: symExecTimeout

Maybe it's for the next release ?

[rappie]

Maybe it's for the next release ?

Correct.

You can download one of the latest builds here (scroll down)
https://github.com/crytic/echidna/actions/runs/9522275975

Or manually build the latest master branch (what I prefer):
https://github.com/crytic/echidna?tab=readme-ov-file#building-using-nix-works-natively-on-apple-m1-systems