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⟩$, were ${\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 transitions system. This consists of choosing an initial state $\sigma \in I_p$, and then executing the program to picking a trace $\tau$:

If the program is deterministic, there is only one trace per input state. If the program is non-deterministic, like for example with 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 behaviours of the program by analysing the trace. Common analyses are (slightly abusing notation):

• did it end in a failure? $${𝐓𝐫𝐚𝐜𝐞}_{\mathtt{\text{𝚎𝚛𝚛}}}(\tau )\equiv {\tau }_{-1}=\mathrm{\text{err}}(\mathtt{\text{‘...’}})$$

• did any opened resource, not get closed? $${𝐓𝐫𝐚𝐜𝐞}_{\mathtt{\text{𝚛𝚎𝚜}}}(\tau )\equiv \exists fi.𝐎({\tau }_i,f)\wedge \forall j.\neg 𝐂({\tau }_j,f)\vee j<i$$

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

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

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 are infinite (or close), and it is impossible to cover them all without some trickery. Therefore, should 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$ from the trace space into a possible finite set of trace classes $\left[\tau \right]$. If we can show that an analysis over the 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 any 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 comes with built-in interpreter. Running the program can sometimes be easier than using a syntactic analysis.

• The analysis can present you with a concrete trace that produce 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 downward 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 subject) to actually check that output of a test is correct. Instead, we can save output the to a file, or trace the events taken to produce the output. After we have checked that the trace or output is correct, we can store it in code repository. We call that the snapshot or (golden master). Every time we then re-run the test, then if the file did not change, we know the output or trace has remained the same.

This technique is prefect at catching regressions.

$ uv run jpamb interpret -r out.expected <your_interpreter>

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 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(Value.int(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 see 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 correspond 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 equivalent classes, those with $i>0$ and $i\le 0$. In this case choosing $i$ randomly give equal chance to hit either branch.

Dictionaries §4.2

The problem is of course, that not all branches are like that, some are checking 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 like e.g. 1 and "test". Then we add those constants to a dictionary, which we can sample from when we choose random values.

Coverage-Guided Fuzzing §4.3

The problem with the above mentioned approaches are 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 the 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 application is Coverage-Guided Fuzzing (Fioraldi 2020).

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

We start with the empty byte-string as input, then we find its coverage (the bytecode offsets it executes). We add that byte-string to a list we call 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.

Property Based Testing §4.4

When using random inputs to generate inputs to tests, we also have to change the way we tests. 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 builtin sort on all that 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()

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 instead test only a few small inputs. The good thing about this approach is that

• you can be deterministic and always test the same inputs, because you can cover all small values to a depth $d$.

• The second advantage is that 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)