Data flow: Introduce ContentSet

[hvitved]

Background

In Ruby, we are tracking flow through arrays with precise array index information, when available. That is, we are correctly able to handle

a[0] = tainted;
a[1] = not_tainted;
sink(a[0]); # bad
sink(a[1]); # good

Flow is tracked using the data flow library's notion of contents, reads, and stores, and we can model known/unknown array information as follows

newtype Content =
  KnownArrayElementContent(int i) { i in [0 .. 10] } or
  UnknownArrayElementContent()

Then the following statements

a1[0] = b1
a2[x] = b2
a3[1]
a4[x]

correspond to the following read/store steps

graph TD
  B1[b1]-->|"store(KnownArrayElementContent(0))"| A1["[post update] a1"]
  B2[b2]-->|"store(UnknownArrayElementContent())"| A2["[post update] a2"]
  A3-->|"read(UnknownArrayElementContent())"| A3I
  A3[a3]-->|"read(KnownArrayElementContent(1))"| A3I["a3[1]"]
  A4[a4]-->|"read(UnknownArrayElementContent())"| A4I["a4[x]"]
  A4-->|"read(KnownArrayElementContent([0..10]))"| A4I

Loading

assuming that x does not have a known constant value.

The Problem

In the example above, we can see how a4[x] gives rise to 11 read steps, since we need to be able to read out values stored at any known or unknown index. Unfortunately, we need to encode this up-front in the readStep relation, which means that all such reads will be replicated 11 times, and it would become even worse if we were to increase the range of KnownArrayElementContent.

Another issue is that when the data-flow library generates reverse store steps from read steps

a[x][1] = taint

we will get the following reverse store steps

graph TD
  A["[post update] a[x]"]-->|"store(UnknownArrayElementContent())"| A1["[post update] a"]
  A-->|"store(KnownArrayElementContent([0..10]))"| A1

Loading

whereas what we really wanted was just a single store step

graph TD
  A["[post update] a[x]"]-->|"store(UnknownArrayElementContent())"| A1["[post update] a"]

Loading

A Solution

This PR proposes a solution to both problems above, where we generalize the interface of the data-flow library for readStep and storeStep, to use a new type ContentSet instead of Content. ContentSet will allow us to represent sets of Contents:

newtype ContentSet =
  SingletonContent(Content c) or
  AnyArrayElementContent()

And we will be able to interpret ContentSets differently, depending on whether they occur in reads or in stores

Content getAStoreContent(ContentSet set) {
  set = SingletonContent(result)
  or
  // for reverse stores
  set = AnyArrayElementContent() and
  result = UnknownArrayElementContent()
}

Content getAReadContent(ContentSet set) {
  set = SingletonContent(result)
  or
  set = AnyArrayElementContent() and
  (result = UnknownArrayElementContent() or result = KnownArrayElementContent(_))
}

We will still be using Contents in access paths, but we will use ContentSets internally, and the data-flow library will make sure to avoid fan-out duplication via getAStoreContent/getAReadContent.

Returning to the original example

a1[0] = b1
a2[x] = b2
a3[1]
a4[x]

we will now have the following read/store steps:

graph TD
  B1[b1]-->|"store(SingletonContent(KnownArrayElementContent(0)))"| A1["[post update] a1"]
  B2[b2]-->|"store(AnyArrayElementContent()))"| A2["[post update] a2"]
  A3-->|"read(SingletonContent(UnknownArrayElementContent()))"| A3I
  A3[a3]-->|"read(SingletonContent(KnownArrayElementContent(1)))"| A3I["a3[1]"]
  A4[a4]-->|"read(AnyArrayElementContent())"| A4I["a4[x]"]

Loading

And for

a[x][1] = taint

we get just a single reverse store step

graph TD
  A["[post update] a[x]"]-->|"store(AnyArrayElementContent())"| A1["[post update] a"]

Loading

which translates via getAStoreContent into a store into UnknownArrayElementContent as desired.

PR Structure

This PR is structured into a sequence of logically self-contained commits, and I strongly encourage reviewing them in order:

• a5040fd: Adds a Ruby test for the reverse store example above.
• 309fd93: Introduces ContentSet into the data-flow library.
• c4fbc61: Syncs the data flow files.
• 725d76e: Implements ContentSet for Ruby, as per the description above.
• d99bb65: Implements ContentSet for C++ as a simple bijection into Content.
• b91858e: Implements ContentSet for Java as a simple bijection into Content.
• 7113c1b: Implements ContentSet for C# as a simple bijection into Content.
• 57f2a74: Implements ContentSet for Python as a simple bijection into Content.
• 415a1c2: Updates shared Java/C# code for generating flow summaries.
• cee527e: Updates the documentation on the shared data flow library.

[hvitved]

I have pushed another commit that is not strictly needed yet (it will be for #7914), but it belongs logically with this PR.

[asgerf]

I think there's a point in the design space worth talking about here. In the literature of (sound) JavaScript analysis the standard solution is to have two "unknown" contents rather than one:

• StoredWithUnknownKey: any store with an unknown key will write to here
• ReadWithUnknownKey: any read with unknown key will read from here

The rule is then:

• Store to unknown key: writes to StoredWithUnknownKey and ReadFromUnknownKey
• Store to known key K: writes to K and ReadFromUnknownKey
• Read from unknown key: reads from ReadFromUnknownKey
• Read from known key K: reads from K and StoredWithUnknownKey

(Another common solution is to collapse a heterogenous array into a homogenous array as soon as any operation acts on it with non-constant index, but that is hard to apply in our setting).

I can't immediately say whether this is better than ContentSet, or if it actually maps down to the same thing. I guess you'd still need to inform the core library that the reverse of ReadFromUnknownKey is StoredWithUnknownKey. And in terms of writing access paths by hand, I can certainly see the convenience in being able to talk about the "unknown element" without having to specify if it's the read or write variant.

Anyway, this isn't meant as an objection, just thought I'd mention it in case it helps somehow.

[aschackmull]

I think the StoredWithUnknownKey and ReadFromUnknownKey approach sounds promising, although I'd probably tweak it a bit to be StoredWithUnknownKey and StoredWithKnownKey instead with the following rules:

• Store to unknown key: writes to StoredWithUnknownKey
• Store to known key K: writes to K and StoredWithKnownKey
• Read from unknown key: reads from StoredWithUnknownKey and StoredWithKnownKey
• Read from known key K: reads from K and StoredWithUnknownKey

This should be equivalent, but ought to perform a bit better in an analysis that is forward-first, as our is.

[hvitved]

Thanks for your inputs @asgerf and @aschackmull . I agree that the above should work as well (except we would still have to handle reverse stores), but I think I have a slight preference for the ContentSet approach because:

1. As @asgerf points out, there will be only one "unknown element" content, so logic that works with Contents (such as inspecting access paths inside PathNodes) will not have to know about the two types of unknowns. And, if we for some reason care about the exact index, we will lose that information when a store is matched up with an uknown read.
2. One could imagine future extensions based on range analysis, where we will be able to refine unknown reads/stores based on known bounds. With the ContentSet approach, we would again not have to touch Content, but only define new (internal) ContentSet entities and define their interpretation in terms of getAStoreContent and getAReadContent.

[aschackmull]

As discussed offline: Let's move the store-related ContentSet-to-Content join into DataFlowImplCommon and reduce the diff in DataFlowImpl for the store steps.

[aschackmull]

This join-order is not optimal, but presumably good enough. Realising the optimal order would require another helper predicate, so I'm not suggesting any change here, merely noting the fact.

[aschackmull]

LGTM.