[Soot-list] Clarification on the Behavior of HEROS

[Eric Bodden]

Hi.

> I think I have a more twisted example for you.
>
> class myServlet ...{
> private String a;
>
>
> doGet(...){
>    response.getWriter().println(a);
> }
>
> doPost(...){
>    a = request.getParameter("meh")
> }
> ...
> }
>
> Assuming that the Heros solver handles the call to doGet first, and
> doPost second, what is going to happen? Is the field a going to be
> considered as untainted in doGet, then marked as tainted in doPost, and
> then doGet be reprocessed? Because a naive exploration of the exploded
> graph would simply consider a as untainted in doGet.


That depends on how the methods are actually called in the analyzed code.
Assume we have those calls:

doGet(..)
doPost(..)
doGet(..)

Then at the first call to doGet() it's considered untainted but then
tainted at the second call.

> And no, I can't force the generated entry point to give them a specific
> order to try to relieve the problem - because we can have a more twisted
> mess like this:

Ok, if you don't have actual driver code that calls those methods in
sequence then the best thing you can do is generate an
over-approximate driver. For the example, this should work:

while(true) {
   if(i==0)
       doGet(..)
   if(i==1)
       doPost(..)
}

Here "i" needs to be assigned some non-constant value such that Soot
won't be optimizing away the checks. In essence, this will tell the
solver that doPost and doGet could happen in any order, also
repeatedly.

Eric