[klee-dev] String Analysis with KLEE

[Kuchta, Tomasz]

Hi,

> On 25 Mar 2015, at 20:52, Anitha B Gollamudi <anitha.boyapati at gmail.com> wrote:
> 
> On 25 March 2015 at 16:51, Anitha B Gollamudi <anitha.boyapati at gmail.com> wrote:
>> Hi,
>> 
>> I would like to use KLEE for string analysis (for analyzing SQL
>> injection vulnerabilities). Here are my concerns:
>> 
>> 1. Can KLEE handle arbitrary length strings? Essentially, can I make a
>> 'char *' symbolic with specifying length?
> 
> My apologies, I meant "without specifying length”.

As far as I know you need to specify the length when you create a symbolic object.
One way to handle unknown length might be to make the symbolic array arbitrarily large, then discover how long is
the string that you pass to klee_make_symbolic (by looking for ‘\0’ character) and call klee_assume or concretize that character
(and possibly all that follow) in the symbolic array to make sure that the symbolic string will be of the same length as the original string.

> 
>> 2. Since STP cannot handle string constraints (correct me here!), I am
>> planning to use a reasonably good string solver like Z3-str. Has this
>> effort been tried before? Like making KLEE target Z3-str. ( I came to
>> know of metaSMT project, but am wondering if there is any readily
>> available port that I can use)
>> 
>> 3. Related to (2), how easy is to make KLEE adapt to other STM-LIB
>> conformant solver? (Like weeks or months?)
>> 

You may want to take a look at http://srg.doc.ic.ac.uk/projects/klee-multisolver/ 

>> It would help me to get these questions answered.
>> 
>> —
>> Anitha


HTH,
Best regards

Tomek

> 
> 
> 
> -- 
> Anitha
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 4869 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150326/de8e1df5/attachment.bin>