[Soot-list] Bug: False positive in sink inside of try block after if statement

[Arzt, Steven]

Hi Miguel,

There is a pretty good example on page 16 in the document from your link. The explanation starts in the last paragraph of page 15. The edge from the predecessor is there, because if the statement that throws the exception might never be executed. Take this example:

a = 5;
try {
a = a * o.f;
}
catch (NullPointerException ex){
}
write(a);

If a NullPointerException happens on line 2, this line has no effect. The program acts like this in case of the exception:

a = 5;
write(a);

The exceptional control flow graph models this potential behavior. In our case, if you apply this definition and then apply the definition of a postdominator, you end up with something that not ideal.

Best regards,
  Steven

-----Original Message-----
From: Soot-list [mailto:soot-list-bounces at cs.mcgill.ca] On Behalf Of Miguel Velez
Sent: Friday, September 1, 2017 2:33 PM
To: soot-list at cs.mcgill.ca
Subject: Re: [Soot-list] Bug: False positive in sink inside of try block after if statement

Hi Steve,

I have been debugging the exceptional unit graph that is generated for the example I showed you, and other examples as well, and I did see that exceptional edges are created between all predecessors (e.g., "if A go to" and "a = true") of a unit that might throw an exception (e.g.,
Sink.sink(b)) to the caughtexception unit. Looking at the code in the ExceptionalUnitGraph class, in the buildExceptionalEdges method, there is this comment:

" We need to recognize:
   - caught exceptions for which we must add edges from the thrower's predecessors to the catcher:
   -all exceptions of non-throw instructions;
   - implicit exceptions of throw instructions.
"
I am not sure what this means. Further, I do not understand why the decision was made to add exceptional edges for all predecessors of a unit that might throw an exception. I found this tech report from 2003

http://ai2-s2-pdfs.s3.amazonaws.com/7cb5/0a2d0625da9377023e2e8a63a5b0ae8722b9.pdf

where they talk about exceptional unit graphs, but I still do not understand why the decision was made. Could you clarify that as well?

Regards,

Miguel Velez
On 9/1/17 5:21 AM, Arzt, Steven wrote:
> Hi Miguel,
>
> After looking into the problem a bit more, I found that it is quite interesting. Let's take this reduced example:
>
>           if(A) {
>               a = true;
>           }
>           try {
>               Sink.sink(b); // -> False positive is detected
>           } catch (Exception e) {
>               e.printStackTrace();
>           }
> 	foo();
>
> FlowDroid encounters the conditional that depends on the tainted value "A". Everything between that conditional and its postdominator is considered to cause an implicit data flow. So the question is: What is the postdominator of the conditional?
>
> Here, we have to understand that (post)dominators are computed on the 
> (exceptional) unot graphs in Soot. For the exceptional unit graph, the 
> following design decision has been made long ago: If a unit can throw 
> an exception, there is an edge from its predecessor to the exception 
> handler. In our example, this means that there is an edge
>
> 	 a = true; --->  Sink.sink(b);
>
> Consequently, the graph assumes that there can be a control flow from the assignment to the sink call. The assignment "a = true" is in a branch of a conditional on a tainted value, and therefore, we an implicit flow here.
>
> Or, getting back to the more technical definition using postdominators: The sink call is not the postdomintor of the conditional (as one would expect). The postdominator is the call to foo() in my modified example. Everything in between leads to an implicit flow.
>
> What can we do about this? Well, that's not trivial. We could patch Soot to support a different semantics for exceptional control flow graphs. It would not be trivial to define a new semantic, though.
>
> Best regards,
>    Steven
>
> -----Original Message-----
> From: Soot-list [mailto:soot-list-bounces at cs.mcgill.ca] On Behalf Of 
> Arzt, Steven
> Sent: Thursday, August 31, 2017 5:42 PM
> To: Miguel Velez <mvelezce at cs.cmu.edu>; soot-list at cs.mcgill.ca
> Subject: Re: [Soot-list] Bug: False positive in sink inside of try 
> block after if statement
>
> Hi Miguel,
>
> This is indeed a bug. For now, you can disable exception tracking and FlowDroid works. I'll look into the issue a bit more to find a proper fix.
>
> Thanks for reporting!
>
> Best regards,
>    Steven
>
> -----Original Message-----
> From: Soot-list [mailto:soot-list-bounces at cs.mcgill.ca] On Behalf Of 
> Miguel Velez
> Sent: Tuesday, August 29, 2017 7:39 PM
> To: soot-list at cs.mcgill.ca
> Subject: [Soot-list] Bug: False positive in sink inside of try block 
> after if statement
>
> I ran an analysis in the following code and I obtained a false positive:
>
>       public static void main(String[] args) {
>           Sink.init();
>
>           boolean A = Source.getOptionA(true);
>
>           boolean a = false;
>           boolean b = false;
>
>           if(A) {
>               a = true;
>           }
>
>           try {
>               Sink.sink(b); // -> False positive is detected
>           } catch (Exception e) {
>               e.printStackTrace();
>           }
>
>           if(a) {
>               System.out.println("");
>           }
>       }
>
> Variable `b`, which is used in the sink, but it is not tainted is reported a leak. I am using the following settings for the analysis:
>
> ic.setCallgraphAlgorithm(InfoflowConfiguration.CallgraphAlgorithm.SPARK);
>       ic.setEnableImplicitFlows(true); 
> ic.setCodeEliminationMode(InfoflowConfiguration.CodeEliminationMode.No
> CodeElimination);
>
>       ic.setInspectSinks(false);
>       ic.setAccessPathLength(10_000);
> ic.setDataFlowSolver(InfoflowConfiguration.DataFlowSolver.ContextFlowS
> ensitive);
>
> ic.setAliasingAlgorithm(InfoflowConfiguration.AliasingAlgorithm.None);
>       ic.setFlowSensitiveAliasing(false);
>       ic.setStopAfterFirstFlow(false);
>       ic.setEnableStaticFieldTracking(true);
>       ic.setEnableExceptionTracking(true);
>       ic.setMaxThreadNum(1);
>       ic.setOneSourceAtATime(true);
>
> Debugging in the ImplicitPropagationRule class, I saw that the jimple instruction that calls the sink method is considered to be inside of the first if statement. Adding any instruction in java code or a nop in jimple before the sink call gives the correct result.
>
> I am using the latest version of this repo, soot, heros, and jasmin. I cloned all those projects, imported them into IntelliJ, and compiled them.
>
> Can someone check if they get the same false positive to confirm it is a bug?
> --
> Regards,
>
> Miguel Velez
> _______________________________________________
> Soot-list mailing list
> Soot-list at CS.McGill.CA
> https://mailman.CS.McGill.CA/mailman/listinfo/soot-list
> _______________________________________________
> Soot-list mailing list
> Soot-list at CS.McGill.CA
> https://mailman.CS.McGill.CA/mailman/listinfo/soot-list
> _______________________________________________
> Soot-list mailing list
> Soot-list at CS.McGill.CA
> https://mailman.CS.McGill.CA/mailman/listinfo/soot-list

_______________________________________________
Soot-list mailing list
Soot-list at CS.McGill.CA
https://mailman.CS.McGill.CA/mailman/listinfo/soot-list