[klee-dev] String Analysis with KLEE

[Anitha B Gollamudi]

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".

> 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



-- 
 Anitha