Collect functions and values of parameters

[Loi Luu]

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]

I posted this question on StackOverflow with an illustrating example
http://stackoverflow.com/questions/19634022/program-analysis-with-given-input

Thanks,

Post by Loi Luu
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

[DAVID LIGHTSTONE]

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

[DAVID LIGHTSTONE]

Sorry, I used the wrong nomenclature

It's not a call tree, rather it is the tree created when Klee invokes fork

[Loi Luu]

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 <

Post by DAVID LIGHTSTONE
Sorry, I used the wrong nomenclature
It's not a call tree, rather it is the tree created when Klee invokes fork
------------------------------
* 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
------------------------------
* 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,

Post by Loi Luu
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

[DAVID LIGHTSTONE]

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

[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 <

Post by DAVID LIGHTSTONE
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
------------------------------
* 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 <

Post by DAVID LIGHTSTONE
Sorry, I used the wrong nomenclature
It's not a call tree, rather it is the tree created when Klee invokes fork
------------------------------
* 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
------------------------------
* 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,

Post by Loi Luu
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