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

[Miguel Velez]

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.NoCodeElimination);
>
>       ic.setInspectSinks(false);
>       ic.setAccessPathLength(10_000);
> ic.setDataFlowSolver(InfoflowConfiguration.DataFlowSolver.ContextFlowSensitive);
>
> 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