Trying concrete values when path execution timeout reached?

[amacfie]

Consider the following function:

def f1(n: int) -> int:
    '''
    pre: n >= 0
    post: n % 2 == __return__ % 2
    '''
    ret = n
    while ret > 0:
        if ret == 10_000:
            ret -= 1
        ret -= 2
    return ret

CrossHair can find and add the constraint 10_000 == n, but thereafter it merely iterates through the loop a few times, adding superfluous constraints, and eventually times out and doesn't notice it found a refutation. How about, when a path execution timeout is reached, CrossHair generate a few concrete realizations of the inputs consistent with current constraints and just run the function on them to completion and test the postcondition?

Of course when running the function on concrete values we'll still want to impose a timeout (and block I/O) but it should be able to get much further.

Addendum: I now see this as less important since this method is good for getting through loops.

[pschanely]

Great idea.
So, we already do a small variant of this! Repeated path timeouts (and also CrossHairUnsupported exceptions) can slowly encourage us to "pre-realize" inputs. If you run something like this,:

crosshair check your_example.py -v --per_condition_timeout=15

You'll see it eventually starts running iterations with comments like Prematurely realizing <class 'int'> value.
Unfortunately, this realization isn't random, and the solver just sort of naturally attempts incrementing values, so we never attempt an input like 10000.

Now, I've got another branch of work that I think will make this better, though not exactly in the way you're proposing.
I'd like to have CrossHair run Atheris in parallel to the symbolic mode. I believe that we can have the two systems share information (other systems like CrossHair do things like this):

• Seed inputs from the fuzzer can be used as candidates for the "premature realization" I described above.
• We can generate inputs for CrossHair path executions, and feed them as seeds to the fuzzer.

In the ideal world, both systems can help the other get past difficult parts of the logic.

One blocker here is that there aren't prebuilt Atheris packages. But there is a fair amount of engineering needed to make get this strategy from concept to reality.

[amacfie]

One blocker here is that there aren't prebuilt Atheris packages. But there is a fair amount of engineering needed to make get this strategy from concept to reality.

Let me know if I can help:)

[pschanely]

Would LOVE some help. I just pinged that atheris thread - we'll see! I was thinking I might try to use cibuildwheel on Github Actions to do the builds. If the atheris folks are ok with it, maybe you want to see whether you'd be able to get that working? It's further complicated by the fact that we need to also build LLVM on Mac - this took a very long time on my local machine (and I had to reduce the -j parameter to avoid running out of memory!).

[amacfie]

Looks like they're going to publish some builds.

In the original example, if CrossHair finds the state n == 10_000 but times out, would we generate an input satisfiying the constraint and give it to Atheris as a seed input (aka initial corpus)?

[pschanely]

Yes - exciting!
And, yes, I think we should give such inputs to Atheris. Note that you can add seeds to Atheris while it's running too! So, I'd suggest that we kick both off right away, and dump inputs for every CrossHair path execution into a corpus input. CrossHair will naturally tend to get coverage, and that sort of thing is exactly what the fuzzer wants.

[amacfie]

Here's a variation of the idea: on timeout, instead of realizing all inputs and running the function to completion, realize only the inputs that appear in the most-recently-added constraint and continue symbolic execution. This might help get out of loops without realizing more variables than necessary. Or maybe those inputs are realized and also added to a set of inputs that are subject to coverage-driven random mutation. I guess the "coverage" of a realization of a subset of inputs would be the overall
coverage (defined as usual e.g. lines) achieved by all iterations of symbolic execution with those inputs realized and the rest symbolic. Or something?

[pschanely]

Ah, so indeed there are already some minimal tactics for realizing a subset of input parameters. I suspect you've got some ideas in here that could make that quite a bit more effective. I have not yet put much thought into using randomized mutation and symbolics together, but it's an interesting line of thought!

One reason I think I'm inclined to integrate Atheris as a first step: Even with fully realized inputs, CrossHair runs MUCH more slowly than stock Python; this is largely because we are tracing per-opcode (via sys.settrace) with a pure Python callback, which intercepts quite a lot of built-in functions and operations. Re-writing this callback as a native extension would help mitigate some of that overhead however.

[amacfie]

Re-writing this callback as a native extension would help mitigate some of that overhead however.

Sounds valuable, maybe create an issue? (I'd do it if I were a C programmer.)

[pschanely]

Agreed; filed #115!