[klee-dev] String Analysis with KLEE
Anitha B Gollamudi
anitha.boyapati at gmail.com
Wed Mar 25 20:51:58 GMT 2015
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
More information about the klee-dev
mailing list