Report

CREST Internal Yunho Kim Provable Software Laboratory CS Dept. KAIST CREST • CREST is a concolic testing tool for C programs – Generate test inputs automatically – Execute target under test on generated test inputs – Explore all possible execution paths of a target systematically • CREST is a open-source re-implementation of CUTE – mainly written in C++ • CREST’s instrumentation is implemented as a module of CIL(C Intermetiate Language) written in Ocaml 2/20 Yunho Kim Provable SW Lab Overview of CREST code C source code CIL EXT cil/src/ext/crestInstrument.ml CREST symbolic execution library Instrumented code Legend src/libcrest/crest.cc src/base/symbolic_interpreter.cc src/base/symbolic_execution.cc src/base/symbolic_expression.cc src/base/symbolic_path.cc src/base/symbolic_predicate.cc Source code External tool GCC CREST constraint yices run_crest next input 3/20 src/run_crest/run_crest.cc src/run_crest/concolic_search.cc src/base/yices_solver.cc src/base/symbolic_execution.cc src/base/symbolic_expression.cc src/base/symbolic_path.cc src/base/symbolic_predicate.cc src/base/basic_types.cc Yunho Kim Provable SW Lab Directory Structure • src/ : Base libraries for symbolic execution base/ libcrest/ : Probe code for collecting symbolic states process_cfg/ : CFG generator for CFG-based search heuristic run_crest/ : Main function of run_crest and search algorithms tools/ : A tool for printing execution path from szd_execution • cil/src/ext/crestInstrument.ml – A CIL module for instrumentation 4/20 Yunho Kim Provable SW Lab CREST Code Metrics Name Value .h 9 .cc 12 Total 21 Code 2,210 Others 1,595 Total 3,805 # of files # of lines 5/20 # of classes 14 # of functions 147 Yunho Kim Provable SW Lab Symbolic Execution Component • Symbolic execution component collects symbolic states during concrete execution and manages symbolic execution paths • Related files File Content src/libcrest/crest.cc Probe functions inserted into instrumented target src/base/symbolic_interpreter.cc Main symbolic execution engine for CREST src/base/symbolic_execution.cc A class for a symbolic execution which consists of symbolic path and inputs src/base/symbolic_path.cc A class for a symbolic path which is a sequence of symbolic predicates at taken branches src/base/symbolic_predicate.cc A class for a symbolic predicate which consists of a symbolic expression and a comparator src/base/symbolic_expression.cc A class for a symbolic expression 6/20 Yunho Kim Provable SW Lab Symbolic Interpreter • Symbolic interpreter performs dynamic symbolic execution during execution of a target program • Symbolic interpreter implements a symbolic machine which has stack-architecture • 4 types of statements – – – – Symbolic variable initialization Assignments Applying operators Branches 7/20 Yunho Kim Provable SW Lab Symbolic Machine • Symbolic machine has a symbolic stack, symbolic memory and a symbolic predicate register – Symbolic memory stores symbolic expressions – Symbolic stack element: <symbolic expr, concrete value> – If the top of the stack is a predicate, the predicate is stored in the symbolic predicate register Symbolic stack Symbolic memory Address 8/20 Symbolic predicate register Symbolic expression Yunho Kim Provable SW Lab Example Revisited 1 #include <crest.h> 2 main() { 3 int a,b,c, match=0; 4 CREST_int(a); \ CREST_int(b); \ CREST_int(c); 5~9 … omitted… 10 if(a==b) match=match+1; 10~32 … omitted … 33 } 9/20 int a, b, c; #line 4 /* Initializes symbolic variables a, b, c */ __CrestInt(& a); __CrestInt(& b); __CrestInt(& c); … omitted … #line 10 { /* Creates symbolic expression a==b */ __CrestLoad(36, (unsigned long )(& a), (long long )a); __CrestLoad(35, (unsigned long )(& b), (long long )b); __CrestApply2(34, 12, (long long )(a == b)); if (a == b) { //extern void __CrestBranch(int id , int bid , unsigned char b ) __CrestBranch(37, 11, 1); /* Creates symbolic expression match = match = 1; */ __CrestLoad(41, (unsigned long )(& match), (long long )matc h); __CrestLoad(40, (unsigned long )0, (long long )1); __CrestApply2(39, 0, (long long )(match + 1)); __CrestStore(42, (unsigned long )(& match)); match ++; } else { __CrestBranch(38, 12, 0); } Yunho Kim } Provable SW Lab Symbolic Variable Initialization • Creates a symbolic memory element in symbolic memory – A concrete address of a variable is used as a symbolic address • Suppose that we start with the input a = b = c = 0; Symbolic variable initialization int a, b, c; #line 4 /* Initializes symbolic variables a, b, c */ __CrestInt(& a); __CrestInt(& b); __CrestInt(& c); Symbolic stack Symbolic memory Address Symbolic expression &a a &b b &c c Symbolic predicate register 10/20 Yunho Kim Provable SW Lab Symbolic Compare Operator(1/4) • Symbolic compare operator is used for a branch condition and results in a symbolic predicate – The predicate is store in a symbolic predicate register #line 10 { /* Creates symbolic expression a==b */ __CrestLoad(36, (unsigned long)(&a), (long long )a); Symbolic PC __CrestLoad(35, (unsigned long)(&b), (long long )b); __CrestApply2(34, 12, (long long )(a == b)); if (a == b) { 11/20 Symbolic stack Symbolic memory Address Symbolic expression &a a &b b &c c Symbolic predicate register Yunho Kim Provable SW Lab Symbolic Compare Operator(2/4) • __CrestLoad(int id, unsigned long *ptr, long long val) function loads a symbolic expression which ptr points to and pushes <loaded expr, val> to the stack – If *ptr is a concrete variable, the function pushes <NULL, val> to the stack #line 10 { /* Creates symbolic expression a==b */ __CrestLoad(36, (unsigned long)(&a), (long long )a); __CrestLoad(35, (unsigned long)(&b), Symbolic PC (long long )b); __CrestApply2(34, 12, (long long )(a == b)); if (a == b) { Symbolic stack Symbolic memory Address Symbolic expression &a a &b b &c c Symbolic predicate register <a, 0> 12/20 Yunho Kim Provable SW Lab Symbolic Compare Operator(3/4) #line 10 { /* Creates symbolic expression a==b */ __CrestLoad(36, (unsigned long)(&a), (long long )a); __CrestLoad(35, (unsigned long)(&b), (long long )b); __CrestApply2(34, 12, (long long )(a == b)); if (a == b) { Symbolic PC Symbolic stack <b, 0> Symbolic memory Address Symbolic expression &a a &b b &c c Symbolic predicate register <a, 0> 13/20 Yunho Kim Provable SW Lab Symbolic Compare Operator(4/4) • __CrestApply2(int ID, int op_type, long long val) 1. pops two elements from the stack, 2. applies a binary operator corresponding to op_type to the popped elements, 3. pushes a result to the stack if the result is not a predicate – A predicate is stored in the register #line 10 { /* Creates symbolic expression a==b */ __CrestLoad(36, (unsigned long)(&a), (long long )a); __CrestLoad(35, (unsigned long)(&b), (long long )b); __CrestApply2(34, 12, (long long )(a == b)); if (a == b) {//extern void __CrestBranch(int id , int bid , unsigned char b ) __CrestBranch(37, 11, 1); Symbolic PC 14/20 Symbolic stack Symbolic memory Address Symbolic expression &a a &b b &c c Symbolic predicate register <a==b, 1> Yunho Kim Provable SW Lab Symbolic Branch(1/2) • Whenever a branch statement is executed, CREST stores which branch is taken by calling __CrestBranch() function. #line 10 { /* Creates symbolic expression a==b */ __CrestLoad(36, (unsigned long)(&a), (long long )a); __CrestLoad(35, (unsigned long)(&b), (long long )b); __CrestApply2(34, 12, (long long )(a == b)); if (a == b) { //extern void __CrestBranch(int id , int bid , unsigned char b ) __CrestBranch(37, 11, 1); Symbolic PC 15/20 Symbolic stack Symbolic memory Address Symbolic expression &a a &b b &c c Symbolic predicate register <a==b, 1> Yunho Kim Provable SW Lab Symbolic Branch(2/2) • Symbolic path is a sequence of <symbolic pred, branch ID> • __CrestBranch(int id, int bid, unsigned char b) function appends a new element <symbolic pred, bid> to the current symbolic path – Symbolic pred comes from the register – If b == 0, negated predicate is appended if (a == b) { //extern void __CrestBranch(int id , int bid , unsigned char b ) __CrestBranch(37, 11, 1); /* Creates symbolic expression match = match = 1; */ __CrestLoad(41, (unsigned long )(& match), Symbolic PC (long long )match); 16/20 Symbolic stack Symbolic memory Address Symbolic expression &a a &b b &c c Symbolic predicate register Symbolic path: <a==b, 11> Yunho Kim Provable SW Lab Symbolic Arithmetic Operator (1/2) • Symbolic arithmetic operator is similar to symbolic compare operator – Pops operands from the stack, applies operator to the operands, and pushes the result to the stack if (a == b) { __CrestBranch(37, 11, 1); /* Creates symbolic expression match = match = 1; */ __CrestLoad(41, (unsigned long )(& match), (long long )match); Symbolic __CrestLoad(40, (unsigned long )0, PC (long long )1); __CrestApply2(39, 0, (long long )(match + 1)); __CrestStore(42, (unsigned long )(& match)); match ++; 17/20 Symbolic stack <NULL, 1> Symbolic memory Address Symbolic expression &a a &b b &c c Symbolic predicate register <NULL, 0> Symbolic path: <a==b, 11> Yunho Kim Provable SW Lab Symbolic Arithmetic Operator (2/2) • If at least one of operands is symbolic, the result is also symbolic – Otherwise, the result is concrete if (a == b) { __CrestBranch(37, 11, 1); /* Creates symbolic expression match = match = 1; */ __CrestLoad(41, (unsigned long )(& match), (long long )match); __CrestLoad(40, (unsigned long )0, (long long )1); __CrestApply2(39, 0, (long long )(match + 1)); __CrestStore(42, (unsigned long )(& match)); match ++; Symbolic Symbolic stack Symbolic memory Address Symbolic expression &a a &b b &c c Symbolic predicate register <NULL, 2> PC 18/20 Symbolic path: <a==b, 11> Yunho Kim Provable SW Lab Symbolic Assignment (1/1) • __CrestStore(int id, unsigned long *ptr) function pops one element from the stack and update symbolic memory – If the popped element is concrete, just ignore it – If the element is symbolic • If ptr has an entry in symbolic memory, the corresponding symbolic expression is updated • Otherwise, a new entry is added to symbolic memory Symbolic stack __CrestApply2(39, 0, (long long )(match + 1)); __CrestStore(42, (unsigned long )(& match)); match ++; Symbolic PC Symbolic memory Address Symbolic expression &a a &b b &c c Symbolic predicate register 19/20 Symbolic path: <a==b, 11> Yunho Kim Provable SW Lab Conclusion • CREST does not support full ANSI-C semantics – – – – No symbolic pointer dereference Only linear integer arithmetic No bit-wise operator And so on • To support them, we need to improve CREST’s dynamic symbolic interpreter engine • I hope this presentation will be a good starting point 20/20 Yunho Kim Provable SW Lab