[PATCH] D28445: [Analyzer] Extend taint propagation and checking

Tue Jan 10 09:14:55 PST 2017

NoQ added a comment.

Thanks for working on the taint! I really wish the taint analysis in the analyzer to flourish, and the part you've digged into is particularly sensitive, so i'd dump some thoughts here, hopefully helpful.

**What works as it should: **

> In the second example, the SVal obtained in `GenericTaintChecker::getPointedToSymbol()` is a `LazyCompoundVal` so `SVal::getAsSymbol()` returns a NULL SymbolRef, meaning the symbol is not tainted.

Only symbols currently can, and in my opinion ever should, directly carry taint.

We have symbols, regions, concrete values, and compound values.

A symbol //$s// denotes a particular but unknown value from a certain set //**S**// (say, of all integers or all pointers); we are not generally sure if it can denote any value from //**S**//, or only from a smaller subset //**S'**// within //**S**// (for example, the analyzer may be unaware that //$s// is always positive, because the small part of the code it's looking into doesn't give any hints). Analyzer also gathers constraints //**C**// when he picks execution paths - for instance, on a branch condition "//if ($s < 5)//", if we pick the true branch, //**C**// gets cropped into //[-INT_MIN, 4]//, and the possible values of //$s// stay within //**S'**// intersected with //**C**//, while the analyzer thinks that possible values of //$s// are within //**S**// intersected with //**C**//.

A tainted symbol merely corresponds to the special case when we know that //**S'** = **S**//, which we normally don't - that is, the analyzer knows that for some reason the symbol's value is so much chaotic that it may definitely take any value from //**S**// in run-time. The analyzer can know it by seeing that the symbol comes from an "untrusted source" such as from "outside".

We do not really talk about tainted regions - instead, we talk about tainted pointer values, which are symbols. In this sense, in code

  char buffer[100];

the region of variable `buffer` cannot be tainted. No matter what we do, the buffer region itself comes from a perfectly trusted source - it's always in the same well-known segment of memory (stack or in global memory). In practice this means that the attacker cannot affect or forge the positioning of this segment in any way. On the other hand, if //$i// is a tainted index symbol, then region //buffer[$i]// of the //$i//'th element would be "said to be tainted" - in the sense, its pointer is known to possibly take any value, not necessarily within range of the buffer. Similarly, if a pointer-symbol is tainted, the segment of memory (region) it points to (called `SymbolicRegion`) is "said to be tainted". So //whenever we're talking about a "tainted region", it's always a shorthand for talking about a certain tainted symbol//.

Concrete values shouldn't be tainted for the same reason - they are already "known", their //**S**// would consist of one element, so there's little interest in saying that they can take any value from this set - they're bound to take that only value.

Now, we have (possibly lazy) compound values. The whole point of compound values is that they consist of multiple other values, and therefore there's usually little sense in even considering them as a whole. Some sub-values of them may be null, over-constrained, uninitialized, irrelevant (eg. padding), or tainted, while other sub-values may be completely different. In your example, you obtain a compound value of an array, which consists of all values of all elements of the array. There's no point in asking if the compound value itself is tainted; instead, you might be interested in particular elements. For example, `buffer[1]` may be tainted, while `buffer[2]` was overwritten with `'\0'` and is no longer tainted. If you had a structure, you may ask if a certain field is tainted, or if all fields are tainted.

**What works but not as it should:**

> In the first example, buf has it's symbol correctly extracted (via `GenericTaintChecker::getPointedToSymbol())` as a `SymbolDerived{conj_$N{char}, element{buf,0 S64b,char}}`.

Nope, unfortunately, in fact this is not correctly extracted either. This symbol denotes the value of the first element of the buffer. The taint checker marks the first element as tainted, and then later reads that the first element is tainted, and throws the warning. However, if we pass, say, `buffer+1` to `execl`, it breaks.

The root cause of the problem is how the analyzer denotes casted/typed pointers: the `SVal` for a pointer of type `T*` is said to be the element region with index 0 of the region behind the pointer. You can read this as "The pointer points to the first `T` on this segment of memory". In this case, we try to say that the value behind the pointer is tainted, and we forget that the value behind the pointer is not only the first element of the array, but the whole array, even though the pointer points to the first element only.

How this should work: //we should instead put the taint over the conjured symbol//, on which the derived symbol you mention is //based//. The conjured symbol denotes the unknown noise that wipes the whole array after reading tainted data into it, which in other words means that it denotes the tainted data itself. Derived symbols denote values for sections of this noise that correspond to sub-regions. You have already seen from the code that derived symbols inherit taint from parent symbols (on which they are "based", or from which they are "derived"), so if we taint the conjured symbol, then all the derived symbols for all elements will be tainted automagically; however, elements overwritten later will not carry taint.

Then when you try to find out if the value passed to `execl` is tainted, some imagination is required to conduct a proper check. You definitely shouldn't try to inspect the same conjured symbol - instead, this time you should try to pay attention to the elements. Probably the first element's being tainted is already a good time to panic. Probably you could improve upon this by scanning until a null character and see how much taint is there. So the taint-discovering code currently works more or less correctly, but it requires a different version of `getPointedToSymbol` than the taint-origination code discussed above.

**What doesn't work and you're trying to fix:**

Now you observe that by changing the array-to-pointer cast syntax slightly, you make the analyzer core drop the element region (which, as i mentioned, only represents pointer casts) from your lvalue - and receive the rvalue of the whole array (the lazy compound value of all elements), instead of the rvalue of the first element (the derived symbol).

How it should work? Same as above: when adding the initial taint, we should instead put the taint over the conjured symbol. //It is the pointed-to symbol you're looking for.// Similarly, when detecting tainted values, we should unpack the lazy value and see if its elements or fields in which we are interested are tainted.

**Regarding the origin regions:**

Origin regions for `SymbolRegionValue`,  and even more so for`SymbolDerived`, and even more so for `LazyCompoundVal`, are immaterial for most purposes. Usually the region isn't at fault that a certain tainted value was written into it.

Well, in case of `SymbolRegionValue`, he is actually at fault, because if the origin region is a pointer that comes from "outside", then the values that came with it may also have been forged; after all, `SymbolRegionValue` denotes "what have been there in this region before we noticed".

However, the value of `SymbolDerived` is known to be a "sub-section" of the parent symbol, and no matter how hard you try to forge the parent region, you can't change that fact. So unless the parent symbol is tainted, we shouldn't call the derived symbol tainted.

You may say that if the parent region's address can be an arbitrary forged pointer, then deriving the symbol may cause buffer overflow and therefore denote a forged data. Unfortunately, our implemenetation of the `Store` allows such examples, but ideally it shouldn't construct a `SymbolDerived` for such cases.

Finally, `LazyCompoundVal`'s origin (parent) region is also not at fault. The value only captures the contents of this region. All we know is that at some prior point of time contents of this region were as represented by the lazy compound value. But because this moment occurs during analysis, the value has little connection with the region; this region may have been overwritten many times, completely or partially, with values of completely different nature, both before and after taking the snapshot we call a lazy compound value.

**What to do:**

I'd suggest to consider moving taint to the invalidation-related conjured symbols. It wouldn't be easy because API of the Store doesn't allow obtaining this symbol easily, so it needs some work, which would be useful for other purposes as well (this is brought up often in C++ discussions, where we also need to work with complete structures a lot, eg. iterators).

https://reviews.llvm.org/D28445