Search

We present the Z3strBV solver for a many-sorted first-order quantifier-free theory Tw,bv of string equations, string length represented as bit-vectors, and bit-vector arithmetic aimed at formal verification, automated testing, and security analysis of C/C++ applications. Our key motivation for building such a solver is the observation that existing string solvers are not efficient at modeling the combined theory over strings and bit-vectors. We demonstrate experimentally that Z3strBV is significantly more efficient than a reduction of string/bit-vector constraints to strings/natural numbers followed by a solver for strings/natural numbers or modeling strings as bit-vectors. We also propose two optimizations. First, we explore the concept of library-aware SMT solving, which fixes summaries in the SMT solver for string library functions such as strlen in C/C++. Z3strBV is able to consume these functions directly instead of re-analyzing the functions from scratch each time. Second, we experiment with a binary search heuristic that accelerates convergence on a consistent assignment of string lengths. We also show that Z3strBV is able to detect nontrivial overflows in realworld system-level code, as confirmed against seven security vulnerabilities from the CVE and Mozilla databases. [ABSTRACT FROM AUTHOR]

We present a novel technique, automatic input rectification, and a prototype implementation, SOAP. SOAP learns a set of constraints characterizing typical inputs that an application is highly likely to process correctly. When given an atypical input that does not satisfy these constraints, SOAP automatically rectifies the input (i.e., changes the input so that it satisfies the learned constraints). The goal is to automatically convert potentially dangerous inputs into typical inputs that the program is highly likely to process correctly. Our experimental results show that, for a set of benchmark applications (Google Picasa, ImageMagick, VLC, Swfdec, and Dillo), this approach effectively converts malicious inputs (which successfully exploit vulnerabilities in the application) into benign inputs that the application processes correctly. Moreover, a manual code analysis shows that, if an input does satisfy the learned constraints, it is incapable of exploiting these vulnerabilities. We also present the results of a user study designed to evaluate the subjective perceptual quality of outputs from benign but atypical inputs that have been automatically rectified by SOAP to conform to the learned constraints. Specifically, we obtained benign inputs that violate learned constraints, used our input rectifier to obtain rectified inputs, then paid Amazon Mechanical Turk users to provide their subjective qualitative perception of the difference between the outputs from the original and rectified inputs. The results indicate that rectification can often preserve much, and in many cases all, of the desirable data in the original input. [ABSTRACT FROM AUTHOR]

We present a new automated white box fuzzing technique and a tool, BuzzFuzz , that implements this technique. Unlike standard fuzzing techniques, which randomly change parts of the input file with little or no information about the underlying syntactic structure of the file, BuzzFuzz uses dynamic taint tracing to automatically locate regions of original seed input files that influence values used at key program attack points (points where the program may contain an error). BuzzFuzz then automatically generates new fuzzed test input files by fuzzing these identified regions of the original seed input files. Because these new test files typically preserve the underlying syntactic structure of the original seed input files, they tend to make it past the initial input parsing components to exercise code deep within the semantic core of the computation. We have used BuzzFuzz to automatically find errors in two open-source applications: Swfdec (an Adobe Flash player) and MuPDF (a PDF viewer). Our results indicate that our new directed fuzzing technique can effectively expose errors located deep within large programs. Because the directed fuzzing technique uses taint to automatically discover and exploit information about the input file format, it is especially appropriate for testing programs that have complex, highly structured input file formats. [ABSTRACT FROM AUTHOR]