Add motivating example from Smartian to research examples

[webthethird]

Add echidna-fied version of Smartian motivating example.
Original: https://github.com/SoftSec-KAIST/Smartian/blob/main/examples/sol/motiv.sol

[gustavo-grieco]

Thanks a lot for the contribution. We want to add this example, however, since every research example is added into the CI testing and echidna does not quickly trigger this issue. If that is solved, then we can add this example.

[webthethird]

That makes sense!

[webthethird]

It seems like making use of the msg_sender and/or functions_relations properties in the SlitherInfo input would help trigger the bug faster. As you mentioned on Slack, re: the generationGraph created when parsing the functions' "impacts" and "impacted by" properties,

Echidna is not using that yet. However, we are unsure about it. It seems to be easier to just randomly select functions instead. We want to see that this will help in general, not only this micro benchmark.

My (possibly naive) understanding is that the Smartian paper essentially proved that such data-flow analysis does help in general, at least on the benchmarks they evaluated it against (see section V.B in that paper, where they compared the tool against itself with the analyses disabled).
Is there a branch of the Echidna repo in which this generation graph is used, which one could test on a wider variety of contracts to determine if it does help in general?
Aside from the functions_relations and related generationGraph, it seems like the msg_sender property would be much easier to utilize, and should clearly be helpful in general since it would avoid sending transactions that are sure to fail. Is there any work being done to integrate this? Seems like it would be a very useful contribution!

[gustavo-grieco]

My (possibly naive) understanding is that the Smartian paper essentially proved that such data-flow analysis does help in general, at least on the benchmarks they evaluated it against (see section V.B in that paper, where they compared the tool against itself with the analyses disabled).

Smartian and Echidna are different tools and therefore, it could be the case that the improvements that such data-flow analysis are absorbed by other things we do, however, we want to see concrete evidence on small and large contracts to decide.

Is there a branch of the Echidna repo in which this generation graph is used, which one could test on a wider variety of contracts to determine if it does help in general?

We don't have code yet, the graph should be parsed from slither and then the generation should be tweaked to use probabilities given the last generated transactions (e.g. just executed A, let's execute B or C).

Aside from the functions_relations and related generationGraph, it seems like the msg_sender property would be much easier to utilize, and should clearly be helpful in general since it would avoid sending transactions that are sure to fail. Is there any work being done to integrate this? Seems like it would be a very useful contribution!

Another potential improvement that we have not integrated yet, happy to heard ideas about that. In particular, to know exactly what to do if code depends on msg.sender.

[dguido]

@gustavo-grieco wondering if echidna finds this bug faster now, and this can get merged?

[gustavo-grieco]

While symbolic execution helps here, in the exploration mode, triggering the actual bug requires more than a single transaction (which is implemented right now). Triggering with a single transaction in exploration mode is possible, but it is not reliable enough to add it into the research examples yet. I think we should wait until we can chain sequences in symbolic mode, which is not very far away in terms of roadmap.

[gustavo-grieco]

It took a few years, but finally we have all the components to solve this properly using symbolic execution. PR #1538 includes this example almost without modifications as a test, so let's close this one. Sorry for the delay @dguido !