Is this how to test a stateful API with klee symbolic execution?

Question

I'm currently testing out a few approaches on how to test and fuzz a C API. In the process thereof I found KLEE which runs the code symbolically, meaning that it tries to cover all branches that depend on some symbolic input and checks for all sorts of errors. I managed to get it to work and am now asking if my approach is good or if it has some major drawbacks or problems.

Let's suppose we have following simple but buggy API:

#include <assert.h>

static int g_state;

void setState(int state) {
    g_state = state;
}

void run(void) {
    if (g_state == 123) {
        assert(0);
    }
}

If the state is set to 123 and then run() is invoked the placed assertion fails.

For this I have written following symbolic test with KLEE:

#include "klee/klee.h"
#include "buggy_api.h"

int main(void) {
    for (int i = 0; i < 2; ++i) { // sequentially call 2 APIs
        int f_select = klee_choose(2); // what API to call
        if (f_select == 0) {
            int state = 0;
            klee_make_symbolic(&state, sizeof(state), "state");
            setState(state);
        } else if (f_select == 1) {
            run();
        }
    }
    return 0;
}

When running with KLEE, the sequence of calls necessary to trigger the assertion is found almost immediately. I then tried to extend the API with a few other functions and hid the assertion behind a combination of states. KLEE again found the planted bug but naturally took a bit longer.

Is this how I can efficiently use KLEE for checking an API? Or is there documentation about a better approach?

Answer 1

In order to test an API with KLEE, you indeed need to write a driver that calls it. Yours works well, I'm not sure why you're using a for loop though? This smaller example should work:

#include "klee/klee.h"
#include "buggy_api.h"

int main(void) {
    int state;
    klee_make_symbolic(&state, sizeof(state), "state");
    setState(state);
    run();
    return 0;
}