[klee-dev] String Analysis with KLEE

[Anitha B Gollamudi]

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?
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?)

It would help me to get these questions answered.

-- 
 Anitha