High-performance Concrete Fuzzing Taking Advantage of Expr

[msooseth]

Original Idea (already implemented)

There are some hard cases where running concrete execution for a little bit will get us a win. For example:

    function prove_distributivity(uint120 x, uint120 y, uint120 z) public pure {
        assert(x + (y * z) == (x + y) * (x + z));
    }

In the benchmark suite https://github.com/eth-sc-comp/benchmarks/ will take forever for an SMT solver to deal with, but a fuzzer should find a counterexample in <1s.

This sounds like a hack, and in some sense it is, but I can very easily see this being helpful to the users. The perceived utility of HEVM would be higher, and that's all that matters.

We could even run a thread that just does fuzzing, while the other threads do the symbolic interpretation, etc.

Follow-ups

The original idea as per above has been implemented already, see Fuzz.hs. However, as detailed below by d-xo, there are a number of significant improvements that can be done that could improve the performance in very significant ways.

[d-xo]

I think a hybrid fuzzing mode will be extremely powerful. The dream setup I've always had in my head is as follows:

1. summarize the contract under test
2. try to get models that can hit every branch
3. use any models as seeds for a dictionary
4. fuzz by evaluating the summary directly (this should be a lot faster than actually running the evm), use standard mutation heuristics on the seed in the dictionary. Fallback to direct evm execution for Partial branches (perhaps even give Partial nodes enough data to be able to directly resume execution in a full interpreter).

steps 2,3, and 4 can be run in parallel. I am fairly confident that this approach would be very competitive with the best available evm fuzzers (even with the perf hit that we pay for using haskell).

[d-xo]

for ultimate fuzzer perf we could consider applying a futamura projection and compiling Expr down to c or x86 assembly and executing that directly. This would also allow us to make use of e.g. afl for instrumented fuzzing, and use the symbolic exec features in hevm to to seed the afl dictionary with interesting values.

https://github.com/uni-due-syssec/efcf-framework

[gustavo-grieco]

I know this is an old discussion but was the futamura projection consider at some point. How much work involved? (I don't even know if there is a good way to do it in Haskell but I'm interested on this feature).

[gustavo-grieco]

Another approach will be to take the SMT formulas and convert them to LLVM code in order to compile and fuzz them using libFuzzer. this project implements this exactly: https://github.com/mc-imperial/jfs

[msooseth]

This SMT compilation is actually a really nice way of doing it. Adding that as an SMT solver would be great, honestly.

As a side-note, it's useful to keep in mind that the majority of the formuas will be UNSAT, and this approach can only solve for SAT. However, it still is a very valuable work and should certainly be explored as e.g. one thread out of say, 8.

[gustavo-grieco]

jfs seems to be the closer to original vision of this issue, however jfs is also very outdated/unmaintained and fails to compile in modern versions LLVM. Another possibility is to run ParaFROST with conversts SMT formulas to run in GPUs (CUDA support only, for now). I think this is a very good option, since GPUs are there and we not using them for anything during FV/fuzzing campaings.

[msooseth]

jfs seems to be the closer to original vision of this issue, however jfs is also very outdated/unmaintained and fails to compile in modern versions LLVM.

Yeah, it's a classic research tool, only to get citations for the people who made it. Almost all academic software is like that unfortunately. It's sad.

Another possibility is to run ParaFROST with conversts SMT formulas to run in GPUs (CUDA support only, for now). I think this is a very good option, since GPUs are there and we not using them for anything during FV/fuzzing campaings.

Actually, this is by some people who tend to maintain their academic tools. So it likely will survive for (some?) years. Regarding the CUDA -- "for now" is a very unrealistic, it'd take very serious effort and deep expertise to rewrite it for anything else. It's beyond hopeful thinking. If anyone had the expertise to rewrite it to something else, I sincerely hope they are earning 500k/year on AI, as a base salary. Convincing them of working on this academic tool instead, for essentially free, for people who couldn't care less about your achievements unless there is a paper about it, is "slightly" unrealistic.

Anyway, ParaFROST is kinda cool, and I like the work. But I am not 100% convinced about running CDCL on GPGPUs. I think it's a cool achievement, but requires too much effort to maintain and too deep insight to keep improving. Compiling to bytecode/asm/llvm is likely a better long-term, maintainable option.

[gustavo-grieco]

It seems that ParaFROST only solves CNFs, so there is a requirement of converting the query before. I think Z3 can do, but the process also needs to do a couple of transformation which tend to solve the formula itself (the results is FALSE or a trivial formula with a single variable) so I'm not sure it will worth the effort for hevm 🤔

[msooseth]

Actually, the transformation is not direct to CNF in case of UF (uninterpreted functions) -- it's actually a set of queries. Even without UF, most BV (bitvector) solvers will not translate the whole thing directly to SAT immediately, instead, they often do incremental bit-blasting, thereby not generating a single CNF. ParaFROST is likely tuned to work in the one-shot setting, and may not work at all, or perform poorly in incremental mode. That is because incremental mode requires more careful information management and much faster startup times. These incremental queries tend to be quick, so the speedup of ParaFROST may not be worth it given that its startup is likely nontrivial.

To re-iterate, systems like ParaFROST are not really meant for the end-user. They could be made to work, but only in certain scenarios. With time, they may become what we want them to be -- but that's expected to be a lot of work. It took me almost a decade to get CryptoMiniSat to the point where the XOR part "just works" and can be enabled by default, running at all times. Other people are likely to be smarter and may be able to spend more of their time on refining things. But I don't expect it to be trivial, and ParaFROST is aiming to achieve more than what I was aiming for with CryptoMiniSat.

[gustavo-grieco]

A very primitive proof of concept for futamura projects of opcodes is here: #784, please take a look.