A taint analysis method for small program sections, based not on the size of the set of inputs to an output variable (numeric) but on the size of the set of possible output values of that variable, is introduced in this paper. More precisely, for a numeric variable V, the authors define its influence measure to be log₂ Card(F), where F is the set of values that can actually be obtained from any input. Newsome, McCamant, and Song regard the influence measure as a very simple channel capacity with the program section in the role of a channel. The main idea is to use the influence measure as a subtler indicator of tainting than the binary “taint/no-taint” approach that is widely used, which depends on input influence analysis.

The paper’s main claim is that influence measure significantly reduces both false positive and negative outcomes, relative to input taint methods. Obstacles to the application of the influence measure are carefully considered in the paper. A program section is converted (manually, it appears) to Boolean. Generally, this is possible if the section’s behavior can be modeled in terms of a Turing machine running in a fixed time bound as a function of input length. The authors describe their technique, but do not state whether semi-automation has been attempted. If the behavior involves branching execution paths or quantifiers, then this simple conversion will not work.

Given the Boolean for the section, a heuristic for estimating Card(F) using a binary search-driven range analysis is described, but the more important idea of the paper is the application of #SAT solvers to compute Card(F) as the number of satisfying truth assignments of the Boolean. Although there has been much work on #SAT solvers, since #SAT is P-complete, this approach seems to limit the section size.

Much of the paper is given to experiments on program sections in terms of computation time to obtain log₂ Card(F) (so Card(F) can vary over a range 2^k to 2^k+1 with only one bit variation in the influence measure) and resistance of the influence measure to false negatives and positives. There is much scope for further study of this approach to defending critical code.