Symbolic Execution

Question 1

What are the steps of symbolic execution?

Answer 1

Replacing inputs with symbolic values
Executing along a path using the symbolic values to build a formula over the input symbols
Solve for the symbolic symbols to find inputs that yield the path

Question 2

______ symbolic execution works over traces. In this one, it’s driven by one program execution

Answer 2

dynamic

Question 3

CBMC is an example of _________ symbolic execution

Answer 3

Static

Question 4

Using symbolic execution can also determine satisfiable inputs in one program but not the other. This represents a _______

Answer 4

regression

Question 5

What do SMT solvers do? What are some examples?

Answer 5

They solve constraints.
SAT
SMTLIB2

Question 6

What are 2 ways to traverse the execution tree? Describe them

Answer 6

Concolic (dynamic symbolic): Given a first input, construct the symbolic formula while execution. It’s essentially depth first search. After finishing a branch, negate the very last conjunct to take the other path.

Execution Generated Testing: Set some inputs to be symbolic, then execute forward. At the next split, solve the formula for each branch to create a frontier of explored paths

Question 7

What are some applications for symbolic execution?

Answer 7

Creating test suites via path and branch coverage
Targeted tests: ask for inputs that drive execution through areas of interest
Automated exploit discovery: Extension of the above point. You could encode the constraints of an error in the program path. You could inject shell code into your initial inputs

Question 8

What are some challenges with symbolic execution?

Answer 8

Path explosion (loops, many ifs)
Challenging constraints (we cannot solve all constraints, ex password hashes)
Constraint representation on domain knowledge (how can we represent memory?)

Question 9

How can we alleviate the issues of path explosion?

Answer 9

Search heuristics

Memoization

Question 10

How can we alleviate the issues of challenging constraints?

Answer 10

Observe the actual values of variables in runs we have and reuse these values