11. Dynamic Symbollic Execution

Question 1

Dynamic Symbolic Execution

Answer 1

Stores program state concretely and symbollically
Solves constraints to guide execution at branch points
Explores all execution paths of the unit tested

Question 2

Computation tree

Answer 2

each node represents the execution of a conditional statement
Each edge represents the execution of a sequence of non-conditional statements
Each path in the tree represents an equivalence class of inputs

Question 3

Node left child is

right child is

Answer 3

false path

true path

Question 4

Random testing approach

Answer 4

Generate random inputs, execute the program on those concrete inputs.

Question 5

Random testing approach problem

Answer 5

PRobablility of reaching error could be astronomically small

Question 6

Symbolic execution approach

Answer 6

Use symbolic values for input
Execute program symbolically on symbolic input values
Collect symbolic path constraints
Use theorem prover to check if a branch can be taken

Question 7

Symbolic execution problem

Answer 7

does not scale for large programs

Question 8

Combined approach - Dynamic Symbolic Execution (DSE)

Answer 8

Start with random input values
Keep track of both concrete values and symbolic constraints
Use concrete values to simplify symbolic constraints

Question 9

Incomplete theorem prover

Answer 9

never declare an unsatisfiable constraint as satisfiable but may not be able to satisfy a satisfiable constraint

Question 10

DSE overvieW

Answer 10

1. init concrete values and establish symbolic state.
2. go through program with values and record the results. If a conditional is passed, write it as a path condition. Keep adding these on.
3. Once a path ends, have the last path condition written be inversed and have the concrete state values be replaced by values that adhere to the inversed last path condition as well as the path conditions before that
4. repeat forever

Question 11

When the DSE may be complex

Answer 11

So like if I have x = ? and y = 7 and z = hash(y)
then hit the condition that z !=x and I want to inverse that
no problem, instead of mixing all the numbers the solver can just keep y constant so z is constant and set x to z

Question 12

DSE false negative example

Answer 12

if(x!=y)
if( hash(x) == hash(y)) ERROR
can’t find a value to satisfy the conditions for that branch so its marked as unsatisfiable and we continue on the true path.

Because of this we fail to find the ERROR in the program creating a false negative

Question 13

DSE is complete/incomplete

Answer 13

complete, it will never return false positives

Question 14

DSE is sound/unsound

Answer 14

unsound, it can miss actual runs of code that lead to errors.

Question 15

symbolic execution is complete/incomplete

Answer 15

incomplete as it may model runs of the program that could never happen, sometimes returning spurious errors

Question 16

symbolic execution is sound/unsound

Answer 16

sound, it will take all reachable branches, so it will never incorrectly declare a program to be error-free