Executable Analysis using Abstract Interpretation with Circular Linear Progressions
Citations Over TimeTop 14% of 2007 papers
Abstract
We propose a new abstract domain for static analysis of executable code. Concrete states are abstracted using circular linear progressions (CLPs). CLPs model computations using a finite word length as is seen in any real life processor. The finite abstraction allows handling overflow scenarios in a natural and straight-forward manner. Abstract transfer functions have been defined for a wide range of operations which makes this domain easily applicable for analyzing code for a wide range of ISAs. CLPs combine the scalability of interval domains with the discreteness of linear congruence domains. We also present a novel, lightweight method to track linear equality relations between static objects that is used by the analysis to improve precision. The analysis is efficient, the total space and time overhead being quadratic in the number of static objects being tracked.
Related Papers
- → IKOS: A Framework for Static Analysis Based on Abstract Interpretation(2014)68 cited
- → Hypercollecting semantics and its application to static analysis of information flow(2017)8 cited
- → Generating Features of Windows Portable Executable Files for Static Analysis using Portable Executable Reader Module (PEFile)(2021)6 cited
- → Numerical static analysis with Soot(2013)10 cited
- Value Range Analysis of Executable Code Based on Abstract Interpretation(2010)