Memory Abstraction, Emerging Techniques and Applications

NII Shonan Meeting:

@ Shonan Village Center, September 11 – 14, 2017

Organizers

  • Bor-Yuh Evan Chang, CU Boulder, USA
  • Xavier Rival, INRIA, France
  • Sukyoung Ryu, KAIST, Korea

Overview

Memory abstraction

Static analysis aims at computing semantic properties of programs, so as to verify properties such as absence of runtime errors, functional correctness, termination, security, and more. Since these properties are generally undecidable, automatic program analysis tools usually need to be conservative so as to attempt to prove properties of interest. In that process, they need to reason about all components of the semantics of programs (numeric and symbolic computations, parallelism, etc).

The notion of abstraction [1] is central in static analysis: an abstraction defines a set of logical properties that a program analysis tool may use, their meaning, and the supporting algorithms. Numeric abstractions made strong progress early in the development of static analysis. However, to reason about complex languages (be it C, Java, ML, or JavaScript), analysis tools also need to use a careful abstraction of the structures stored in memory.

Many kinds of memory abstractions have been introduced in the last thirty years. Initially memory abstractions mainly consisted of pointer abstractions based on aliasing graphs or points-to relations. Such abstractions cannot cope precisely with data-structures of unbounded size, thus shape analysis techniques were introduced in the 1990s. Shape analysis techniques rely on more complex mathematical objects to describe unbounded memory graphs by summarizing inductive patterns [2]. In the last decade, a large number of novel techniques and applications for memory abstractions have emerged. Even though the development of memory abstractions still seems to be lagging compared to, e.g., numeric abstraction, recent progresses seem to make this field more mature.

Meeting objectives.

The purpose of the meeting is to bring together experts in the design and in the use of memory abstractions, so as to leverage on the recent advances in this field, allow for the development of new fundamental principles and tools, and ease the use of memory abstractions in emerging applications. In the next two sections we elaborate on the two main aspects of the envisioned seminar, namely the memory abstraction techniques, and their applications. For each aspect, we explain why we think such a meeting would be timely, and outline the expected benefits.

Emerging techniques for memory abstraction.

In the last few years, a large number of new memory abstractions and techniques to construct static analysis tools using them have been developed. We name a few:

Separation logic [3] provides a formal language for precisely expressing memory assertions, and is very convenient for defining analysis algorithms. Indeed, one of the most important issues when reasoning over memory data structures is when an object will be left unmodified by a piece of code, and separation logic can express this very nicely. It was introduced in 2001, and has become increasingly popular in static analysis since 2005 [4, 5].

Dedicated abstractions make it possible to describe families of very complex data structures with very subtle invariants. For instance, array abstractions typically group cells in zones that satisfy different properties, and can express initialization, sortedness, absence of duplicates, etc. Other dedicated abstractions allow to reason over dynamic structures, strings, buffers…

Combination of abstractions have been defined so as to enable the design of analysis tools that can reason about heterogeneous structures (i.e., programs that manipulate several very different structures in memory) or about both memory and numerical properties.

These recent approaches are sophisticated and often rely on rather different mathematical tools, which a one week seminar will allow to discuss more in depth than usual conference talks and tutorials. Moreover, a large number of tools are currently under development, and we expect a seminar to allow participants to discuss implementation efforts more in depth and better explore the possible reuse or sharing of analysis components. Thus, awareness of existing (theoretical and practical) developments should be increased, and opportunities to initiate collaborations.

Novel applications of memory abstractions.

A second important trend is the emergence of new applications for memory abstractions, to cope with different programming languages to analyze and families of target properties to verify.

Quite early, memory abstraction techniques have targeted imperative and object oriented programming languages (such as C, C++, Java). In the last few years, several programming languages have emerged as new targets for memory abstractions. For instance, JavaScript (and other web / scripting languages) has become very popular and raises specific verification problems: as it is untyped and very dynamic, reasoning statically over programs is extremely complex, and requires the development of novel static analysis and memory abstraction techniques [6].

The set of target properties of interest has also grown. Safety properties such as absence of certain classes of errors (null or invalid pointer dereferences) was a natural first target for static analysis and memory abstraction. Structural invariance properties state that certain data structures should remain well formed at all times, and form a very interesting class of (more complex) safety properties. Additionally, analyses to establish liveness properties such as termination also require precise information about memory. Moreover, in the last few years, security properties have become a huge concern (at the level of operating system components, web services, communication and cryptographic protocol implementations). These also require to first compute a precise description of the memory data structures manipulated in programs.

The envisioned seminar will allow to gather designers of memory abstractions and potential users, and will provide an opportunity for these two groups to better exchange on outstanding problems. We expect new collaborations to emerge from such a meeting.

References

[1] Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints Patrick Cousot and Radhia Cousot. POPL 1977.
[2] Parametric Shape Analysis via 3-Valued Logic. Mooly Sagiv, Thomas Reps and Reinhard Wilhelm. POPL 1999.
[3] Separation Logic: A Logic for Shared Mutable Data Structurse. John Reynolds. LICS 2001.
[4] A Local Shape Analysis Based on Separation Logic. Dino Distefano, Peter O’Hearn and
Hongseok Yang. TACAS 2006.
[5] Relational Inductive Shape Analysis. Bor-Yuh Evan Chang and Xavier Rival. POPL 2008.
[6] Scalable and Precise Static Analysis of JavaScript Applications via Loop-Sensitivity. Changhee Park and Sukyoung Ryu. ECOOP 2015.

Comments are closed.