Efficient Memory Representations for Abstract Interpretation

Institution

The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, development, and innovation. Drawing on the widely acknowledged expertise gained by its 16,000 staff spanned over 9 research centers with a budget of 4.1 billion Euros, CEA actively participates in more than 400 European collaborative projects with a large number of academic (notably as a member of Paris-Saclay University) and industrial partners. Within the CEA Technological Research Division, the CEA List institute addresses the challenges coming from smart digital systems.

Among other activities, CEA List’s Software Safety and Security Laboratory (LSL) research teams design and implement automated analysis in order to make software systems more trustworthy, to exhaustively detect their vulnerabilities, to guarantee conformity to their specifications, and to accelerate their certification. In particular, the open-source Frama-C platform is dedicated to the analysis of C programs (with an experimental C++ front-end).

Scientific context

As software becomes increasingly prevalent in critical applications, concerns about safety and security are growing in importance. To address this concern, formal methods offer a mathematical framework for applying logical reasoning to programs, enabling rigorous proofs of their correctness and the absence of flaws. Among these methods, Abstract Interpretation (Wilhelm 2022) stands out as a theory well-suited for fast and automated program verification.

Eva (Bühler, Maroneze, and Perrelle 2024) is a Frama-C plugin based on Abstract Interpretation dedicated to the automatic inference of properties about C programs, such as the possible values of variables and arithmetic relationships between them. Its primary objective is to prove the absence of runtime errors, including arithmetic overflows and invalid memory accesses, as well as other forms of undefined behavior in C. Such errors can lead to safety issues or introduce vulnerabilities that attackers may exploit. Eva’s results can also support code auditing and serve as a foundation for other program analyses.

A central challenge for abstract interpreters such as Eva is to represent program memory in a way that is both precise and computationally tractable. Most programs manipulate far too many memory locations for an analyzer to maintain a separate description of each one, even more so when dynamic allocation can create an unbounded number of memory locations. A common solution is to group memory locations and summarize the properties shared by the resulting groups (Gopan et al. 2004). For example, array smashing consists in representing an entire array as a single abstract object, allowing the analyzer to infer properties that hold for all its elements.

However, such coarse abstractions are often insufficient to prove the absence of errors in programs that manipulate arrays. More precise abstractions are needed to capture properties that hold only for specific parts of an array. In particular, loop invariants describing array contents are essential for reasoning about array initialization and manipulation.

Consider, for example, a loop that initializes an array to zero by iterating over an index variable i. A suitable loop invariant would express that every element preceding the current index has already been initialized:

∀ℓ,  0 ≤ ℓ < i ⟹ A[ℓ] = 0

More generally, we would like to represent properties of arbitrary array segments, that is, sets of consecutive array elements. Several approaches have been proposed to select and represent such segments during program analysis (Cousot, Cousot, and Logozzo 2011; Halbwachs and Péron 2008).

Eva currently provides two memory models:

• A low-level memory model, which represents memory at the bit level and enables precise and efficient reasoning about low-level memory operations.
• A high-level memory model, which represents typed memory by exploiting the C types associated with memory accesses. It uses distinct abstract representations for structures, unions, and arrays, with a recursive organization that reflects the nesting of these aggregate types.

The high-level memory model incorporates a variant of the array segmentation functor (Cousot, Cousot, and Logozzo 2011).

Internship objectives

The objective of this internship is to design a new abstraction for arrays that improves upon existing abstractions in precision and/or efficiency. The work will combine theoretical investigation with the implementation of a prototype within Frama-C/Eva. Its effectiveness will then be evaluated on the Open-Source-Case-Studies – a curated collection of open-source C programs used to evaluate Frama-C’s analyses.

Two main challenges will be investigated.

Precision challenges

A common approach to array segmentation is to partition an array into disjoint, non-overlapping segments that collectively cover the entire array. The precision of the resulting abstraction strongly depends on the chosen partition, but determining the most appropriate segmentation is a difficult problem.

One possible strategy is to construct the segmentation dynamically, using properties inferred during the analysis, such as equalities and inequalities between index variables. However, the more properties the analyzer discovers, the more possible segmentations it may need to consider. Furthermore, the validity of these properties may only become established as the analysis progresses.

Choosing a partition too early can therefore compromise precision: a segmentation that initially appears appropriate may become unsuitable once additional information about the program becomes available.

To address this issue, we propose investigating an approach that postpones the choice of a definitive segmentation until sufficient information is available. Rather than committing prematurely to a partition, the abstraction would temporarily allow overlapping segments. This additional flexibility could preserve information that would otherwise be lost and enable more precise reasoning about array contents.

Efficiency challenges

Several approaches based on overlapping array segments have already been proposed (Halbwachs and Péron 2008; Perrelle 2013; Gange et al. 2014). However, they face significant computational challenges, as maintaining and manipulating overlapping segments can become expensive.

A key objective will therefore be to reduce the computational cost of the memory abstraction. Possible directions include avoiding unnecessary reductions and simplifying the memory representation when appropriate, for instance before a update affects overlapping segments.

Qualifications

• Minimal

  • Master student in Computer Science or Computer Engineering (M2)
  • Knowledge of OCaml
  • Ability to work in a team

• Preferred

  • A certain flair/affinity for mathematical matters
  • Some knowledge of imperative programming, preferably C

Characteristics

• Duration: 5-6 months

• Location: CEA Nano-INNOV, Paris-Saclay Campus, France (Work From Home possible up to 2-3 days/week)

• Compensation:

  • €1400 monthly stipend
  • Maximum €229 housing and travel expense monthly allowance (in case a relocation is needed)
  • 75% refund of transit pass
  • Subsidized lunches

Application

If you are interested in this internship, please send to the contact persons an application containing:

• Your resume
• A cover letter indicating how your curriculum and experience match the qualifications expected and how you would plan to contribute to the project
• Your bachelor and master transcripts, if any

Applications are welcome until the position is filled. Please note that the administrative processing may take up to 3 months.

Contact persons

For further information or details about the internship before applying, please contact:

• Valentin Perrelle (valentin.perrelle@cea.fr)
• David Bühler (david.buhler@cea.fr)

References