[Soot-list] Clarification on the Behavior of HEROS

[Eric Bodden]

Hello.

> Is the Heros solver working by defining some constraints and then
> propagating them, or is it traversing the exploded graph on the fly?

It's doing the latter.

> class Foo{
>
> String a = "meh";
>
> void setA(String b){
>    a = new String(b);
> //new String to avoid a simple case where they're plainly aliased
> }
>
> String getA(){return a;}
>
> }
>
> If I am to use this as follows:
>
> Foo f = new Foo();
> String t = f.getA(); //gets meh
> f.setA(taintedString);
>
> String s = f.getA(); //gets tainted string
> sink(s);
>
> What happens in this case? Is the taint fact going to go from
> taintedString to Foo.a to s? If so, would t be considered possibly
> tainted too (as it dereferences the same field)? Will Heros request a
> re-analysis of that call after I set the fact in f.setA(taintedString)?

Ah, now I see what you mean. What you are actually asking is whether
the solver is context sensitive - and yes, it is! Calls like getA are
going to be re-evaluated anew at every call site. I suggest you read
the original IFDS paper by Reps, Horwitz and Sagiv...

Having said that, let me make clear that Heros is a *framework* for
defining data-flow analyses, and that it's generally up to the user to
decide how precisely fields, etc., will be handled. The example taint
analysis I included with Heros won't track such fields. So that's
something you as a user will have to code appropriately in the flow
functions. We are currently working on a taint analysis that treats
such issues precisely but are still struggling with finding the right
performance/precision tradeoff.

Eric