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

[Arzt, Steven]

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