Accessing Symbolic State or Path Conditions in CrossHair for Research Use

[Stefania-P11]

I’m working on extending DIG (https://github.com/dynaroars/dig), a tool that uses CIVL to generate invariants for C programs, to support Python analysis. I’m exploring how CrossHair might fit into this pipeline.

I have two main questions:

1. Does CrossHair internally generate symbolic states over inputs during execution? If so, is there a way to extract or inspect those symbolic states?

2. Is there a way to obtain path conditions at a specific program point — e.g., by inserting an assert and retrieving the input constraints that reach that point?

Any pointers on how CrossHair handles symbolic state under the hood or where to hook in would be greatly appreciated.

[pschanely]

I’m working on extending DIG (https://github.com/dynaroars/dig), a tool that uses CIVL to generate invariants for C programs, to support Python analysis. I’m exploring how CrossHair might fit into this pipeline.

Neat stuff!

1. Does CrossHair internally generate symbolic states over inputs during execution? If so, is there a way to extract or inspect those symbolic states?
2. Is there a way to obtain path conditions at a specific program point — e.g., by inserting an assert and retrieving the input constraints that reach that point?>
   Any pointers on how CrossHair handles symbolic state under the hood or where to hook in would be greatly appreciated.

CrossHair does internally generate symbolic states, and it's possible to extract these, but there are caveats. You can do something like what's discussed here:

• When operating outside CrossHair's normal "tracing" context (within a NoTracing() context), the true class of a symbolic value (e.g., <class 'crosshair.libimpl.builtinslib.SymbolicInt'>) becomes visible.
• You can access the underlying Z3 variable(s) of any CrossHair symbolic object using its .var attribute. For instance, symbolic_x.var would return the underlying Z3 variable. This allows you to build or inspect Z3 expressions directly.
• Dumping Solver State: For more comprehensive inspection of the constraints accumulated for a given execution path, you can dump the entire SMT solver state. This can be achieved by adding a line like print(state.solver.sexpr()) within a NoTracing() context. This outputs the SMT-LIB representation of all current path constraints.

You will have a few challenges here: first, there are often many different ways to model a Python value in SMT, and sometimes (e.g. right now, floats) CrossHair will even try different ways of modeling the same Python type. If you're limiting yourself to integers, this probably isn't a problem however. Second, CrossHair is more attempting to be a smart fuzz tester than a software verification tool and makes design decisions that may be less appropriate for your use case. In particular, nearly anything with a loop will have an infinite number of execution paths, and so you will not be able to exhaustively determine invariants.

Please also check out the discussion in this issue and perhaps this one!

I can help out if you decide that you want to proceed with some sort of integration - LMK!