Symbolic Execution Tree for a Program
EXERCISE #30
1
SYMBOLIC EXECUTION REVIEW
Write your name and answer the following on a piece of paper
Draw out the complete symbolic execution tree for the following program. Nodes
should be annotated with the path constraint and line number
01. int main(){02. int c = getchar();
03. if (c > 2){04. if (c < 5){05. return 7;
06. } else {07. return 0 / 1;
08. }
09. }
10. return 3;
11. }
ADMINISTRIVIA
AND
ANNOUNCEMENTS
CONCOLIC EXECUTION
EECS 677: Software Security Evaluation
Drew Davidson
WHERE WE’RE AT
DYNAMIC ANALYSIS
4
- generating test cases
5
PREVIOUSLY: SYMBOLIC EXECUTION
OUTLINE / OVERVIEW
A
DVANCE
A
BSTRACT
S
TATES
ACROSS
THE
PROGRAM
Split abstract states according to predicates to
enhance coverage
Symbolic Execution =/= Burning in Effigy
Use an SMT Solver to determine if the path constraint
is feasible
S
OUND
AND
C
OMPLETE
MODULO
TERMINATION
Stealth caveat of testing as dynamic analysis as well
6
THIS TIME: ENHANCING SYMBOLIC EXECUTION
OUTLINE / OVERVIEW
F
ROM
STATE
TREES
TO
TEST
CASES
7
GENERATING TEST CASES
CONCOLIC EXECUTION
W
AIT
A
MINUTE
… W
E
’
RE
SUPPOSED
TO
BE
BUILDING
A
TEST
SUITE
!
… instead, we generated a symbolic execution tree
8
GENERATING TEST CASES
CONCOLIC EXECUTION
W
AIT
A
MINUTE
… W
E
’
RE
SUPPOSED
TO
BE
BUILDING
A
TEST
SUITE
!
… instead, we generated a symbolic
execution tree
01. int main(){02. int a = getchar();
03. int b = getchar();
04. if (a > 5){05. return 1;
06. } else {07. return 2;
08. }
09. if (b > 3){10. return 3;
11. } else {12. return 4;
13. }
14. }
9
GENERATING TEST CASES
CONCOLIC EXECUTION
W
AIT
A
MINUTE
… W
E
’
RE
SUPPOSED
TO
BE
BUILDING
A
TEST
SUITE
!
… instead, we generated a symbolic
execution tree
01. int main(){02. int a = getchar();
03. int b = getchar();
04. if (a > 5){05. return 1;
06. } else {07. return 2;
08. }
09. if (b > 3){10. return 3;
11. } else {12. return 4;
13. }
14. }
10
FROM TREE TO TESTS
CONCOLIC EXECUTION
E
ACH
STATE
’
S
PATH
CONSTRAINT
SYMBOLIZES
A
SET
OF
TEST
CASES
A
SK
THE
SMT
SOLVER
FOR
A
SATISFYING
ASSIGNMENT
01. int main(){02. int a = getchar();
03. int b = getchar();
04. if (a > 5){05. return 1;
06. } else {07. return 2;
08. }
09. if (b > 3){10. return 3;
11. } else {12. return 4;
13. }
14. }
11
TERMINATION
OUTLINE / OVERVIEW
O
NE
ADVANTAGE
OF
SYMBOLIC
EXECUTION
:
Partial credit
W
E
CAN
GUARANTEE
TERMINATION
AT
THE
EXPENSE
OF
COMPLETENESS
Quit after a certain threshold is met
- Size of the execution tree
- Wall clock time
12
STATE PRUNING
SYMBOLIC EXECUTION
T
ERMINATION
I
NSIGHT
: A
REDUNDANT
STATE
HAS
REDUNDANT
SUCCESSORS
* With proper environmental handling
01. int main(){02. while (true) {03. int b = getchar();
04. if (b > 5){05. return 1;
06. }
07. }
08. }
13
RESEARCH DIRECTION: “FIE ON FIRMWARE”
FUZZING
S
YMBOLIC
E
XECUTION
FOR
“
EXOTIC
”
ENVIRONMENTS
14
STATE PRUNING: LIMITATION
OUTLINE / OVERVIEW
S
ERIOUS
PROGRAMS
LIKELY
HAVE
STATE
SPACE
EXPLOSION
States are too complicated to prune.
15
STATE PRUNING: ALTERNATIVES
OUTLINE / OVERVIEW
S
TATE
P
RIORITIZATION
Akin to the fuzzing heuristics
16
STATE PRUNING: ALTERNATIVES
OUTLINE / OVERVIEW
C
ONCRETIZATION
17
CONCOLIC EXECUTION
OUTLINE / OVERVIEW
18
CONCOLIC EXECUTION
OUTLINE / OVERVIEW
B
ENEFITS
Increased coverage (at the cost of completeness)
Can still pair with termination thresholds
Much easier to deal with model boundaries
WRAP-UP
SYMBOLIC EXECUTION
19
A simple, elegant idea
20
RECALL: TEST CASE GENERATION
SYMBOLIC EXECUTION
21
THE PROBLEM OF COVERAGE
SYMBOLIC EXECUTION
22
PREDICATES GET IN THE WAY!
SYMBOLIC EXECUTION
23
ELIMINATING INFEASIBLE PATHS
SYMBOLIC EXECUTION
24
THE MAGIC OF THE SOLVER
SYMBOLIC EXECUTION
25
THE SYMBOLIC EXECUTION TREE
SYMBOLIC EXECUTION
26
SOUNDNESS / COMPLETENESS
SYMBOLIC EXECUTION
Generate the complete symbolic execution tree for a given program by annotating nodes with path constraints and line numbers, aiding in understanding program execution flow.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
EXERCISE #30 SYMBOLIC EXECUTION REVIEW Write your name and answer the following on a piece of paper Draw out the complete symbolic execution tree for the following program. Nodes should be annotated with the path constraint and line number 01. int main(){ 02. int c = getchar(); 03. if (c > 2){ 04. if (c < 5){ 05. return 7; 06. } else { 07. return 0 / 1; 08. } 09. } 10. return 3; 11. } 1
ADMINISTRIVIA AND ANNOUNCEMENTS
CONCOLIC EXECUTION EECS 677: Software Security Evaluation Drew Davidson
4 WHERE WE RE AT DYNAMIC ANALYSIS - generating test cases
5 PREVIOUSLY: SYMBOLIC EXECUTION OUTLINE / OVERVIEW ADVANCE ABSTRACT STATESACROSSTHE PROGRAM Split abstract states according to predicates to enhance coverage Use an SMT Solver to determine if the path constraint is feasible SOUNDAND COMPLETEMODULOTERMINATION Stealth caveat of testing as dynamic analysis as well Symbolic Execution =/= Burning in Effigy
6 THIS TIME: ENHANCING SYMBOLIC EXECUTION OUTLINE / OVERVIEW FROMSTATETREESTOTESTCASES
7 GENERATING TEST CASES CONCOLIC EXECUTION WAITAMINUTE WE RESUPPOSEDTOBE BUILDINGATESTSUITE! instead, we generated a symbolic execution tree
8 GENERATING TEST CASES CONCOLIC EXECUTION WAITAMINUTE WE RESUPPOSED TOBEBUILDINGATESTSUITE! instead, we generated a symbolic execution tree 01. int main(){ 02. int a = getchar(); 03. int b = getchar(); 04. if (a > 5){ 05. return 1; 06. } else { 07. return 2; 08. } 09. if (b > 3){ 10. return 3; 11. } else { 12. return 4; 13. } 14. }
9 GENERATING TEST CASES CONCOLIC EXECUTION WAITAMINUTE WE RESUPPOSED TOBEBUILDINGATESTSUITE! instead, we generated a symbolic execution tree 01. int main(){ 02. int a = getchar(); 03. int b = getchar(); 04. if (a > 5){ 05. return 1; 06. } else { 07. return 2; 08. } 09. if (b > 3){ 10. return 3; 11. } else { 12. return 4; 13. } 14. }
10 FROM TREE TO TESTS CONCOLIC EXECUTION EACHSTATE SPATHCONSTRAINT SYMBOLIZESASETOFTESTCASES 01. int main(){ 02. int a = getchar(); 03. int b = getchar(); 04. if (a > 5){ 05. return 1; 06. } else { 07. return 2; 08. } 09. if (b > 3){ 10. return 3; 11. } else { 12. return 4; 13. } 14. } ASKTHE SMT SOLVERFORA SATISFYINGASSIGNMENT
11 TERMINATION OUTLINE / OVERVIEW ONEADVANTAGEOFSYMBOLICEXECUTION: Partial credit WECANGUARANTEETERMINATIONATTHE EXPENSEOFCOMPLETENESS Quit after a certain threshold is met - Size of the execution tree - Wall clock time
12 STATE PRUNING SYMBOLIC EXECUTION TERMINATION INSIGHT: A REDUNDANTSTATEHAS REDUNDANTSUCCESSORS * With proper environmental handling 01. int main(){ 02. while (true) { 03. int b = getchar(); 04. if (b > 5){ 05. return 1; 06. } 07. } 08. }
13 RESEARCH DIRECTION: FIE ON FIRMWARE FUZZING SYMBOLIC EXECUTIONFOR EXOTIC ENVIRONMENTS
14 STATE PRUNING: LIMITATION OUTLINE / OVERVIEW SERIOUSPROGRAMSLIKELYHAVESTATESPACEEXPLOSION States are too complicated to prune.
15 STATE PRUNING: ALTERNATIVES OUTLINE / OVERVIEW STATE PRIORITIZATION Akin to the fuzzing heuristics
16 STATE PRUNING: ALTERNATIVES OUTLINE / OVERVIEW CONCRETIZATION
17 CONCOLIC EXECUTION OUTLINE / OVERVIEW
18 CONCOLIC EXECUTION OUTLINE / OVERVIEW BENEFITS Increased coverage (at the cost of completeness) Can still pair with termination thresholds Much easier to deal with model boundaries
19 WRAP-UP SYMBOLIC EXECUTION A simple, elegant idea
20 RECALL: TEST CASE GENERATION SYMBOLIC EXECUTION
21 THE PROBLEM OF COVERAGE SYMBOLIC EXECUTION
22 PREDICATES GET IN THE WAY! SYMBOLIC EXECUTION
23 ELIMINATING INFEASIBLE PATHS SYMBOLIC EXECUTION
24 THE MAGIC OF THE SOLVER SYMBOLIC EXECUTION
25 THE SYMBOLIC EXECUTION TREE SYMBOLIC EXECUTION
26 SOUNDNESS / COMPLETENESS SYMBOLIC EXECUTION
