Memory-Efficient Fixpoint Computation

TL;DR

This paper introduces a memory-efficient method for fixpoint computation in static analysis, significantly reducing peak memory usage without compromising precision or performance, demonstrated through an implementation in the MIKOS tool.

Contribution

It presents an optimal memory minimization technique for Bourdoncle's fixpoint iteration strategy, applicable across abstract domains, and integrates it into a practical static analysis tool.

Findings

Peak-memory usage reduced to 4.07% during assertion verification

Memory usage decreased to 43.7% in buffer-overflow analysis

Technique is proven optimal for Bourdoncle's iteration strategy

Abstract

Practical adoption of static analysis often requires trading precision for performance. This paper focuses on improving the memory efficiency of abstract interpretation without sacrificing precision or time efficiency. Computationally, abstract interpretation reduces the problem of inferring program invariants to computing a fixpoint of a set of equations. This paper presents a method to minimize the memory footprint in Bourdoncle's iteration strategy, a widely-used technique for fixpoint computation. Our technique is agnostic to the abstract domain used. We prove that our technique is optimal (i.e., it results in minimum memory footprint) for Bourdoncle's iteration strategy while computing the same result. We evaluate the efficacy of our technique by implementing it in a tool called MIKOS, which extends the state-of-the-art abstract interpreter IKOS. When verifying user-provided assertions, MIKOS shows a decrease in peak-memory usage to 4.07% (24.57x) on average compared to IKOS. When performing interprocedural buffer-overflow analysis, MIKOS shows a decrease in peak-memory usage to 43.7% (2.29x) on average compared to IKOS.