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

Wed Jul 10 14:18:56 PDT 2019

Dear Jakub,

Thank you very much for your detail explanations and valuable suggestions. I will follow your suggestions.

I completely agree with you that KLEE requires libraries with the .bca extension. In fact, I have already tried to generate the archived bit-code version of libclang_rt.dfsan-x86_64.a using WLLVM tool. But it could not generate the .bca file successfully (please, see the attached screenshot).

Would you please let me know how I can get the archived bit-code version of the LLVM DataFlowSanitizer library? Is there any repository that I may not be aware of? If there is none, could you please guide me on how I can generate it? I really appreciate any suggestion you may have. Thank you very much.

Sincerely,
-Monir
________________________________
From: Jakub (Kuba) Kuderski <kubakuderski at gmail.com>
Sent: Monday, July 8, 2019 12:22 PM
To: Hossain,Muhammad Monir
Cc: via llvm-dev; Rahman,Fahim; Tehranipoor, Mark; Farahmandi,Farimah
Subject: Re: [llvm-dev] Seeking suggestions about interfacing of LLVM DataFlowSanitizer library with KLEE in C code.

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/<https://urldefense.proofpoint.com/v2/url?u=http-3A__klee.github.io_tutorials_testing-2Dcoreutils_&d=DwMFaQ&c=sJ6xIWYx-zLMB3EPkvcnVg&r=lDSmMGOiBAYgoioljve3DA&m=YCp0CzVKUdPTT1gYkqtYENRpDDmo-MoJUGhg9EfiY7Y&s=N7mBNCWumzZlQ2m9gF4uiAeH9ueQYRqBFRFR18VN-gU&e=>
[2] https://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf<https://urldefense.proofpoint.com/v2/url?u=https-3A__www.doc.ic.ac.uk_-7Ecristic_papers_klee-2Dosdi-2D08.pdf&d=DwMFaQ&c=sJ6xIWYx-zLMB3EPkvcnVg&r=lDSmMGOiBAYgoioljve3DA&m=YCp0CzVKUdPTT1gYkqtYENRpDDmo-MoJUGhg9EfiY7Y&s=22fD7F1PzwNQrvP15qZYJ-jSgwuzpH33BUShYRMDzyo&e=>
[3] http://seahorn.github.io/seahorn/memory%20safety/2017/05/27/seahorn-memory-safety.html<https://urldefense.proofpoint.com/v2/url?u=http-3A__seahorn.github.io_seahorn_memory-2520safety_2017_05_27_seahorn-2Dmemory-2Dsafety.html&d=DwMFaQ&c=sJ6xIWYx-zLMB3EPkvcnVg&r=lDSmMGOiBAYgoioljve3DA&m=YCp0CzVKUdPTT1gYkqtYENRpDDmo-MoJUGhg9EfiY7Y&s=vXBYnki_GXpMg2m3AjXhkSYWpqp0qbWQjlssKmtqz-k&e=>

On Fri, Jul 5, 2019 at 9:32 PM Hossain,Muhammad Monir via llvm-dev <llvm-dev at lists.llvm.org<mailto: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.

[cid:16bd2465d09b9bdfba41]

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<mailto:llvm-dev at lists.llvm.org>
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev<https://urldefense.proofpoint.com/v2/url?u=https-3A__lists.llvm.org_cgi-2Dbin_mailman_listinfo_llvm-2Ddev&d=DwMFaQ&c=sJ6xIWYx-zLMB3EPkvcnVg&r=lDSmMGOiBAYgoioljve3DA&m=YCp0CzVKUdPTT1gYkqtYENRpDDmo-MoJUGhg9EfiY7Y&s=d5Palxb4z0zzQotZmk3mG7dVPeZUtiEDCvBg_iEpBVE&e=>

--
Jakub Kuderski
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20190710/76eb20e7/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Outlook-2540iq24.png
Type: image/png
Size: 50984 bytes
Desc: Outlook-2540iq24.png
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20190710/76eb20e7/attachment-0002.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: wllvm.png
Type: image/png
Size: 407482 bytes
Desc: wllvm.png
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20190710/76eb20e7/attachment-0003.png>