[klee-dev] Improving KLEE coverage

[Vlad Ivanov]

Hello KLEE developers, 
 
first of all thank you for working on this tool and making it available to the
public. I'm working on using KLEE to fuzz a simple RPC protocol. The setup is as 
follows:
 
1. Create a symbolic variable buffer_size and use klee_assume on it to create
   a constraint of maximum size
2. Allocate a buffer of length buffer_size and make it symbolic as well
3. Take some data from random buffer and use it to create RPC request
4. Pass the request to the RPC endpoint input function
 
I've created a setup to collect coverage data after KLEE is done fuzzing and put
it into a HTML report. I can see that within several minutes, several paths are
discovered but for some reason, even when running for hours, KLEE doesn't seem
to be able to get past certain conditions in code.
 
To illustrate, here's a code example (numbers on the left represent hit count):
 
    163    auto const cSize = mapSize(inputBuffer[4]);
    163 
    163    if (inputBuffer[5] != cSize)
    163    {
    163        return ArgumentError;
    163    }
    0   
    0      if (inputBuffer[6] != cSize)
    0      {
    0          return ArgumentError;
    0      }
 
While I can't share the exact program this is the type of checks that's 
ultimately happening there. What I find interesting is that in order to reach 
this point, a rather complex set of conditions has to be satisfied: basically,
7 or so positions in the input buffer need to match a specific set of constants.
These constants are discovered rather quickly, and it would seem to me that
there should be no trouble in finding the 8th one, but that's not what I'm
seeing, and after many hours of fuzzing I'm stuck with the same number of test
cases I had when I ran fuzzing just for a few minutes.
 
The command line I'm using to start fuzzing is rather simple:
 
    klee --optimize --libcxx --libc=uclibc --posix-runtime ./build/application
 
And here's a --version output:
 
    KLEE 2.2 ()
      Build mode: RelWithDebInfo (Asserts: ON)
      Build revision: 5719d2803e93252e5d4613f43afc7db0d72332f1
    
    LLVM ():
      LLVM version 11.0.0
      Optimized build.
      Default target: x86_64-unknown-linux-gnu
      Host CPU: skylake
 
KLEE is built with Z3 support.
 
What would be a good way to understand why it's not progressing further? 
Perhaps there is some sort of option to try?

(apologies for the previous non-plaintext email)
 
Best Regards,
 
Vlad