MASc seminar - Sanu Edayath Subramanian

Wednesday, November 18, 2015 11:00 am - 11:00 am EST (GMT -05:00)


Sanu Edayath Subramanian


Bit-Vector Support In Z3-str2 Decision Procedure


Vijay Ganesh


Improper string manipulations are an important cause of software defects, which makes them an important target for program analysis. Symbolic execution based program analysis techniques that systematically explore paths through a program requires reasoning about string and bit-vector constraints cohesively. The current state of the art symbolic execution engines for programs written in C/C++ languages tracks constraints on a bit-level and uses bit-vector solver to reason about the collected path constraints. However, string functions incur high-performance penalties and lead to path explosion in the symbolic execution engine. The current state of the art string solvers are written primarily for the analysis of web applications with underlying support for the theory of strings and integers, which limits their use in the analysis of low-level programs. Therefore, we designed a decision procedure for the theory of strings and bit-vectors atop of Z3-str2 to efficiently solve word equations and length functions over bit-vectors. Furthermore, the new theory combination has a significant role in the detection of integer overflows and memory corruption vulnerabilities associated with string operations. We introduced a new search space pruning technique for string lengths based on binary search approach, which enable the decision procedure to solve constraints involving large strings. We evaluated the decision procedure on a set of real security vulnerabilities collected from Common Vulnerabilities and Exposures (CVE) database and compared the result against the state of the art string-integer solver. We also conduct experiments to evaluate the search space pruning technique on a benchmark suite and present imperial comparison with other solvers.