Dynamic Analysis

Trace Selection §1.1

First, recall the definition of a transition system from Transition System and Traces (§2.4). A program can be described as a triplet $⟨{𝐒𝐭𝐚𝐭𝐞}_p,{\delta }_p,I_p⟩$, where ${\delta }_p$ is the transition function and $I_p$ is the set of initial states.

In the first phase, we select a trace from the transition system. This consists of choosing an initial state $\sigma \in I_p$, and then executing the program to pick a trace $\tau$:

If the program is deterministic, there is only one trace per input state. If the program is non-deterministic, like parallel programs, each initial state might give rise to multiple traces.

Selecting the initial state or even executing the program is not trivial in practice (see Running the Program (§2)).

Trace Analysis §1.2

Now that we have a trace, we can make several deductions about the behaviors of a program by analyzing it. Common analyses are (slightly abusing notation):

• did it end in a success? $$T{A}_{\mathtt{\text{𝚘𝚔}}}(\tau )\equiv {\tau }_{-1}=\mathtt{\text{𝚘𝚔}}$$

• did any opened $𝐎$ resource, not get closed $𝐂$? $$T{A}_{\mathtt{\text{𝚛𝚎𝚜}}}(\tau )\equiv \exists f,i.𝐎({\tau }_i,f)\wedge \forall j\ge i.\neg 𝐂({\tau }_j,f)$$

• did we execute this instruction? $$T{A}_{\mathtt{\text{𝚌𝚘𝚟𝚎𝚛}}(i)}(\tau )\equiv i\in \{e.\iota \mathrm{ | }e\in \tau \}$$

Any question that we can answer correctly for one trace can be turned into a not-must analysis for the full program (see 🗒 Trace Terminology). If we find a trace that ends in a failure, the program might fail. If we find a trace where an opened resource is not closed, we know that the program must not close all resources in the program. So, essentially, for any property $X$ we can find in one trace, we can build a not-must analysis which can detect it:

For example, if we find a trace which does not terminate in an $\mathtt{\text{𝚘𝚔}}$, we know that the program must not always succeed.

Actually, if we can increase the precision of the analysis by running the program multiple times. And, in the limit (assuming that we could run all traces) a dynamic analysis precisely captures any property.

Trace Abstraction and Prediction §1.3

The problem is, of course, that the number of traces in the semantics of most programs is infinite (or close), and it is impossible to cover them all without some trickery. Therefore, can we try to expand the number of traces we cover every time by inferring information about other traces from one trace? We call this Trace Prediction.

Trace prediction works by mapping each trace $\tau$ $ in the trace space into a possible finite set of trace classes $\left[\tau \right]$. If we can show that an analysis over a trace class is equivalent to a trace analysis over all traces in the trace class: ${𝐓𝐫𝐚𝐜𝐞}_X(\left[\tau \right])⟹\exists {\tau }^{\prime }\in \left[\tau \right].{𝐓𝐫𝐚𝐜𝐞}_X({\tau }^{\prime })$, we can save a lot of executions. And if we are also able to avoid a trace class in our next trace selection, we can potentially cover all traces of a program.

This step is especially useful when dealing with parallel programs. It can be very hard to run into deadlocks or data-races. With trace prediction, we can infer that there exist a datarace in the program even if we don't run into it (Kalhauge 2018).

int checkTheWrongThing(int a) { 
  if (a != 0) { 
    return a / 0;
  } else { 
    return 0;
  }
}

Why Should We Run the Program? §2.1

Running the program is often a good initial analysis we can do on most programs, and it has a lot of advantages:

• Most programming languages come with a built-in interpreter. Running the program can sometimes be easier than using syntactic analysis.

• The analysis can present you with a concrete trace that produces the error. This makes it very easy to debug the error.

• Since the goal of the dynamic analysis is to underestimate the set of valid traces, if it warns us about a problem, then the problem is real.

Why Shouldn't We Run the Program? §2.2

It might seem obvious that we can learn things about the program by running it; however, running the program is not always as easy as we would like.

• Setting up the correct environment of a program can be hard to downright impossible without running it in production.

• Warning that something can happen by doing it can be problematic if the program has side-effects like deleting the database or firing the missiles.

• Running the program will never tell you if something can't happen, like the program running forever.

Characterization Trace Testing §3.1

In many cases, it is too complicated (or the assessment of correctness is subjective) to actually check that the output of a test is correct. Instead, we can save the output to a file, or trace the steps taken to produce the output. After we have checked that the trace or output is correct, we can store it in a code repository. We call that a snapshot or (golden master). Every time we re-run the test, if the file did not change, we know the output or trace has remained the same.

This technique is prefect at catching regressions.

Assertions §3.2

One specifically useful tool for improving the usefulness of testing is to use assertions to trace that the behavior of the system is correct. The cool idea here is that, by using assertions, we can catch programmer errors early, and closer to the bug, instead of as part of a complicated crash.

public static int square(int height, int width) {
  assert height > 0; 
  assert width > 0;
  return height * width;
}

case Get(field=field):
  assert field.fieldid.name == "assertionsDisabled"
  frame.stack.push(StackInt(0)) # Push False

Inserting these assertions by hand can be a lot of work, and a good dynamic analysis can insert some of them automatically. Since Java is a memory safe language, most out-of-bounds memory accesses are caught by the language at runtime. You can think of this as automatically inserting assertions.

For other languages like C, there exist tools to extend capabilities of testing by adding memory checks at runtime. These are called sanitizers.

Random Inputs §4.1

The easiest way to get started with fuzzing is to simply choose an input at random at the start of the program and then see if it can make the program fail.

This works because most traces of a program can be approximated using relatively few inputs. The hypothesis is that the input space relatively corresponds to the path-equivalent space, and this is correct for examples like this:

void split(int i) { 
  if (i > 0) { 
    ...
  } else {
    ...
  }
}

In this world, we can clearly see there are two path-equivalence classes: those where $i>0$ and $i\le 0$. In this case, choosing $i$ randomly gives an equal chance of hitting either branch.

Dictionaries §4.2

The problem is, of course, that not all branches are like that; some check for specific values.

void isEqualToZero(int i) { 
  if (i == 0) { 
    ...
  } else {
    ...
  }
}

In this case, we can use a trick called dictionaries. First, we use a syntactic analysis to scan the code for constants such as 1 and "test". Then we add those constants to a dictionary, which we can sample from when we choose random values.

ints_in_class = syntactically_all_ints_in_class(methodid.classname)

...

for p in methodid.extension.params:
    match p:
        case jvm.Int():
          if rand.choice([True, False]):
            input.append(jpamb.case.Int(rand.choice(ints_in_class)))
          else:
            input.append(jpamb.case.Int(rand.randint(-(1 << 31), 1 << 31)))

Coverage-Guided Fuzzing §4.3

The problem with the above-mentioned approaches is that they are not good at directing the execution down specific paths of the program. Consider the arraySpellsHello test case:

@Case("([C: 'h','e','l','l','o']) -> ok")
@Case("([C: 'x']) -> assertion error")
@Case("([C: ]) -> out of bounds")
@Tag({ ARRAY })
public static void arraySpellsHello(char[] array) {
  assert array[0] == 'h'
      && array[1] == 'e'
      && array[2] == 'l'
      && array[3] == 'l'
      && array[4] == 'o';
}

Using random testing or the dictionary approach alone, we would have a hard time finding hello by chance. A cool approach to get around this, and which is used in real-world applications, is Coverage-Guided Fuzzing (Fioraldi 2020).

This approach manipulates a list of byte-strings called test cases. The user of the fuzzer is expected to provide a function that can parse those byte-strings into input of the program. Now the fun begins.

We start with the empty byte-string as input and then find its coverage (the bytecode offsets it executes). We add that byte-string to a list called interesting.

Now, while we have interesting test-cases:

• We pick a test-case, and manipulate it, by either changing a byte, removing a byte or appending a byte.

• Then we run it, and see if it add coverage compared to the previous cases.

• If it does add it to the interesting cases, otherwise ignore it.

• Repeat.

class Corpus:
  parameters: jpamb.Parameters
  interesting: list[bytes]
  coverage: set[PC]
 
  def fuzz_input(self, code: bytes) -> Input:
      """Using an sequence of bytes, create a new input which matches 
      the parameters"""

  def next(self) -> Input:
      """Randomly pick an intersting case, and mutate by making changes to the bytes"""

  def add(self, input: Input, coverage: set[PC]):
      """Add the input to the interesting cases if increases coverage"""

Property Based Testing §4.4

When using random inputs to generate inputs to tests, we also have to change the way we test. Instead of testing for equalities, we now have to test for properties. This approach is called property-based testing.

In Python, there is a very nice library called Hypothesis, which helps you do just that. In the following example from the website, they test that their sorting algorithm my_sort is equivalent to the built-in sort on all lists of integers and floats:

from hypothesis import given, strategies as st

@given(st.lists(st.integers() | st.floats()))
def test_sort_correct(lst):
    # lst is a random list of numbers
    assert my_sort(lst) == sorted(lst)

test_sort_correct()

Take a look at the extra-fuzzer commit to get feel for how to use hypothesis to test the creation of a fuzzer.

The Small-Scope Hypothesis §4.5

As an alternative to the fuzzing technique, we have the small-scope hypothesis:

Model-checkers like Alloy (Jackson 2006) and testing frameworks like SmallCheck (Runciman 2008) use this idea by only investigating small test-cases. Instead of testing random numbers, you test only a few small inputs. The good thing about this approach is that

• It is deterministic and always test the same inputs, as you can cover all small values to a depth $d$;

• If a buggy input is found, it is the smallest input that can create that error.

This technique excel at small cases, like checking of empty lists or stuff like that:

void isEqualToZero(int i) { 
  if (i == 0) { 
    ...
  } else {
    ...
  }
}

However, the technique does have clear disadvantages: what if the error hides behind a big input?

void isEqualToAMillion(int i) { 
  if (i == 1000000) { 
    ...
  } else {
    ...
  }
}

In the following activity, you can seek inspiration from the SmallCheck paper Runciman (2008).

def gen_int(depth): 
  yield 0
  for i in range(depth):
    yield (i + 1)
    yield -(i + 1)

$ jpamb -vv analyse --report report.sexp dynamic-analysis