Andrew Bedford

Identifying likely program invariants using dynamic analysis ​

Regardless of the static analysis tool they use, users often complain about one thing: false positives. False positives occur when tools report issues that, well, aren't really issues. For example, reporting that there might be a null pointer dereference when we know that the pointer in question can never actually be null. The reality of it is, static analyzers checking for non-trivial properties are always going to have false positives because it is essentially an undecidable problem. In addition to this, static analyzers often have to sacrifice accuracy for speed in order to avoid path explosions.

If you got this far, you might be wondering why I'm talking about static analysis and false positives when the title of this article is about invariants and dynamic analysis. Well, this is because one way to improve a static analyzer's accuracy and reduce its number of false positives is to use information gathered at runtime (i.e., dynamic analysis)[1].

Filtering Mechanism: Likely invariants can act as a filtering mechanism to distinguish between true positives and false positives. If a detected issue contradicts a known invariant, it is more likely to be a false positive, but not necessarily.

Good static analyzers are, among other things, path sensitive. That is, they make sure that the path is feasible before reporting a defect. This is typically done using

c
void foo(int x) {
  int *p = nullptr;
  if (x > 32) {
    *p = 1; // Null pointer dereference when x > 32
  }
}

void bar() {
  foo(1);
}

What is Daikon? ​

Daikon is a dynamic analysis tool, built on valgrind, that captures and observes values used during a program's execution. It then reports properties that were true over all of those executions (i.e., likely invariants). Note that since it is based on valgrind, it shares some of its limitations, such as working only on Unix systems.

How to build it? ​

sh
git clone https://github.com/codespecs/daikon.git
git clone https://github.com/codespecs/fjalar.git

sudo apt install binutils-dev zlib1g-dev opendjk-8-jdk

cd $DAIKONDIR
make compile
make compile-java
make kvasir

If successful, it will output a daikon.jar file in $DAIKONDIR and kvasir-dtrace in $DAIKONDIR/scripts.

How to use it? ​

To analyze a C/C++ program, Daikon requires it to be compiled with the following options:

-g -no-pie -fdebug-default-version=3

To illustrate its use, let's consider the following program:

c
int foo(int param) { return param * 2; }
int bar(float param2) { return param2 * 10.0; }

int main(int argc, char *argv[]) {
    int x = 1;
    float y = 2.5;
    for (int i = 0; i < argc; i++) {
        if (atoi(argv[i]) == 42) {
            x = 42;
            printf("%d was passed as argument!\n", x);
        }
    }
    foo(x);
    foo(x+1);
    bar((float)(x));
    return 0;
}

Note that the values returned by foo and bar depends on the value of x, which can be 1 or 42 depending on the program's arguments.

Capturing traces ​

To analyze it, we must first capture some traces:

bash
export DAIKONDIR=~/Projects/daikon
$DAIKONDIR/kvasir-dtrace ~/Projects/hello/a.out 123
$DAIKONDIR/kvasir-dtrace --dtrace-append ~/Projects/hello/a.out 42

This

Kvasir will dynamically capture variable values when entering and exiting functions.

It also possible to specify which functions we want to analyze, and static/global variables can be ignored to boost performance (see options).

Output ​

The trace files that Kvasir produced can then be passed to Daikon, which will use them to analyze and summarize the ranges of function inputs (i.e., parameter values) and outputs (i.e., returned values).

Daikon version 5.8.19, released June 24, 2023; http://plse.cs.washington.edu/daikon.
(read 1 decls file)                                                            
Processing trace data; reading 1 dtrace file:                                  
[2024-02-17T23:33:12.475217]: Finished reading daikon-output/a.out.dtrace      
===========================================================================    
..bar(float):::ENTER
param2 one of { 1.0, 42.0 }
===========================================================================
..bar(float):::EXIT
return one of { 10, 420 }
===========================================================================
..foo(int):::ENTER
===========================================================================
..foo(int):::EXIT
===========================================================================
..main():::ENTER
argc == 2
argv has only one value
argv[] == [/home/abedford/Projects/hello/a.out]
argv[] elements == "/home/abedford/Projects/hello/a.out"
===========================================================================
..main():::EXIT
argv[] == [/home/abedford/Projects/hello/a.out]
argv[] elements == "/home/abedford/Projects/hello/a.out"
return == 0
Exiting Daikon.

  1. Enforcing Information-Flow Policies by Combining Static and Dynamic Analyses.  ↩︎

Andrew Bedford