Scaling Concolic Execution of Binary Programs for Security Applications

Concolic execution is a technique for program analysis that makes the values of certain inputs symbolic, symbolically executes a program’s code, and computes a symbolic logical formula to represent a desired behavior of the program under analysis. The computed formula is then solved by a decision procedure to determine whether the desired behavior is feasible and, if so, provide an example program input that satisfies the formula. Concolic execution and similar techniques have widely been applied to a variety of securityrelated applications including automatic test input generation, vulnerability discovery, exploit generation, signature generation, protocol reverse engineering, and detecting deviations between software implementations. Although there has been a great success in applying it to various securityrelated