Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

KLEE LLVM Execution Engine

klee.github.io

Post reply on HN
Print view View original

1–10 of 22 posts

Re: KLEE LLVM Execution Engine

#3

Post by TheNewAndy »

mslate wrote: post #2

Anyone using this in practice?

I use it - I am writing a subset-of-yaml parser, and I've littered the code with a bunch of abort()/assert() statements for things I don't think should be possible. Running klee over my code spits out ~100K test cases (I let it use any 10 byte YAML input), and so while I don't inspect the output of any of the cases - I do make sure that none of them crash.

Similarly, if I make a change which I don't expect to change the output of the parser, then I can use this test suite to be quite sure that my change hasn't changed behaviour.

One thing I am unclear about is what it means for klee to be "done" on my binary. When it has generated all the test cases, if none of them crash my binary, then does that mean it is impossible to crash my binary in 10 bytes of input?

Re: KLEE LLVM Execution Engine

#5

Post by xnum »

TheNewAndy wrote: post #3
mslate wrote: post #2

Anyone using this in practice?

I use it - I am writing a subset-of-yaml parser, and I've littered the code with a bunch of abort()/assert() statements for things I don't think should be possible. Running klee over my code spits out ~100K test cases (I let it use any 10 byte YAML input), and so while I don't inspect the output of any of the cases - I do make sure that none of them crash. Similarly, if I make a change which I don't expect to change…

if your program calls system call or random function which KLEE couldn't handle, some parts of code may not be tested. KLEE uses its special libc (uclibc) to deal with that cases in glibc. To solve this problem perfectly, we usually uses S2E instead of KLEE in large and complex softwares (http://s2e.systems/)

Re: KLEE LLVM Execution Engine

#6

Post by wyldfire »

TheNewAndy wrote: post #3
mslate wrote: post #2

Anyone using this in practice?

I use it - I am writing a subset-of-yaml parser, and I've littered the code with a bunch of abort()/assert() statements for things I don't think should be possible. Running klee over my code spits out ~100K test cases (I let it use any 10 byte YAML input), and so while I don't inspect the output of any of the cases - I do make sure that none of them crash. Similarly, if I make a change which I don't expect to change…

Can you share more details about this? Is the work already public?

Re: KLEE LLVM Execution Engine

#7

Post by modeless »

senatorobama wrote: post #4

What is CS 101 explanation for this project?

I found a blog post with a succinct explanation.

> KLEE [runs] a program considering its input(or some other variables) to be symbols instead of concrete values like 100 or “cacho”. In very few words, a symbolic execution runs through the code propagating symbols and conditions; forking execution at symbol dependant branches and asking the companion SMT solver for path feasibility or counter-examples.

https://feliam.wordpress.com/2010/10/07/the-symbolic-maze/

Re: KLEE LLVM Execution Engine

#8

Post by TheNewAndy »

xnum wrote: post #5
TheNewAndy wrote: post #3

Earlier quoted context omitted.

I use it - I am writing a subset-of-yaml parser, and I've littered the code with a bunch of abort()/assert() statements for things I don't think should be possible. Running klee over my code spits out ~100K test cases (I let it use any 10 byte YAML input), and so while I don't inspect the output of any of the cases - I do make sure that none of them crash. Similarly, if I make a change which I don't expect to change…

if your program calls system call or random function which KLEE couldn't handle, some parts of code may not be tested. KLEE uses its special libc (uclibc) to deal with that cases in glibc. To solve this problem perfectly, we usually uses S2E instead of KLEE in large and complex softwares ( http://s2e.systems/ )

Right - but being a parser, I don't have those problems. My problem domain is quite well specified and there isn't any place for random numbers of system calls.

Re: KLEE LLVM Execution Engine

#9

Post by TheNewAndy »

wyldfire wrote: post #6
TheNewAndy wrote: post #3

Earlier quoted context omitted.

I use it - I am writing a subset-of-yaml parser, and I've littered the code with a bunch of abort()/assert() statements for things I don't think should be possible. Running klee over my code spits out ~100K test cases (I let it use any 10 byte YAML input), and so while I don't inspect the output of any of the cases - I do make sure that none of them crash. Similarly, if I make a change which I don't expect to change…

Can you share more details about this? Is the work already public?

The work won't be public. What details are you interested in?

Re: KLEE LLVM Execution Engine

#10

Post by withzombies »

TheNewAndy wrote: post #3
mslate wrote: post #2

Anyone using this in practice?

I use it - I am writing a subset-of-yaml parser, and I've littered the code with a bunch of abort()/assert() statements for things I don't think should be possible. Running klee over my code spits out ~100K test cases (I let it use any 10 byte YAML input), and so while I don't inspect the output of any of the cases - I do make sure that none of them crash. Similarly, if I make a change which I don't expect to change…

Have you checked out DeepState (https://github.com/trailofbits/deepstate), it's a symbolic unit testing framework that has an interface similar to google test.
Post reply on HN