3 results
Now showing1 - 3 of 3
- Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: with files , BDD-based value analysis for X86 executables(2017); We present an abstract domain for integer value analysis that is especially suited for the analysis of low-level code, where precision is of particular interest. Traditional value analysis domains trade precision for efficiency by approximating value sets to convex shapes. Our value sets are based on modified binary decision diagrams (BDDs), which enable size-efficient storage of integer sets. The associated transfer functions are defined on the structure of the BDDs, making them efficient even for very large sets. We provide the domain in the form of a library that we use in the implementation of a plug-in for the binary analysis framework Jakstab. The library and the plug-in are evaluated by comparison to set representations in traditional value analyses and application of the plug-in to CPU2006 benchmarks respectively.Publicationtype: Doctoral Thesis618 684 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: without files , A non-convex abstract domain for the value analysis of binariesA challenge in sound reverse engineering of binary executables is to determine sets of possible targets for dynamic jumps. One technique to address this challenge is abstract interpretation, where singleton values in registers and memory locations are overapproximated to collections of possible values. With contemporary abstract interpretation techniques, convexity is usually enforced on these collections, which causes unacceptable loss of precision. We present a non-convex abstract domain, suitable for the analysis of binary executables. The domain is based on binary decision diagrams (BDD) to allow an efficient representation of non-convex sets of integers. Non-convex sets are necessary to represent the results of jump table lookups and bitwise operations, which are more frequent in executables than in high-level code because of optimizing compilers. Our domain computes abstract bitwise and arithmetic operations precisely and looses precision only for division and multiplication. Because the operations are defined on the structure of the BDDs, they remain efficient even if executed on very large sets. In executables, conditional jumps require solving formulas built with negation and conjunction. We implement a constraint solver using the fast intersection and complementation of BDD-based sets. Our domain is implemented as a plug-in, called BDDStab, and integrated with the binary analysis framework Jakstab. We use Jakstab's k-set and interval domains to discuss the increase in precision for a selection of compiler-generated executables.Publicationtype: Conference Paper39 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: without files , Driving a sound static software analyzer with branch-and-boundDuring the last decade, static analyzers of source code have improved greatly. Today, precise analyzers that propagate values for the program's variables, for instance with interval arithmetic, are used in the industry. The simultaneous propagation of sets of values, while computationally efficient, is a source of approximations, and ultimately of false positives. When the loss of precision is detrimental to the user's goals, a user needs to provide some kind of manual guidance. Frama-C, a framework for the static analysis of C programs, provides a sound value analyzer. This analyzer can optionally be guided by skillfully placed user annotations. This article describes SPALTER, a Frama-C plug-in that uses a variation of the Skelboe-Moore algorithm from the field of interval arithmetic to guide Frama-C's value analyzer towards a high-level objective set by the user. SPALTER reproduces the results of a case study that used Frama-C's value analysis and required extensive manual guidance. In difference, our approach with SPALTER required no guidance, except preparation of the analyzed program by slicing.Publicationtype: Conference Paper93