Partial Concrete Storage for symbolic execution

[ethever]

A fully symbolic contract storage is not always a desirable option when performing symbolic execution. In fact, when analyzing the state of a contract at a specific block, you might want to use the concrete values in its storage to prune some unfeasible paths and simplify the symbolic execution.

When this mode is activated and greed encounters an SLOAD (let's say at slot id 0x5), greed will automatically fetch the concrete value of slot 0x5 in the contract's on-chain storage at block NUMBER (18808898) instead of using an unconstrained symbol. Similarly, any subsequent (and possibly symbolic) SSTORE at slot 0x5 will overwrite its value.

** In other words, you can imagine this mode of operation as a "lazy" initialization of the contract's storage in the symbolic executor that uses its on-chain storage at the specified block. **

related source:
https://ucsb-seclab.github.io/greed/advanced/

[ggrieco-tob]

Isn't this implemented in echidna (which uses hevm) already?

[msooseth]

It is certainly possible to set up the state partially/fully symbolically. However, the CLI only allows for this in some cases. For example, with #526 you can set up the caller to be concrete. Similarly for initial storage for #509 . More could be done, but how it should be controlled by the user is unclear. The ones supported are the relatively clear ones. What granularity would be useful, you think? What do you think, how should the user be able to control it?