secure-software-engineering / FlowDroid

FlowDroid Static Data Flow Tracker
GNU Lesser General Public License v2.1
1.02k stars 293 forks source link

Nondeterministic Results from DataFlowSolver Flow Insensitive. #583

Closed Pancax closed 1 year ago

Pancax commented 1 year ago

Hello,

I have recently been using Flowdroid and noticed what I think could be an issue in the option -ds FLOWINSENSITIVE.

Description

Originally, I was investigating the Flowdroid commit 72734bd629dfae2aacaf6e6973abfe73d035c979 but I have confirmed that a similar behaviour is present in the more recent commit f29b1d77221b7a44fe1e157aca7d96f5bebbc299. When running the command line Flowdroid with the command java -jar ../soot-infoflow-cmd-jar-with-dependencies.jar -a 'apk' -s .... -p ... -ds FLOWINSENSITIVE where the apk is produced from this (this project is actually AnonymousClass1 from Droidbench, modified slightly to build with Gradle and should produce an equivalent APK to the original) - I receive nondeterministic results from Flowdroid. I have observered this behaviour across multiple machines, on both Mac and Ubuntu (and in Docker containers).

Results

Running Flowdroid (on Ubuntu 22.04) 20 times with the above configuration results in

Thoughts

All of these flows are True Positives in the AnonymousClass1 project, I don't think this is the expected behaviour but I could be wrong, is this expected?

I cannot pinpoint exactly what is causing this behaviour because I have only a basic understanding of the solver code. From my investigation, whenever I modified Flowdroid's code (in the older commit, have not tried this on the later commit) to ignore using threads the results then became deterministic (20 runs & 20 outputs that were all getLongitude() -> log.i() in onResume()). This is, naturally, expected because using only 1 thread makes the order we propagate taint consistent but I am struggling to even understand how this could be the case. I would think that the order we process edges does not matter, we should still end up with the same flows at the end?

StevenArzt commented 1 year ago

FlowDroid should deliver deterministic results even in the multi-threaded case. However, we know that there is a strange bug somewhere. @timll has been investigating a flaky test case that sometimes returns one result (which is correct), and sometimes returns no result at all. Unfortunately, we have not yet fully understood why this happens.

What we know so far:

Some variability in the taints is expected. Each abstraction records its predecessor and a set of neighbors, each of which also has a predecessor. That means you can have equivalent taint graphs by moving between predecessors of the taint at the sink and predecessors of neighbors of that sink. It's conceptually the same, but the structure (i.e., what becomes "main" abstraction and what becomes a neighbor) is timing-dependent.

This makes debugging the analysis harder, because we can't just check for graph equivalence. We have different graphs, and sometimes traversing one of these graphs leads to fewer paths between sinks and sources (reconstruction is bottom-up). We're still thinking about a good way to really understand what the differences are (aside from the expected re-organization I mentioned). Only then, we can look into why these differences occur.

If we reduce the thread count to one, we deterministically get the same taint graph. However, this graph (as you have also found) seems to be correct consistently, i.e., doesn't help us with understanding the problem at hand.

If you have a new APK file (which is not yet part of our test suite) that exhibits a similar behavior, we can try to look into the problem again based on your APK.