[klee-dev] Collect functions and values of parameters

[Loi Luu]

Thanks David.
I've been working around and hooking into some parts of KLEE. Seems like
KLEE randomizes the symbolic string from the start of execution. At each
function call, all arguments are concrete, for example what I got from
strcmp(x, y) operator (x is symbolic):
strcmp

ARGUMENT 0/2 = 54242560
 Type = Constant Width = 64 ZExtValue Value = 54242560
ARGUMENT 1/2 = 54209552
 Type = Constant Width = 64 ZExtValue Value = 54209552

Of course for Integer variable, KLEE maintains the symbolic property. For
the function get_sign(int a):
get_sign
ARGUMENT 0/1 = (ReadLSB w32 0 a)

So what I want now is to track the symbolic property of each variable. For
example, if we have x is symbolic string and s = x + "123", then s is
marked as symbolic and I want to store the relationship s = x + "123" also.
Which part of KLEE should I start working on?

Thank you,


On Tue, Oct 29, 2013 at 6:06 PM, DAVID LIGHTSTONE <
david.lightstone at prodigy.net> wrote:

> I suspect not always. The reason being that the involving call may not be
> on the stack.
> Quite likely the library call will be somewhere between two KLEE branch
> fork invocations.
>
> For your example where the involving call is in the conditional, the
> answer is yes.
>
> This suggests that the library will need to be modified so as to output to
> a trace file the argument lists that you wish to capture ; A lot of work.
> The effort has a definite recursion to avoid; the various print procedures
> use the library also
>
> There are code translation systems such as ROSE which probably can
> automate the modification effort, but there is a nontrivial effort needed
> to learn them.
>
> Dave Lightstone
>
>  ------------------------------
> * From: * Loi Luu <loi.luuthe at gmail.com>;
> * To: * DAVID LIGHTSTONE <david.lightstone at prodigy.net>;
> * Cc: * klee-dev <klee-dev at imperial.ac.uk>;
> * Subject: * Re: [klee-dev] Collect functions and values of parameters
> * Sent: * Tue, Oct 29, 2013 2:20:27 AM
>
>   Thank you David. Are we able to query the values of parameters in each
> function call by KLEE? Using the line numbers generated by KLEE to identify
> the invokes tree is easy, but to get the parameter values parsed into each
> function I'm not sure.
>
> Regards,
>
>
> On Tue, Oct 29, 2013 at 2:29 AM, DAVID LIGHTSTONE <
> david.lightstone at prodigy.net> wrote:
>
>> Sorry, I used the wrong nomenclature
>>
>> It's not a call tree, rather it is the tree created when Klee invokes fork
>>
>>  ------------------------------
>> * From: * DAVID LIGHTSTONE <david.lightstone at prodigy.net>;
>> * To: * Loi Luu <loi.luuthe at gmail.com>; <klee-dev at imperial.ac.uk>;
>>  * Subject: * Re: [klee-dev] Collect functions and values of parameters
>> * Sent: * Mon, Oct 28, 2013 6:01:09 PM
>>
>>   Take a look at your favorite debugger. Ask the question - how does it
>> figure the call tree?
>>
>> When KLEE writes out the test case, walk the call tree in the same
>> fashion as the debugger until you get to main.
>>
>> You probably need a debug version of the code to get the symbols needed
>> to play this game, but it should work. Use the line numbers to identify the
>> branch locations, there may not be symbols at those locations
>>
>> Dave Lightstone
>>
>>  ------------------------------
>> * From: * Loi Luu <loi.luuthe at gmail.com>;
>> * To: * klee-dev <klee-dev at imperial.ac.uk>;
>> * Subject: * Re: [klee-dev] Collect functions and values of parameters
>> * Sent: * Mon, Oct 28, 2013 4:34:20 PM
>>
>>   I posted this question on StackOverflow with an illustrating example
>> http://stackoverflow.com/questions/19634022/program-analysis-with-given-input
>>
>> Thanks,
>>
>>
>> On Mon, Oct 28, 2013 at 6:54 PM, Loi Luu <loi.luuthe at gmail.com> wrote:
>>
>>> Hi,
>>>
>>> Given a program path, I wanna track all libc functions  (in path
>>> condition) with their corresponding parameters in each execution path. For
>>> example, given the branch condition if (strcmp(s, s1)) in which s is
>>> symbolic, s1 is concrete; I wanna get the function name (strcmp), the value
>>> of s1 and the return value of this function. Which part of KLEE should I
>>> modify to get it stored in each execution state and printed in somewhere
>>> like .pc file.
>>>
>>> Thanks,
>>>
>>> --
>>> Loi, Luu The (Mr.)
>>> RA at Security Lab, SoC, NUS
>>>
>>
>>
>>
>> --
>> Loi, Luu The (Mr.)
>> RA at Security Lab, SoC, NUS
>>
>
>
>
> --
> Loi, Luu The (Mr.)
> RA at Security Lab, SoC, NUS
>



-- 
Loi, Luu The (Mr.)
RA at Security Lab, SoC, NUS
-------------- next part --------------
HTML attachment scrubbed and removed