Detecting memory-safety violations in binaries is complicated by the lack of knowledge of the intended data layout, i.e., the locations and sizes of objects. We present lightweight, static, heuristic analyses for recovering the intended layout of data in a stripped binary. Comparison against DWARF debugging information shows high precision and recall rates for inferring source-level object boundaries. On a collection of benchmarks, our analysis eliminates a third to a half of incorrect object boundaries identified by an IDA Pro-inspired heuristic, while retaining nearly all valid object boundaries. In addition to measuring their accuracy directly, we evaluate the effect of using the recovered data for improving the precision of static buffer-overrun detection in the defect-detection tool CodeSonar/x86. We demonstrate that CodeSonar's false-positive rate drops by about 80% across our internal evaluation suite for the tool, while our approximation of CodeSonar's recall only degrades about 25%.

We present a points-to analysis technique suitable for environments with small time and memory budgets, such as just-in-time (JIT) compilers and interactive development environments (IDEs). Our technique is demand-driven, performing only the work necessary to answer each query (a request for a variable's points-to information) issued by a client. In cases where even the demand-driven approach exceeds the time budget for a query, we employ early termination, i.e., stopping the analysis prematurely and returning an over-approximated result to the client. Our technique improves on previous demand-driven points-to analysis algorithms [17, 33] by achieving much higher precision under small time budgets and early termination.We formulate Andersen's analysis [5] for Java as a CFL-reachability problem [33]. This formulation shows that Andersen's analysis for Java is a balanced-parentheses problem, an insight that enables our new techniques. We exploit the balanced parentheses structure to approximate Andersen's analysis by regularizing the CFL-reachability problem, yielding an asymptotically cheaper algorithm. We also show how to regain most of the precision lost in the regular approximation as needed through refinement. Our evaluation shows that our regularization and refinement approach achieves nearly the precision of field-sensitive Andersen's analysis in time budgets as small as 2ms per query. Our technique can yield speedups of up to 16x over computing an exhaustive Andersen's analysis for some clients, with little to no precision loss.

Automatic discovery of relationships among values of array elements is a challenging problem due to the unbounded nature of arrays. We present a framework for analyzing array operations that is capable of capturing numeric properties of array elements.In particular, the analysis is able to establish that all array elements are initialized by an array-initialization loop, as well as to discover numeric constraints on the values of initialized elements.The analysis is based on the combination of canonical abstraction and summarizing numeric domains. We describe a prototype implementation of the analysis and discuss our experience with applying the prototype to several examples, including the verification of correctness of an insertion-sort procedure.