Finding Bugs

ex2.c shows a program that contains an error. It is equivalent to tossing a coin 5 times and checking whether heads appears at least once. In on average 1 of 32 tries however, this is not the case.

extern int __VERIFIER_nondet_uint(); extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } int main() { int n = 0; for (int i = 0; i<5; i++) { if (__VERIFIER_nondet_uint() % 2 == 0) { n = 1; break; }; } __VERIFIER_assert(n == 1); return 0; }

The special functions declared before the main function follow a convention that is used in the Competition on Software Verification and as such understood by many different software verifiers. The function __VERIFIER_nondet_uint returns a nondeterministic unsigned integer. The function __VERIFIER_error signals to the verifier that an error /specification violation has occurred.

With CPAchecker

We now try to find the error in ex2.c with CPAchecker using three different analysis.

Try with value analysis:

scripts/cpa.sh -valueAnalysis-NoCegar examples/ex2.c

In the report named Report.html we can see that the bug is found, but the ARG shows a lot of branching.

Try with predicate analysis:

scripts/cpa.sh -predicateAnalysis examples/ex2.c

In the report named Counterexample.1.html we can observe that the bug is found, and the ARG shows less branching. We also can distinguish between abstration states(blue), non-abstraction states(no background color), states that were not expanded (orange) and error states (red). There is also a additional bar at the left that lets us step through the counterexample and look at the values of each variable at each step (this explains the different name of the report file, when multiple counterexamples are found, more than one Counterexample.X.html file might be generated).

Try with symbolic execution:

scripts/cpa.sh -symbolicExecution examples/ex2.c

In the report named Result.html we can now observe that the ARG contains states with symbolic values.

With Klee

We need to modify the example file in order for it to work with KLEE. See ex2_klee.c:

#include <klee/klee.h> extern unsigned int __VERIFIER_nondet_uint(); extern void __VERIFIER_error(); void __VERIFIER_error() { klee_assert(0); } unsigned int __VERIFIER_nondet_uint(){ unsigned int __sym___VERIFIER_nondet_uint; klee_make_symbolic(&__sym___VERIFIER_nondet_uint, sizeof(__sym___VERIFIER_nondet_uint), "__sym___VERIFIER_nondet_uint"); return __sym___VERIFIER_nondet_uint; } void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } int main() { int n = 0; for (int i = 0; i<10; i++) { if (__VERIFIER_nondet_uint() % 2 == 0) { n = 1; break; }; } __VERIFIER_assert(n == 1); return 0; }

The main changes are that we define __VERIFIER_nondet_uint __VERIFIER_error in a way KLEE understands. klee_assert(0) will tell KLEE to log if this assertion is reached

We start klee as docker container and mount the current working directory to /home/klee/dir inside the container:

$ docker run --rm -ti --ulimit='stack=-1:-1' -v $(pwd):/home/klee/dir klee/klee
klee@7435ce6644ce:~$ cd dir
klee@7435ce6644ce:~/dir$ ls
ex2_klee.c

(If you got the KLEE binaries installed otherwise (e.g. via TBF), just move into the directory where the example files are) Now the program needs to be compiled before we can use KLEE:

klee@7435ce6644ce:~/dir$ clang -I ~/klee_src/include -emit-llvm -c -g ex2_klee.c

This creates a file ex2_klee.bc that can then be given as input program to KLEE:

klee@7435ce6644ce:~/dir$ klee ex2_klee.bc 
KLEE: output directory is "/home/klee/dir/klee-out-14"
KLEE: Using STP solver backend
KLEE: ERROR: /home/klee/dir/ex2_klee.c:5: ASSERTION FAIL: 0
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 191
KLEE: done: completed paths = 6
KLEE: done: generated tests = 6

Result:

  • KLEE found (all) six paths through the program and generated test cases, which are in the output folder klee-out-xx.
  • The output also indicates that it found an ERROR. This means that there is a test case that triggered the klee_assert(0).

  • It is also described in a file with the extension .assert.err in the klee-out-xx folder. The corresponding .ktest files can be viewed with ktest-tool:

      ktest-tool --write-ints klee-out-xx/test000yyy.ktest

Variations

if the number of iterations is increased in ex2.c/ex2_klee.c, e.g. to 50, predicate analysis takes longer while KLEE still returns almost instantly. This changes if the break instruction is removed => KLEE will not terminate in reasonable time (at least not with the default search strategy) while predicate analysis takes longer, but finishes eventually. The symbolicExecution in CPAchecker behaves similar to KLEE, as far as i can tell.

Another Example

A program that takes a nondeterministic, positive integer and calculates the length of the corresponding collatz sequence. The program assumes that this length is always smaller than a certain boundary (here 6 is chosen). This is of course wrong, so the program has a bug. It is interesting to see if and how CPAchecker/KLEE find this. Here is the source code of ex3.c:

extern unsigned int __VERIFIER_nondet_uint(); extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } int main() { unsigned int n = __VERIFIER_nondet_uint(); int i = 0; while (n>1) { if (n%2==0) { n = n/2; } else { n = 3*n + 1; } i++; } __VERIFIER_assert(i < 6); return 0; }

And the modified source code for KLEE is ex3_klee.c:

#include <klee/klee.h> extern unsigned int __VERIFIER_nondet_uint(); extern void __VERIFIER_error(); void __VERIFIER_error() { klee_assert(0); } unsigned int __VERIFIER_nondet_uint(){ unsigned int __sym___VERIFIER_nondet_uint; klee_make_symbolic(&__sym___VERIFIER_nondet_uint, sizeof(__sym___VERIFIER_nondet_uint), "__sym___VERIFIER_nondet_uint"); return __sym___VERIFIER_nondet_uint; } void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } int main() { unsigned int n = __VERIFIER_nondet_uint(); int i = 0; while (n>1) { if (n%2==0) { n = n/2; } else { n = 3*n + 1; } i++; } __VERIFIER_assert(i < 6); return 0; }

Check program with CPAchecker:

scripts/cpa.sh -predicateAnalysis examples/ex3.c
# ... usual output, CPAchecker finds the bug

Check program with KLEE:

klee@7435ce6644ce:~/dir$ clang -I ~/klee_src/include -emit-llvm -c -g ex3_klee.c
klee@7435ce6644ce:~/dir$ klee ex3_klee.c
KLEE: output directory is "/home/klee/dir/klee-out-6"
KLEE: Using STP solver backend
KLEE: ERROR: /home/klee/dir/ex3_klee.c:5: ASSERTION FAIL: 0
KLEE: NOTE: now ignoring this error at this location
^CKLEE: ctrl-c detected, requesting interpreter to halt.
KLEE: ctrl-c detected, requesting interpreter to halt.
KLEE: halting execution, dumping remaining states

KLEE: done: total instructions = 9188
KLEE: done: completed paths = 210
KLEE: done: generated tests = 195

With KLEE, we need to abort the analysis after the ERROR is discovered, otherwise KLEE will run indefinitely. Alternatively we can call KLEE with an extra option:

klee --exit-on-error ex3_klee.c

There is also an option only-output-states-covering-new that reduces the amount of generated test cases. This will only output a new testcase if it covers new code:

klee only-output-states-covering-new ex3_klee.c

Result:

  • CPAchecker (predicate analysis) finds the bug. In the report, we can see that n=64 is chosen as the initial value of n
  • KLEE also finds the bug. By inspection of the test case, we see that n=10 is chosen as initial value.

Variations

Changing the length from 6 to 15:

  • KLEE takes very long to find the bug, while CPAchecker(predicate analysis) is faster.

  • This is only half the truth. KLEE can find it faster with different search strategies, e.g.:

      klee -search=dfs ex3_klee.bc
  • CPAchecker with symbolicExecution does not terminate here. Maybe another search strategy would change this?

results matching ""

    No results matching ""