[llvm-dev] Seeking suggestions about interfacing of LLVM DataFlowSanitizer library with KLEE in C code.

Mon Jul 8 09:22:17 PDT 2019

Hi Monir,

I'm not entirely familiar with KLEE nor with the dataflow sanitizer, but I
think there are two issues with your approach.

First, I would expect KLEE to require for the whole program to be provided
together with its bitcode (modulo known library functions) -- you can see
how they achieve that in the tutorials section on their website (e.g., for
coreutils [1]). From the high-level point of view, KLEE uses a technique
called dynamic symbolic execution (DSE) that when interpreting LLVM bitcode
maintains symbolic execution state alongside the (usual) concrete state
[2], and while it's possible to use it on binaries, KLEE works on the level
of LLVM IR. They have a custom libc implementation that KLEE can reason
about (the files with .bca extension on your screenshot). I think that
unless you link in whatever binaries you use (such that you end up with a
single bitcode file), use on of the provided libraries like libc, KLEE
won't be able to come up with a symbolic state for library code.

The second issue I see is that you want to use the dataflow sanitizer
together with KLEE. Typically, the mainstream sanitizers provide cleaver
encoding that makes checking some property of interest fast for runtime
execution. For example, a sanitizer can maintain a mapping from normal
program memory to shadow memory, and instrumentation that maintains this
mapping and asserts some invariants over both the memory regions. This
encoding/mapping use fast (runtime) operations like shifts, bit operations,
hashing, that can be very difficult to reason about for an underlying
constraint solver in a DSE tool. Software verification tools usually use
custom encodings/instrumentation that is easier to reason about and can use
tricks that don't work for runtime verification (e.g., use of
nondeterminism in [3]). Things you want to avoid are complicated math
function (hashing), large arrays and dependencies across them, etc.

My suggestion would be to try to first manually instrument your C/C++
source with an encoding friendly for DSE, and once you are happy with it
create a custom transformation pass over LLVM IR that emits the
instrumentation.

Best,
Jakub

[1] http://klee.github.io/tutorials/testing-coreutils/
[2] https://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf
[3]
http://seahorn.github.io/seahorn/memory%20safety/2017/05/27/seahorn-memory-safety.html

On Fri, Jul 5, 2019 at 9:32 PM Hossain,Muhammad Monir via llvm-dev <
llvm-dev at lists.llvm.org> wrote:

> Dear Developers,
>
> I am a Master's student at the ECE department of the University of
> Florida, USA. For my research project, supervised by Prof. Mark
> Tehranipoor <http://tehranipoor.ece.ufl.edu/> and Prof. Farimah Farahmandi
> <http://farimah.ece.ufl.edu/>,  I need to use Clang LLVM
> DataflowSanitizer library in KLEE. However, I have faced some difficulties
> (explained below) while interfacing this library with KLEE and I am seeking
> your help to solve it.
>
> For our research purpose, we are using LLVM compiler and LLVM
> DataFlowSanitizer library. We instrumented a C code using LLVM
> DataFlowSanitizer library (from *dfsan_interface.h*) along with the
> insertion of some KLEE assertion (from *klee.h*) and converted it to LLVM
> Bit-code. Then we provided this LLVM Bit-code to KLEE (software
> verification tool) to run with the archive library of DataFlowSanitizer
> tool, *libclang_rt.dfsan-x86_64.a*. But, KLEE showed the following error.
>
>
>
> However, to figure out the problem, I have built a sample custom archive
> library from the object files generated by Clang/LLVM (using cmd *llvm-ar*)
> and used this library in a C code along with KLEE. In this case, KLEE gave
> the same error as above. Then I generated the same sample custom archive
> library from the LLVM bit-code files and this time KLEE executed
> successfully. Hence, I am afraid whether KLEE requires the bit-code version
> of *libclang_rt.dfsan-x86_64.a* or there is any other solution.
>
> In this circumstance, it would be great if you could direct me to resolve
> this issue. Please let me know if you need any other information.
>
>
> Thank you,
> Monir
>
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
>

-- 
Jakub Kuderski
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20190708/b219539a/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Outlook-2540iq24.png
Type: image/png
Size: 50984 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20190708/b219539a/attachment.png>