[klee-dev] Improving KLEE coverage

[Cristian Cadar]

Hi Vlad,

It's difficult to say without seeing the full program, but it could be 
that KLEE is spending all its time in some other parts on the code.  You 
can use klee-stats to understand how many states are in memory, how much 
time is spent in constraint solving etc., and kcachegrind to visualize 
code-level statistics (see 
https://klee.github.io/tutorials/testing-coreutils/)

Best,
Cristian

On 23/07/2021 14:22, Vlad Ivanov wrote:
> 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
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>