Unbounded Static Analysis

Christian Gram Kalhauge

Table of Contents

Dependent Values§1
1. Dependencies between different values.§1.1
Unbounded Static Analysis§2

In this section, we are going to revisit abstract interpretation from our previous session by discussing Dependent Values (§1). Then, we will show how we can perform Unbounded static analysis with no limits. To do this, we have to introduce fixpoints, the widening operator, and finally, a more efficient algorithm.

Dependent Values §1

A big problem, which we have glossed over so far, is dependent variables. Dependent variables are variables whose solution spaces are constrained by each other.

Safe Div By N

Consider the case in Dependent.safeDivByN:

@Case("(0) -> ok")
@Case("(1) -> ok")
public static int safeDivByN(int n) { 
  if (n != 0) {
    return 1 / n;
  }
  return 0;
}

If we run our sign analysis naively on the decompiled code, we get the following. The offset column shows the offset, the instruction column shows the instruction, and the abstract state column shows the abstract state right before the instruction and at which instructions the results are stored.

Offset	Instruction	Abstract State
`000`	`load:I 0`	$⟨ {0 \mapsto {+, -, 0}}, ϵ, 0 ⟩ \to {1}$
`001`	`ifz eq 6`	$⟨ {0 \mapsto {+, -, 0}}, {+, -, 0}, 1 ⟩ \to {2, 6}$
`002`	`push:I 1`	$⟨ {0 \mapsto {+, -, 0}}, ϵ, 2 ⟩ \to {3}$
`003`	`load:I 0`	$⟨ {0 \mapsto {+, -, 0}}, {+}, 3 ⟩ \to {4}$
`004`	`binary:I div`	$⟨ {0 \mapsto {+, -, 0}}, {+} {+, -, 0}, 4 ⟩ \to {5, err (‘𝚍𝚒𝚟 𝚋𝚢 𝚣𝚎𝚛𝚘’)}$
`005`	`return:I`	$⟨ {0 \mapsto {+, -, 0}}, {+, -}, 5 ⟩ \to {ok}$
`006`	`push:I 0`	$⟨ {0 \mapsto {+, -, 0}}, ϵ, 6 ⟩ \to {7}$
`007`	`return:I`	$⟨ {0 \mapsto {+, -, 0}}, {0}, 7 ⟩ \to {ok}$

The problem with the above execution is that we find a divide by zero error, even though it does not exist. This happens because we do not capture the dependency between the integer on the stack and in the locals during the choice at 001.

To fix this, we need to add a notion of named values and constraints. In the example above, we could add a named value $n$ with constraint $n = {+, -, 0}$ indicating that values are the same. We can keep these constraints in addition to the state:

Offset	Instruction	Abstract State
`000`	`load:I 0`	${n \mapsto {+, -, 0}} / ⟨ {0 \mapsto n}, ϵ, 0 ⟩ \to {1}$
`001`	`ifz eq 6`	${n \mapsto {+, -, 0}} / ⟨ {0 \mapsto n}, n, 1 ⟩ \to {2, 6}$
`002`	`push:I 1`	${n \mapsto {+, -}} / ⟨ {0 \mapsto n}, ϵ, 2 ⟩ \to {3}$
`003`	`load:I 0`	${n \mapsto {+, -}} / ⟨ {0 \mapsto n}, {+}, 3 ⟩ \to {4}$
`004`	`binary:I div`	${n \mapsto {+, -}} / ⟨ {0 \mapsto n}, {+} n, 4 ⟩ \to {5}$
`005`	`return:I`	${n \mapsto {+, -}} / ⟨ {0 \mapsto n}, {+, -}, 5 ⟩ \to {ok}$
`006`	`push:I 0`	${n \mapsto {0}} / ⟨ {0 \mapsto n}, ϵ, 6 ⟩ \to {7}$
`007`	`return:I`	${n \mapsto {0}} / ⟨ {0 \mapsto n}, {0}, 7 ⟩ \to {ok}$

Now we can see that we can constrain the state-space of the named values inside each of the branches, allowing for more precise results.

A couple of things to keep in mind when using named values are that:

They should not change. This means that if a variable, like a local, is overridden, we need to create a new named value, so that values copied out of the locals do and not change when the original variable changes.
Try to be smart about when to create named values and when to remove them again, as too many named variables might make your analysis slow.
Try to think about which instructions create dependencies between values. Some examples are dup and load, but array and field accesses do the same.

Dependencies between different values. §1.1

Cousot (1978)
??

It is possible to capture more interesting relationships between values. This is especially important when they depend on each other.

@Case("(0, 0) -> ok")
@Case("(1, 1) -> ok")
public static int safeDivAByB(int a, int b) { 
  if (a >= 0) {
    if (b > a) {
      return a / b
    }
  }
  return 0;
}

The example above contains no errors. But this would be hard for our current techniques to detect. To maintain these constraints efficiently, we can use Polyhedrons (Cousot 1978) or, most of the time, faster Octagons (??).

Unbounded Static Analysis §2

The problem with bounded static analysis is that even if we run our static analysis for 1,000,000 iterations, we have no guarantee that our program will not exhibit bad behavior in iteration 1,000,001. Unbounded Static Analysis seeks to fix this by running the static analysis until a fixed point is reached.

Fixed Points §2.1

Ideally, we want the smallest such fixed point, which we refer to as the Minimal Fixed Point.

Minimal Fixed Point

Given a function $f : A \to A$ , that is monotone over $(A, ⊑_{A})$ $(\forall a \in A . a ⊑_{A} f (a))$ then the minimal fixed point is the least $n$ st. $f^{n} (⊥) = f^{n + 1} (⊥) .$

$f^{n} (⊥)$ means $f (f (\dots f (⊥) \dots))$ , where $f$ is applied $n$ times.

Not all functions have a fixed point, but if one does, we can run the function until the result no longer changes, and then we know we don't have to continue running the analysis.

For example, given our $𝐒 𝐢 𝐠 𝐧$ abstraction, we are guaranteed a fixed point in no more than 4 iterations, as the height of the lattice is 4.

Adding One

Imagine a function adding one:

a (x) = x +_{𝐒 𝐢 𝐠 𝐧} α ({1})

We can make it into a monotone function by joining it with the value.

f (x) = x ⊔ a (x)

Now we can see that we will reach a fixed point on the zero set in only one step.

\begin{matrix} f^{0} ({0}) & = {0} \\ f^{1} ({0}) & = f ({0}) = {0} ⊔ {+} = {0, +} \\ f^{2} ({0}) & = f (f^{1} ({0})) = {0, +} ⊔ {+} = {0, +} \end{matrix}

The Interval Abstraction §2.2

However, not all abstractions form a lattice of finite height. One example of such abstractions is the interval abstraction.

Here, we represent a set of integers as an interval between two numbers.

Interval Abstraction

The interval abstraction $𝐈 𝐭 𝐯 𝐚 𝐥$ is a tuple of two numbers $i$ , $j$ , representing the interval of integers between $[i, j]$ , both inclusive.

\begin{matrix} α (S) & = [\min S, \max S] \\ γ ([i, j]) & = {n \in ℤ | j \geq n \leq i} \\ [i, j] ⊑_{𝐈 𝐭 𝐯 𝐚 𝐥} [k, h] & \equiv k \leq i \land j \leq h \\ [i, j] ⊔_{𝐈 𝐭 𝐯 𝐚 𝐥} [k, h] & \equiv [\min {i, k}, \max {j, h}] \\ [i, j] ⊓_{𝐈 𝐭 𝐯 𝐚 𝐥} [k, h] & \equiv [\max {i, k}, \min {j, h}] \\ ⊤_{𝐈 𝐭 𝐯 𝐚 𝐥} & = [- \infty, \infty] \\ ⊥_{𝐈 𝐭 𝐯 𝐚 𝐥} & = [\infty, - \infty] \end{matrix}

Implement the Interval abstraction.

Now implement the range abstraction in your language of choice. Remember to test your abstraction:

from hypothesis import given
from hypothesis.strategies import integers, sets

@given(sets(integers()))
def test_interval_abstraction_valid(xs):
  r = Interval.abstract(xs) 
  assert all(x in r for x in xs)

@given(sets(integers()), sets(integers()))
def test_interval_abstraction_distributes(xs, ys):
  assert (Interval.abstract(xs) | Interval.abstract(ys)) == Interval.abstract(xs | ys)

Implement Operations on Interval Abstraction.

Define the arithmetic operations you need to run your static analysis.

You can use hypothesis to test them; remember you want the operations to be an over-approximation:

@given(sets(integers()), sets(integers()))
def test_interval_abstraction_add(xs,ys):
  r = Interval.abstract(xs) + Interval.abstraction(ys)
  assert all(x + y in r for x in xs for y in ys)

Notice that the lattice of the interval abstraction does not have a finite height; we can always add 1 to either end of the interval.

Runs forever

Consider the following program:

void example() {
  int i = 0;
  while (i >= 0) {
    i = i + 1;
  }
}

In this case, our interval analysis will look something like this:

State	Comment
${}$	`int i = 0`
${i \mapsto [0, 0]}$	see that `i >= 0`
${i \mapsto [0, 0]}$	`i = i + 1`
${i \mapsto [0, 0] ⊔ [1, 1]}$	loop back
${i \mapsto [0, 1]}$	see that `i >= 0`
${i \mapsto [0, 1] + [1, 1]}$	`i = i + 1`
${i \mapsto [0, 1] ⊔ [1, 2]}$	loop back
...	...

This might continue forever, unless we find a better way.

The Widening Operator §2.3

(Nielson (2020) at page 110)

Because we are not guaranteed to reach a fixed point with the interval abstraction, we need to force it. This is known as the widening operator; the goal of the widening operator $\nabla$ is to dramatically over-approximate joins in a way that we are guaranteed a fixed point in a finite number of steps.

One way of adding a widening operator to the interval abstraction is to use a constant set, often referred to as $𝐊$ . This set contains all the constants in the program or file of interest. This is like the dictionaries we used in the dynamic analysis.

To define the widening operator, we define two operators $\min_{K} J$ and $\max_{K} J$ which, given a set of integers $J$ , pick the largest and smallest, respectively, $k \in K \cup {\infty, - \infty}$ st. $k \leq \min J$ and $k \geq \max J$ .

[i, j] \nabla [k, h] = [\min_{K} {i, k}, \max_{K} {j, h}]

We can see that we can only apply this operator a finite number of times until we either get $\infty$ or $- \infty$ .

Now when running our analysis, we use the $\nabla$ operator instead of the $⊔$ operator, and we can continue computing until we reach a fixed point.

The full abstraction is now:

K-Interval Abstraction

The interval abstraction ${𝐈 𝐭 𝐯 𝐚 𝐥}_{K}$ is a tuple of two numbers $i$ , $j$ , representing the interval of integers between $[i, j]$ , both inclusive, using a set of known boundaries $K$ .

\begin{matrix} α (S) & = [\min S, \max S] \\ γ ([i, j]) & = {n \in ℤ | j \geq n \leq i} \\ [i, j] ⊑_{{𝐈 𝐭 𝐯 𝐚 𝐥}_{K}} [k, h] & \equiv k \leq i \land j \leq h \\ [i, j] ⊔_{{𝐈 𝐭 𝐯 𝐚 𝐥}_{K}} [k, h] & \equiv [\min {i, k}, \max {j, h}] \\ [i, j] ⊓_{{𝐈 𝐭 𝐯 𝐚 𝐥}_{K}} [k, h] & \equiv [\max {i, k}, \min {j, h}] \\ ⊤_{{𝐈 𝐭 𝐯 𝐚 𝐥}_{K}} & = [- \infty, \infty] \\ ⊥_{{𝐈 𝐭 𝐯 𝐚 𝐥}_{K}} & = [\infty, - \infty] \\ [i, j] \nabla_{{𝐈 𝐭 𝐯 𝐚 𝐥}_{K}} [k, h] & = [\min_{K} {i, k}, \max_{K} {j, h}] \end{matrix}

Define a widening operator

Include a widening operator in your analysis, so that you only have to join a finite number of times.

Proving Widening §2.3.1

Proving that a widening operator is correct requires some carefulness. We have to prove two properties: One, that $\nabla$ increases in size;

\forall a, b \in A . a ⊑ (a \nabla b) \land b ⊑ (a \nabla b)

and two, that we can only apply the $\nabla$ operator a finite number of times before a fix point is reached.

\begin{matrix} \exists n \in ℕ . \forall x \in A^{n + 1}, a \in A . \\ (a_{0} \nabla a_{1}) \nabla a_{2}) \dots \nabla a_{n} & = ((a_{0} \nabla a_{1}) \nabla a_{2}) \dots \nabla a_{n + 1} \end{matrix}

The Worklist Algorithm §2.4

(Nielson (2020) at page 59)

Currently our algorithm is a little slow, as we essentially iterate in lockstep over the the entire program for every step.

This is, of course, silly, as we would much rather only handle unprocessed events. Consider you have a stepping function from program locations and an abstract state to a set of program locations and abstract states, which need to be joined at those points: $𝚜 𝚝 𝚎 𝚙 : 𝐏 𝐂 \times \hat{𝐒 𝐭 𝐚 𝐭 𝐞} \to 2^{𝐏 𝐂 \times \hat{𝐒 𝐭 𝐚 𝐭 𝐞}} .$

To extend our current implementation for this, we can modify the per_instruction method in StateSet to only emit:

def step(self) -> tuple[PC, set[str]]:
    # Pop from worklist
    pc = self.worklist.pop()
    for res in manystep(self.bc, pc, self.states[pc]):
        pc_, st = res
        before = self.states.get(pc_, st)
        after = before | st
        if pc_ not in self.states or after != before:
            self.states[pc_] = after
            # Update worklist
            self.worklist.append(pc_)
    # ...

This approach uses significantly fewer instructions than running all steps every time, and still produces the same results.

Control-Flow Analysis and Optimal Order §2.4.1

https://en.wikipedia.org/wiki/Tree_traversal
(Handouts about Control-flow analysis)
(Nielson (2020) at page 63)

However, there is still some work we can do to improve the algorithm. For example, when you analyze the following program:

void fn(int x) { 
  int i = 0;
  if (x == 0) { 
    i += 1;
  } else { 
    i -= 1:
  }
  // Many operations on i.
}

There are not reason to analyse the rest to the instructions before we have covered both sides of the if statement. The correct order to do this computation is in reverse post-order (Nielson (2020) at page 63). If you do this, you are guaranteed to process the branches of the if statements before looking into the instructions after.

The reverse post-order is not enough for fast analysis of full programs; in this case, you need to do more in-depth control-flow analysis. Consider the following program.

void fn() { 
  int i = 0;
  while (i < 100) { 
    i += 1;
  }
  // Many operations on i.
}

Calculating in post-order is no longer enough; instead, you have to find the strongly connected components of the graph, merge them into one node, and then compute those nodes in reverse post-order.

The control flow graph of the example code.

A strongly connected component in a directed graph is a subgraph where every node is reachable from every other node. For example, in the control-flow graph above, we can see that the loop is strongly connected. We should therefore ensure this is calculated before we continue our analysis.

Until next time!

Until next time, write the best analysis you can and upload the results to Autolab, and ponder the following:

What does it mean for two variables to be dependent?
What is the primary problem when doing unbounded static analysis?
Why do we need a widening operator?

Bibliography

Cousot, Patrick; Halbwachs, Nicolas (1978). Automatic discovery of linear restraints among variables of a program. doi:10.1145/512760.512770 link
Nielson, Flemming; Nielson, Hanne Riis (2020). Program Analysis (an Appetizer). link