JDart and KLEE

1. Execution paths of a program can be seen as a binary execution tree:
   • Internal nodes are decision points in the program
   • Leaves are exit points
   • Execution trees of real programs are infinite
   • The leaves of the "current" execution tree form the set of active states
   • Each path from the root to the leaf represents the execution of an equivalent set of inputs
   • The conjunction of constraints gathered is called path condition (or path constraints)
2. Feasible vs Infeasible paths:
   • Some constraints in conjunction can form unsatisfiable conditions
   • Paths associated with such conjunctions are infeasible
3. Finds errors is any "valid" value on the path breaks the code
4. Dynamic Symbolic Execution:
   • Does not require tests cases (automatic)
   • Reaches deep code paths
   • Achieves high statement/branch coverage
   • Can reason about all possible values on the path
   • Finds bugs that depend on the specific values and/or memory layout
   • Finds functional bugs (crosschecking)
   • Generates concrete test cases for explored paths
   • Generates error reports for found bugs
5. Concolic Execution:
   • Mixed Symbolic and Concrete execution
   • Known as directed automatic random testing or whitebox fuzzing
   • All operations that do not depend on symbolic values are executed as in the original code
   • Can have side effects (syscalls, uninstrumented libraries, etc)
   • Only relevant code is executed symbolically
   • Algorithm:
     1. Start with a concrete input
     2. Run the program on it, collecting PC on the side
     3. Choose a PC prefix, negate last constraint
     4. Solve the new PC to obtain the new input
6. Levels of instrumentation:

   Advantages	Source	Binary
   Source access		Yes
   Recompiling		Yes
   Ease of instrumentation	Yes
   Information available	Yes	Yes

7. Static vs Dynamic instrumentation:
   • Static - change code before it is run, generate new binary, run it
   • Dynamic - instrument the program as it runs, like an interpreter
   • Comparison table

     Advantages	Static	Dynamic
     Tracking dependencies		Yes
     Relinking		Yes
     Dynamically changing instrumentation		Yes
     Self-modifying code		Yes
     Performance	Yes
     Ease of implementation	Yes

8. EXE:
   • Static instrumentation at the source-level
9. KLEE:
   • Dynamic instrumentation at the intermediate level
   • Works as a mixed concrete/symbolic interpreter for LLVM bitcode
   • Uses multiple search heuristics in a round-robin fashion
10. Path exploration:
    • Exploring the most important paths first is essential
    • Search heuristics:
      1. DFS
      2. BFS
      3. Coverage-base heuristic:
         • EXE:
           1. Pick the process that is at the line that has been run the fewest
           2. Run it in DFS for a while
           3. Iterate
         • KLEE:
           1. MD2U = minimum distance from state x to an uncovered instruction
           2. States are selected non-uniformly with weight 1/MD2U²
      4. Random:
         • Subtrees have equal probability of being selected whatever their size is
         • NOT random state selection
         • Favours paths high in the tree (fewer constraints)
         • Loops could cause starvation
    • Elimination redundant paths:
      1. If two paths reach the same point with the same constraint sets, we can prune one of them
      2. We can discard from constraint sets those constraints involving memory that is never read again
      3. Biggest improvement in branch coverage
    • Statically merging paths:
      1. Path merging == outsourcing the problem to the constraint solver
      2. Removes unnecessary conditionals: if (a > b) { max = a; } else { becomes max = select(a>b, a, b); max = b; }
    • Using existing regression testing suites:
      • Pros:
        • Designed to execute interesting behaviour
        • Often achieve good coverage of different program features
      • Cons:
        • Execute each path with a single set of inputs
        • Often exercise the general case, missing edge cases
      • ZESTI:
        • Use the paths executed by the regression suite to bootstrap exploration:
          • Benefits from the coverage of the manual test suite
          • Finds additional errors on these paths
        • Incrementally explore paths around dangerous operations in increasing distance from them:
          • Tests all possible corner cases for the features tested by the test suite
        • No need to construct test drivers (existing tests drive input generation)
11. Constraint solving challenges: (STP is used as an example)
    • Accuracy:
      • Bit-level modelling of memory
      • Many errors are related by corner cases on pointer/integer casting and overflows
      • STP models each memory block as an array of 8-bit bitvectors
      • STP binds types to expressions, not to bits
    • Performance:
      • Real programs generate many expensive constraints
      • Solver must be invoked at every branch
      • Computation is expensive (NP-complete)
12. Constraint solving optimisations:
    • Simplifying and normalising constraints
    • Elimination of irrelevant constraints:
      • Remove all constraints that do not contain the variables used to evaluate the branch
    • Caching constraints:
      • Cache outputs for inputs of constraints and return known output for the seen input
    • Exploiting subset/superset relations:
      • Match cached constraints with the sub/supersets that do not invalidate solutions
    • Accelerating array constraints:
      • Dynamic constant folding on array reads -- pins every element to a constant value
      • Index-based transformation -- remove reads completely and only compare indices
      • Value-based transformation -- replaces array reads with unique value guarded by range checks
    • Environment problem:
      • Choose concrete parameters and call the environment:
        1. Paths missing
        2. potential interaction between paths (side effects)
      • Make results from environment unconstrained:
        1. Infeasible paths
      • Symbolic environment:
        1. Provide a symbolic file system
        2. Vitalises access to native resources among states
        3. Provides symbolic arguments, files with symbolic contents, etc
        4. Has to be implemented at the OS level (because of the syscalls)
13. Testing:
    • Semantics-Preserving Evolution via Crosschecking:
      • Compare optimised vs non-optimised versions
      • Can find semantic errors
      • Crosschecking queries can be solved faster
14. SIMDs:
    • Tame path explosion by statically merging paths
    • Crosschecking queries can be syntactically proved to be equivalent using simple rewrite rules
15. Summary: • Automatic, does not require test cases • Highly systematic – reaches deep code paths – achieves high statement/branch coverage – can reason about all possible values on a path • Finds deep bugs – including those depending on specific values and/or memory layout – including functional bugs (e.g. via crosschecking) – generates inputs that hit the bugs found • Scalability challenges – Path exploration – Constraint solving