Questions tagged [symbolic-execution]
36 questions
11
votes
4 answers
What are the gaps between symbolic execution and taint analysis?
I recently read a paper titling "All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)" by Dr. EJ Schwartz. In the paper, he mainly talked about their applications in binary level…
Hongxu Chen
- 5,240
- 2
- 45
- 85
9
votes
2 answers
In concolic testing, what does "concrete execution" mean?
I came across the terms "concrete & symbolic execution" when I was going through the concept of concolic testing. (The article mentioned there, "CUTE: A concolic unit testing engine for C", uses that term in its abstract section.)
"The approach…
Suhas Chikkanna
- 1,292
- 5
- 20
- 34
7
votes
2 answers
symbolic execution and model-checking
What is the difference between symbolic execution and model checking (for example in model transformation)? I don't understand difference of them. Are they the same?!
any
- 325
- 5
- 17
5
votes
1 answer
How to implement a symbolic execution engine for a particular language?
I'm considering using symbolic execution to test the robustness of programs written in a particular language such as java. I've read some papers introducing the basic concepts of symbolic execution. But I'm not clear about how to get it started.…
clasnake
- 309
- 2
- 9
3
votes
1 answer
Out-of-bounds `select` even though I `constrain` the index
I have a static-length list of values ks :: [SInt16] and an index x :: SInt16. I'd like to index into the list using x:
(.!) :: (Mergeable a) => [a] -> SInt16 -> a
xs .! i = select xs (error "(.!) : out of bounds") i
I would expect to be able to…
Cactus
- 27,075
- 9
- 69
- 149
3
votes
3 answers
Reachability and symbolic execution
Now I am confused about symbolic execution (SE) and reachability analysis (RA). As I know, SE uses symbols to execute some code to reach each branch with branch conditions. And RA can be used to find the reachability of each branch, right? When RA…
Eve
- 785
- 3
- 7
- 15
2
votes
0 answers
how to use 'stdin' in angr
I'm new to angr, trying to solve a simple executable, it reads 3 characters and compare to string 'abc'.
#include
using namespace std;
int main() {
char v[3];
scanf("%3s", v);
if(v[0] == 'a' && v[1] == 'b' && v[2] == 'c') {…
aj3423
- 2,003
- 3
- 32
- 70
2
votes
1 answer
Efficient way to "keep turning the crank" on a stateful computation
I have a stateful process that is modelled as an i -> RWS r w s a. I want to feed it an input cmds :: [i]; currently I do that wholesale:
let play = runGame theGame . go
where
go [] = finished
go ((v, n):cmds) =…
Cactus
- 27,075
- 9
- 69
- 149
2
votes
1 answer
implement symbolic execution without model-checking
How can I implement symbolic execution for particular language without using model checking and Finite State Machine (FSM) for example not such as Java Path Finder? I need a detail about it. for example by what language I can implement this symbolic…
any
- 325
- 5
- 17
2
votes
2 answers
Static analysis vs. symbolic execution in implementation
What is the difference between implementation of static analysis and symbolic execution?
any
- 325
- 5
- 17
2
votes
1 answer
Is there any symbolic execution tools in llvm?
I want to do points-to anlysis in llvm IR. I want it to be path sensitive, which means that when I print out the result, I need append the condition for the "May" Points-to.
I plan to using symbolic execution to achieve this goal.
Are there any…
blankboy2011
- 349
- 1
- 10
1
vote
1 answer
Why IR is needed for symbolic execution?
For example, KLEE works on LLVM bitcode.
Can we build symbolic execution directly on C source code?
RJ J
- 15
- 3
1
vote
1 answer
Is this how to test a stateful API with klee symbolic execution?
I'm currently testing out a few approaches on how to test and fuzz a C API. In the process thereof I found KLEE which runs the code symbolically, meaning that it tries to cover all branches that depend on some symbolic input and checks for all sorts…
NikLeberg
- 65
- 1
- 5
1
vote
0 answers
how to apply constraints to heap side effects in angr
I'm trying to use angr to verify a function's behavior by deriving the correct input for a given result. The function modifies a buffer, in this case it simply copies the input to it, so I set up symbolic variables on the heap that I apply an…
ragingSloth
- 1,094
- 8
- 22
1
vote
1 answer
How is Symbolic Execution different from Whitebox Fuzzing?
I do not understand how symbolic execution is different from Whitebox fuzzing? From what I understand, Whitebox Fuzzers symbolically execute the code with some initial input format.
Additionally, it will be helpful if someone could differentiate…
Madhuparna Bhowmik
- 2,090
- 4
- 12
- 22