Please enable JavaScript.

Coggle requires JavaScript to display documents.

2015 - Multi-Platform Binary Program Testing Using Concolic Execution…

- - - - Input files
        
        Input selection
        
        Scoring
        
        Produces a new path of execution
        
        Number of inputs executed targeting this branch
        
        Targets the uncovered edge of a known branch
        
        Length of the path
        
        Initialize algorithm with seed input
        
        Length of the content should vary since the system only varies the content of the file, but not the length of it.
        
        New input obtained from mutating previous input based on constraint information from the model
      - Begin recording of program execution with input
      - Concolic execution of PANDA replay
        
        Branch Constraint
        
        LLVM instrumentation
        
        Augment LLVM code with callback function
        
        Implemented by LLVM pass
        
        Memory I/O
        
        If the memory location is not tainted, the byte from the concrete memory is picked and turned into a bit-vector.
        
        If an instruction reads a value from memory as an operator, and that memory is marked as tainted, we construct a new bit-vector expression with the size of the read.
        
        Need to capture potential symbolic values read from (or written to) shadow memory, while still mixing in concrete values from the underlying storage if no symbolic values are present.
        
        Operator Translation
        
        Translates LLVM instruction in the form of a symbolic SMT-LIB expression
        
        Symbolic Pointers
        
        When the address read from or written to is tainted i.e. is a symbolic value. This involves that the exact result of the operation depends on the input
      - SMT solver solves selected constraint
        
        Z3 SMT solver
      - Generate new input
        
        Test Case Generation
        
        Once the constraints of the current test case have been captured, new inputs are generated using the solutions to the constraints produced by Microsoft's Z3 SMT solver
        
        Individual constraints are iteratively negated
  - - - Taint analysis requires bookkeeping of the taint state of the systems memory, including I/O memory and CPU registers, in order to properly propagate taint.
  - - - Restricted variant of symbolic execution
      - Instead of covering all possible execution paths in one execution, concolic execution outputs the PC that is recorded during a single execution.
      - Generate new input files by selectively negating individual branch constraints and solving the resulting, new, path constraint.
    - - List of logical frst-order expressions
        depending on the input variables.
    - - Not scaling well to larger applications
  - - - Determining if an interpretation of boolean variables for a given boolean formula exists
  - - - Executing a program with (semi-)random inputs in an automated fashion with the goal of causing errors in the program.
  - - - Complex Control Flow Logic
        
        Samples from real-world applications
        
        Server software
        
        Sendmail
        
        WU-FTP
        
        BIND
        
        Source code with buffer overflow vulnerabilities
        
        Not all of the samples could be run
      - Complex Branch Conditions
        
        Simple Comparison
        
        Nested if statements
        
        Loop:
        
        Simple Arithmetic
        
        Arithmetic operations to verify common binary operations
        
        Complex Arithmetic
        
        Larger equation based on two integers read from the input file is compared to a constant value
        
        strcmp
        
        Larger equation based on two integers read from
        the input file is compared to a constant value
    - - American Fuzzy Lop fuzzing tool