Questions tagged [symbolic-execution]
The symbolic-execution tag has no usage guidance.
symbolic-execution
39
questions
0
votes
0
answers
50
views
How to find all paths as a sequence of constraints in angr
I am trying to find all possible paths of all functions from binary executables as a sequence of symbolic expressions and constraints that are compatible with z3 or claripy from the start of any ...
- 21
0
votes
0
answers
22
views
Can I directly perform symbolic execution on P-Code with angr?
I have successfully translate an ELF to P-Code with the following codes.
from pypcode import Context, PcodePrettyPrinter
ctx = Context("sparc:BE:64:default")
with open('example', 'rb') as f:
...
-1
votes
1
answer
27
views
Is there a trade-off between pruning in symbolic execution and coverage as well as the final detection performance? [closed]
A common issue in symbolic execution is path explosion. Would using pruning and other heuristic strategies lead to decreased coverage and thus affect its effectiveness?
- 23
2
votes
0
answers
52
views
Does KLEE symbolic execution support code coverage with gcov or other tools?
I am trying to obtain code coverage information from KLEE executions. Does KLEE support gcov? I know KLEE provides general coverage information in the istats files, but I want to combine the coverage ...
- 31
0
votes
1
answer
120
views
Is Symbolic Execution a formal Verification technique?
I have spent two days researching on Formal Methods and formal Verification to be more specific. I also came across Symbolic Execution and I don't know whether this is a formal verification technique? ...
- 499
0
votes
2
answers
389
views
How Can I execute a function in angr using concrete value?
In Angr, I have a code like this
#include <stdio.h>
typedef struct A_struct
{
int data1;
int data2;
} A;
void bar(A* a){
a->data2 += 1;
}
void foo(A* a)
{
a->data1 +=...
- 1
0
votes
1
answer
70
views
How can I translate z3::expr(bv_val) into a bit representation of a number?
I am trying to translate Z3::expr into a bit representation of a number in order to find out how many bits 1 the number contains and if the number of bits 1 is even, then I raise the flag.
I wrote the ...
- 15
1
vote
1
answer
83
views
Why IR is needed for symbolic execution?
For example, KLEE works on LLVM bitcode.
Can we build symbolic execution directly on C source code?
- 23
0
votes
1
answer
38
views
How do I create a testcase that targets a specified branch?
I try to "dynamic symbolic execution" with klee.
How do I create a testcase that targets a specified branch?
int a = 0;
klee_make_symbolic(&a, sizeof(a), "a");
if (a == 0)
...
- 5
0
votes
1
answer
109
views
I am unable to get back the file I saved after exiting from the Klee
I am researching symbolic execution based on the klee tool. I am running klee via docker. I create a directory and save c program file in that directory. But after exiting from klee, and again If I ...
- 1
1
vote
1
answer
172
views
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 ...
- 65
0
votes
1
answer
175
views
How to annotate a program to detect dead-code with z3-solver?
Intro
Given a simple function written in C++ as below:
int func(int x, int y)
{
if (x < 3)
{
y = 4;
if (x < 4)
{
y = y + 2;
}
else
...
- 875
1
vote
0
answers
418
views
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 ...
- 1,104
1
vote
1
answer
525
views
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 ...
- 2,260
0
votes
1
answer
516
views
Why is this Symbolic Execution with Z3 resulting in an error?
I am trying to generate test cases using a symbolic execution logic based on the SMT Solver Z3.
I have the following code.
void foo(int a, int b, int c){
int x = 0, y = 0, z = 0;
if(a){
...
user12392751