Symbolic Execution Tree for a Program

Slide Note

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.

eugenia Follow

Uploaded on May 17, 2024 | 0 Views

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. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

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