Hi, > On 25 Mar 2015, at 20:52, Anitha B Gollamudi <[email protected]> > wrote: > > On 25 March 2015 at 16:51, Anitha B Gollamudi <[email protected]> > 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 > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<<attachment: winmail.dat>>
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
