IA159 Formal Verification Methods
Symbolic execution
Jan Strejˇcek
Department of Computer Science
Faculty of Informatics
Masaryk University
Focus and sources
Focus
symbolic execution
automated whitebox fuzz testing
Sources
J. C. King: Symbolic Execution and Program Testing,
Communications of ACM, 1976.
P. Godefroid, M. Y. Levin, and D. Molnar: Automated
whitebox fuzz testing, NDSS 2008.
Special thanks to Marek Trtík for providing me his slides.
IA159 Formal Verification Methods: Symbolic execution 2/37
Motivation
1 procedure sum (a, b, c) {
2 x := a + b
3 y := b + c
4 z := x + y − b
5 return(z)
6 }
Testing checks that a program behaves correctly on selected
inputs:
sum (1, 1, 1) =
sum (1, 2, 3) =
. . .
IA159 Formal Verification Methods: Symbolic execution 3/37
Motivation
1 procedure sum (a, b, c) {
2 x := a + b
3 y := b + c
4 z := x + y − b
5 return(z)
6 }
Testing checks that a program behaves correctly on selected
inputs:
sum (1, 1, 1) = 3
sum (1, 2, 3) = 6
. . .
IA159 Formal Verification Methods: Symbolic execution 4/37
Motivation
1 procedure sum (a, b, c) {
2 x := a + b
3 y := b + c
4 z := x + y − b
5 return(z)
6 }
We can execute the program with symbols α1, α2, α3 representing
arbitrary values:
sum (α1, α2, α3) =
IA159 Formal Verification Methods: Symbolic execution 5/37
Motivation
1 procedure sum (a, b, c) {
2 x := a + b
3 y := b + c
4 z := x + y − b
5 return(z)
6 }
We can execute the program with symbols α1, α2, α3 representing
arbitrary values:
sum (α1, α2, α3) = α1 + α2 + α3
→ symbolic execution
IA159 Formal Verification Methods: Symbolic execution 6/37
Symbolic execution semantics in general
Each programing language has an execution semantics
describing:
the data objects which program variables may represent;
how statements manipulate data objects;
how control flows through the statements of a program.
In symbolic execution semantics:
real data objects can be represented by symbols
basic operators of the language are extended to accept
symbolic input and produce symbolic output.
The execution semantics is changed for symbolic execution, but
neither the language syntax nor the individual programs written
in the language are changed.
IA159 Formal Verification Methods: Symbolic execution 7/37
Simple programming language
Consider the following programming language:
all program variables are of type unbounded signed integer
input can be obtained by procedure parameters, global
variables, or read operations
arithmetic expressions may contain only operators +, −, ∗
commands:
assignment <var> := <expr>
GOTO <label>
IF-THEN-ELSE with condition <expr> ≥ 0
IA159 Formal Verification Methods: Symbolic execution 8/37
Semantics of the language
Standard execution semantics
data objects = signed integers
. . .
Symbolic execution semantics
besides integers, we can use symbols from the list
α1, α2, α3, . . . to represent some data objects
the only oportunity to introduce symbolic data objects is as
inputs to the program
the evaluation rules for arithmetic expressions used in
assignments and IF statements must be extended to
handle symbolic values
GOTO’s function exactly as in normal executions
IA159 Formal Verification Methods: Symbolic execution 9/37
Extending rules for expressions and IF statement
Values of expressions and variables are integer polynomials
over the symbols α1, α2, . . ..
IA159 Formal Verification Methods: Symbolic execution 10/37
Extending rules for expressions and IF statement
Values of expressions and variables are integer polynomials
over the symbols α1, α2, . . ..
Although IF statement do not change state of program
variables, it plays a key role in definition of symbolic semantics.
We extend system state by path condition pc, which is a
conjunction of inequalities of the form R ≥ 0 or ¬(R ≥ 0),
where R is a polynomial over α1, α2, . . ..
pc is initially set to true
pc can only be modified when executing IF statements
Intuitively, pc accumulates conditions navigating the execution
to the current path.
IA159 Formal Verification Methods: Symbolic execution 11/37
Extending path condition
Let q be an inequality resulting from substituting values of
variables into condition of a IF statement.
Assuming pc ≡ false, at most one of the following implications
can be valid:
(a) pc =⇒ q
(b) pc =⇒ ¬q
IA159 Formal Verification Methods: Symbolic execution 12/37
Extending path condition
Let q be an inequality resulting from substituting values of
variables into condition of a IF statement.
Assuming pc ≡ false, at most one of the following implications
can be valid:
(a) pc =⇒ q
(b) pc =⇒ ¬q
If one implication is valid, then we speak about non-forking execution
and pc is not changed.
If (a) is valid, the execution continues by THEN branch.
If (b) is valid, the execution continues by ELSE branch.
IA159 Formal Verification Methods: Symbolic execution 13/37
Extending path condition
Let q be an inequality resulting from substituting values of
variables into condition of a IF statement.
Assuming pc ≡ false, at most one of the following implications
can be valid:
(a) pc =⇒ q
(b) pc =⇒ ¬q
When neither (a) nor (b) is valid, then we speak about forking execution.
The current execution forks into two independent ones,
since both branches are possible. Path conditions of resulting
executions are updated as follows:
pc := pc ∧ q for THEN branch
pc := pc ∧ ¬q for ELSE branch
IA159 Formal Verification Methods: Symbolic execution 14/37
Example
1 procedure power (x, y) {
2 z := 1
3 j := 1
4 lab: if y − j ≥ 0 then
5 z := z ∗ x
6 j := j + 1
7 goto lab
8 return(z)
9 }
IA159 Formal Verification Methods: Symbolic execution 15/37
Example: symbolic execution of power(α1, α2)
# j x y z pc
1 ? α1 α2 ? true
2 - - - 1 -
3 1 - - - IA159
Formal Verification Methods: Symbolic execution 16/37
Example: symbolic execution of power(α1, α2)
# j x y z pc
1 ? α1 α2 ? true
2 - - - 1 -
3 1 - - - -
4 neither true =⇒ α2 − 1 ≥ 0
nor true =⇒ ¬(α2 − 1 ≥ 0)
is valid → fork
IA159 Formal Verification Methods: Symbolic execution 17/37
Example: symbolic execution of power(α1, α2)
# j x y z pc
1 ? α1 α2 ? true
2 - - - 1 -
3 1 - - - -
4 neither true =⇒ α2 − 1 ≥ 0
nor true =⇒ ¬(α2 − 1 ≥ 0)
is valid → fork # j x y z pc
4 1 α1 α2 1 α2 ≥ 1 4 1 α1 α2 1 ¬(α2 ≥ 1)
5 - - - α1 - 8 done, returns 1 when α2 < 1
6 2 - - - -
7 - - - - IA159
Formal Verification Methods: Symbolic execution 18/37
Example: symbolic execution of power(α1, α2)
# j x y z pc
1 ? α1 α2 ? true
2 - - - 1 -
3 1 - - - -
4 neither true =⇒ α2 − 1 ≥ 0
nor true =⇒ ¬(α2 − 1 ≥ 0)
is valid → fork # j x y z pc
4 1 α1 α2 1 α2 ≥ 1 4 1 α1 α2 1 ¬(α2 ≥ 1)
5 - - - α1 - 8 done, returns 1 when α2 < 1
6 2 - - - -
7 - - - - -
4 neither α2 ≥ 1 =⇒ α2 ≥ 2
nor α2 ≥ 1 =⇒ ¬(α2 ≥ 2)
is valid → fork
IA159 Formal Verification Methods: Symbolic execution 19/37
Example: symbolic execution of power(α1, α2)
# j x y z pc
1 ? α1 α2 ? true
2 - - - 1 -
3 1 - - - -
4 neither true =⇒ α2 − 1 ≥ 0
nor true =⇒ ¬(α2 − 1 ≥ 0)
is valid → fork # j x y z pc
4 1 α1 α2 1 α2 ≥ 1 4 1 α1 α2 1 ¬(α2 ≥ 1)
5 - - - α1 - 8 done, returns 1 when α2 < 1
6 2 - - - -
7 - - - - -
4 neither α2 ≥ 1 =⇒ α2 ≥ 2
nor α2 ≥ 1 =⇒ ¬(α2 ≥ 2)
is valid → fork # j x y z pc
4 2 α1 α2 α1 α2 ≥ 1 ∧ 4 2 α1 α2 α1 α2 ≥ 1 ∧
α2 ≥ 2 ¬(α2 ≥ 2)
5
... 8 done, returns α1 when α2 = 1
IA159 Formal Verification Methods: Symbolic execution 20/37
Path condition is always satisfiable
Clearly, every path condition corresponds exactly to one
execution path and vice versa.
Theorem
At each point of every symbolic execution pc ≡ false.
Proof: Initially, pc is set to true. Further, pc is modified only at
forking executions, using assignments of the form pc := pc ∧ q
and pc := pc ∧ ¬q.
Forking execution implies that pc =⇒ ¬q is not valid. Hence,
¬(pc =⇒ ¬q) is satisfiable. As pc ∧ q ≡ ¬(pc =⇒ ¬q),
pc ∧ q is also satisfiable.
The case pc ∧ ¬q is similar.
IA159 Formal Verification Methods: Symbolic execution 21/37
Symbolic execution tree
The execution paths followed during the symbolic execution of
a procedure can be expressed by symbolic execution tree.
executed statement = a node labeled with the statement
number
transition between executed statements = a directed arc
connecting the corresponding nodes
for each forking IF statement execution there are two
outgoing arcs labeled with T and F for THEN and ELSE
branch, respectively
IA159 Formal Verification Methods: Symbolic execution 22/37
Symbolic execution tree for power(α1, α2)
1
2
3
4
5
8
6
7
4
5
8
T
F
T
F
IA159 Formal Verification Methods: Symbolic execution 23/37
Symbolic execution tree
Lemma
For each terminal leaf in the tree there does exist particular
non-symbolic input, which will trace the same path.
Proof: Every input satisfying the corresponding pc trace the
same path. As pc is always satisfiable, there exists such an
input.
Lemma
Path conditions associated with any two terminal leaves are
distinct, i.e. pc1 ∧ pc2 ≡ false.
Proof: The two paths leading from the root to two different
terminal nodes have a unique forking node where the paths
diverge. At that forking node some q was added to one while
¬q to the other. Since q ∧ ¬q ≡ false, the lemma holds.
IA159 Formal Verification Methods: Symbolic execution 24/37
Commutativity
If one normally executes a program with a specific set of
integers {ji}, the result will be the same as executing it
symbolically (using a set of {αi}) and then instantiating the
symbolic results, i.e. assigning {ji} to {αi}.
P,{αi},{ji}
P,{αi} ← {ji}
P({αi}),{ji}
P({ji})
Set parameters to integer values
Symbolic execution
Standard execution
Substitute into symbolic result
IA159 Formal Verification Methods: Symbolic execution 25/37
Applications in verification
Programs can be enriched with ASSUME(ϕ) and ASSERT(ϕ)
statements. When symbolic execution passes through
ASSUME(ϕ), it executes pc := pc ∧ ϕ.
ASSERT(ϕ) and pc =⇒ ϕ is not valid, it reports an error.
With these constructs, symbolic execution can be used with a
modification of Floyd’s proof method to prove program
correctness.
This application is straightforward for any program whose
symbolic execution tree is finite.
IA159 Formal Verification Methods: Symbolic execution 26/37
Practical issues
The symbolic execution of IF and ASSERT statements
requires to decide validity of some implications.
Unfortunately, even for simple programming languages
(including our simple language) it is impossible to build
theorem prover that will decide validity of such implications.
The conflict between discrete arithmetics of computer and
continuous nature of real numbers with infinite precision is
an issue.
Variable storage referencing problem: Let expression A(I)
references some element in array A. When the value of I is
a symbolic expression, the particular element being
referenced is a function of the program input.
Unsatisfactory solution: Let v(I) be symbolic value of I.
Then we might resolve the reference A(I) with
ITE(v(I) = 1, v(A(1)), ITE(v(I) = 2, v(A(2)), . . .) . . .)
IA159 Formal Verification Methods: Symbolic execution 27/37
Practical issues (cont.)
Poor performance of symbolic execution on cycles without
fixed number of iterations (symbolic execution forks again
and again) → path explosion.
Symbolic execution cannot be precise in practice due to
pointer manipulation, complex arithmetic operations
(e.g. in hashing, encryption or decryption), calls to
operating system and libraries
Some of these issues and non-existence of a theorem
prover can be partially solved by concolic execution.
IA159 Formal Verification Methods: Symbolic execution 28/37
Concolic execution
concolic = concrete + symbolic
program is executed on a real input and on symbolic input
simultaneously
symbolic execution does not fork, it always follows the
concrete execution and computes pc
if a symbolic value is not available, we can switch to a
concrete one
IA159 Formal Verification Methods: Symbolic execution 29/37
Real applications
Symbolic execution is more exploitable in program testing
then in program verification.
Typical applications: bug finding, test generation and
analysis of abstract error traces.
Often combined with other techniques.
Used in many tools including KLEE, PEX, SAGE, SLAM,
etc.
IA159 Formal Verification Methods: Symbolic execution 30/37
Bonus
Automated whitebox fuzz testing
IA159 Formal Verification Methods: Symbolic execution 31/37
Automated whitebox fuzz testing
an example of modern and sophisticated testing method
implemented in SAGE (Scalable, Automated, Guided
Execution)
discovered 30+ new bugs in large-shipped (i.e. intensively
tested) file-reading Windows applications including image
processors, media players, file decoders
combines fuzz testing and symbolic execution in a better
way than whitebox dynamic test generation
Fuzz testing
a form of blackbox random testing
randomly mutates well-formed input and test the program
on resulting data
popular since the Month of Browser Bugs (July 2006)
IA159 Formal Verification Methods: Symbolic execution 32/37
Whitebox dynamic test generation
the process follows this scenario
1 test the program with a given correct input
2 symbolically execute the discovered execution path
3 use path condition to generate an input that changes the
evaluation of a condition on the execution path
4 test the program with the new input
5 go to the step 2
the condition of step 3 can be selected in depth-first search
or breath-first search manner
the problem is that the symbolic executions are extremely
expensive
IA159 Formal Verification Methods: Symbolic execution 33/37
Automated whitebox fuzz testing
tries to generate as many new inputs from one symbolic
execution as possible
input for the next iteration is selected by some scoring
function applied to all generated inputs
in particular, inputs exploring the biggest (so-far
uncovered) pieces of code are chosen for the next
symbolic execution
in this way, SAGE can well recover from divergencies
(situations when an execution deviates from the assumed
execution path)
IA159 Formal Verification Methods: Symbolic execution 34/37
Automated whitebox fuzz testing: example
Example
void top(char input[4]) {
int cnt=0;
if (input[0] == ’b’) cnt++;
if (input[1] == ’a’) cnt++;
if (input[2] == ’d’) cnt++;
if (input[3] == ’!’) cnt++;
if (cnt >= 3) abort(); // error
}
IA159 Formal Verification Methods: Symbolic execution 35/37
Symbolic execution tree for power(α1, α2)
0 1 1 2 1 2 2 3 1 2 2 3 2 3 3 4
good goo! godd god! gaod gao! gadd gad! bood boo! bodd bod! baod bao! badd bad!
IA159 Formal Verification Methods: Symbolic execution 36/37
Coming next week
Abstract interpretation + static analysis
Another standard approach.
Applicable to large software projects, e.g. Linux kernel.
What can one learn about a program without executing it?
IA159 Formal Verification Methods: Symbolic execution 37/37