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

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:99d3b241-aa41-425f-94fb-1395932c5c00]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20190706/a3a13643/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/20190706/a3a13643/attachment-0001.png>

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>

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>