Understanding Symbolic Execution and Directed Automated Random Testing
Symbolic Execution is a method used for analyzing programs to determine inputs causing each part to execute, vital in program testing. However, limitations arise in cases without code availability, hindering definitive path conditions. Directed Automated Random Testing (DART) overcomes this through a combination of concrete and symbolic execution, enabling more effective program testing and path condition collection.
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
Symbolic Execution with Mixed Concrete-Symbolic Solving (SymCrete Execution) Jonathan Manos
About the Paper Article found on ACM Digital Library Title: Symbolic Execution with Mixed Concrete-Symbolic Solving Published in: ISSTA '11 Proceedings of the 2011 International Symposium on Software Testing and Analysis Authors: Corina S. P s reanu Neha Rungta Willem Visser
What is Symbolic Execution? A method of analyzing a program to determine what inputs cause each part of a program to execute Used extensively in program testing void test(int y) { if (y == 2) S1; else S2; }
Symbolic Execution Testing void test(int y) { if (y == 2) S1; else S2; } When [y == 2] we get to S1 When [y != 2] we get to S2 These rules are known as Path Conditions
Symbolic Execution in practice Many testing tools make use of symbolic execution Microsoft uses Pex, SAGE, YOGI, and PREfix IBM uses Apollo NASA and Fujitsu use Symbolic (Java) PathFinder Others: UIUC s CUTE and jCUTE Stanford s KLEE UC Berkeley s CREST BitBlaze
Symbolic Execution Testing void test(int x, int y) { if (y == hash(x)) S1; else S2; } There is no code available for hash(x) Therefore we cannot have any definitive path conditions or constraints Therefore Symbolic Execution is not possible
Directed Automated Random Testing (DART) Also known as Concolic Execution Combination of concrete and symbolic execution Executes programs concretely Collects the path condition Runs and executes again with newly found solutuions Conquers the incompleteness of symbolic execution
DART Testing Aim: n/a void test(int x, int y) { if (x > 0){ if (y == hash(x)) test(1, 0) [X > 0] S0; else S1; [X > 0 & Y != 10] if (x > 3 && y > 10) S3; else S4; } [X > 0 & Y != 10 & X <= 3] } Reached: S1 and S4
DART Testing (cont..) Aim: to reach S3; void test(int x, int y) { if (x > 0){ if (y == hash(x)) S0; else S1; if (x > 3 && y > 10) S3; else S4; } } TEST: [X > 0 & Y != 10 & X > 3] test(4, 0) [X > 0] [X > 0 & Y != 40] [X > 0 & Y != 40 & X > 3 & Y <= 10] Reached: S1 and S4
DART Testing (cont..) Aim: to reach S3; TEST: [X > 0 & Y > 10 & Y != 10 & X > 3] test(4, 11) [X > 0] void test(int x, int y) { if (x > 0){ if (y == hash(x)) S0; else [X > 0 & Y != 40] S1; if (x > 3 && y > 10) S3; else S4; [X > 0 & Y != 40 & X > 3 & Y > 10] } Reached: S1 and S3 }
DART Testing (cont..) Aim: to reach S0; TEST: [X > 0 & Y = 40 & Y != 10 & X > 3] test(4, 40) [X > 0] void test(int x, int y) { if (x > 0){ if (y == hash(x)) [X > 0 & Y = 40] S0; else S1; if (x > 3 && y > 10) S3; else S4; [X > 0 & Y = 40 & X > 3 & Y > 10] Reached: S0 and S3 } }
DART Testing (cont..) Aim: to reach S0 and S4 TEST: [X > 0 & Y = 40 & Y != 10 & X <= 3] test(1, 40) [X > 0] void test(int x, int y) { if (x > 0){ if (y == [40]hash(x)) S0; else S1; if (x > 3 && y > 10) S3; else S4; } } [X > 0 & Y != 10] [X > 0 & Y != 10 & X <= 3 & Y > 10] Reached: S1 and S4 DIVERGENCE! Cannot ever finish
Flaws of Execution Strategies Symbolic Execution Sound method, but incomplete functionality Cannot solve problems when: there is no access to code The decision procedures do not work DART Execution Complete method, but unsound performance Can fail when: functions are unpredictable
Symbolic Execution with Mixed Concrete-Symbolic Solving (DART) Concolic = Concrete + Symbolic Concrete execution that produces symbolic path conditions SymCrete = Symbolic + Concrete Symbolic execution that falls back to concrete execution as it is needed
SymCrete Execution Methodology 1. Split the Path Condition into two parts: EASY: Part you can solve symbolically HARD: Part you cannot solve symbolically 2. Solve the easy part symbolically and evaluate the hard part with concrete execution 3. Replace the hard part with the evaluated results and check if results are SAT SAT Satisfies the given boolean formula or Satisfiable
SymCrete Execution void test(int x, int y) { if (x > 0){ if (y == hash(x)) [X > 0] S0; [X > 0 & Y = hash(X) ] S0 Easy 1. X > 0 Y = hash(X) 2. X = 1 Y = hash(1) = 10 3. [X > 0 & Y = 10] is SAT else hard S1; if (x > 3 && y > 10) S3; else S4; [X > 0 & Y != hash(X) ] S1 [X>0 & Y != 10] is SAT } } native int hash(x) { if (0<=x<=10) return x*10; else return 0; }
SymCrete Execution void test(int x, int y) { if (x > 0){ if (y == hash(x)) [X > 0] S0; [X > 0 & Y = hash(X) ] S0 else S1; [X > 3 & Y = hash(X) & Y > 10]S0 and S3 1. X > 3 & Y > 10 Y = hash(X) 2. X = 4 & Y = 11 Y = hash(4) = 40 3. [X > 3 & Y = 40 & Y > 10] is SAT if (x > 3 && y > 10) S3; else S4; } [X > 0 & Y = hash(X) & X <= 3]S0 and S4 1. X > 0 & X <= 3 Y = hash(X) 2. X = 1 Y = hash(1) 3. [X > 0 & Y = 10 & X <= 3] is SAT } native int hash(x) { if (0<=x<=10) return x*10; else return 0; }
Why SimCrete > DART SimCrete avoids the problem of being unsound Checks if boolean path condition is SAT If not SAT, SimCrete will not continue with that path condition DART would continue with the found path condition and diverge SimCrete s Benefits: uses the simplicity of symbolic execution Adds the additional features of DART (concrete execution)
Implementation of SymCrete ex. Symbolic Execution extension for Java s PathFinder called jpf-symbc Symbolic PathFinder SPF -Willem Visser s PowerPoint Model Checker for Java Open Source http://babelfish.arc.nasa. gov/trac/jpf -Willem Visser s PowerPoint
Works Cited 1. P s reanu, Corina S., Neha Rungta, and Willem Visser. "Symbolic Execution with Mixed Concrete-symbolic Solving." ISSTA '11 Proceedings of the 2011 International Symposium on Software Testing and Analysis Table of Contents (2011): 34-44. ACM Digital Library. ACM, 17 July 2011. Web. 1 Mar. 2015. 2. Powerpoint from one of the authors (Willem Visser)
