Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Arithmetizing Shape Analysis

Sebastian Wolff, Ekanshdeep Gupta, Zafer Esen, Hossein Hojjat, Philipp Rümmer, Thomas Wies

TL;DR

This paper tackles automatic memory-safety verification for heap-manipulating programs by arithmetizing shape analysis through a reduction-based approach that combines flow abstraction and view abstraction. By decorating heap objects with flow information and reasoning about a bounded view of stack-referenced objects, the authors reduce memory-safety proofs to checking heap-free imperative programs with off-the-shelf backends, enabling automatic verification for both sequential and concurrent data structures. The core contributions include a novel flow-based view abstraction, its formal grounding via Galois connections, and an implementation (triceratops) that demonstrates broad applicability to singly-, doubly-linked, and nested structures as well as trees, with competitive empirical results against specialized tools. This work broadens the applicability of shape reasoning by decoupling heap reasoning from verification backends, offering a flexible, scalable path to memory-safety verification across diverse data structures and concurrency settings.

Abstract

Memory safety is an essential correctness property of software systems. For programs operating on linked heap-allocated data structures, the problem of proving memory safety boils down to analyzing the possible shapes of data structures, leading to the field of shape analysis. This paper presents a novel reduction-based approach to memory safety analysis that relies on two forms of abstraction: flow abstraction, representing global properties of the heap graph through local flow equations; and view abstraction, which enable verification tools to reason symbolically about an unbounded number of heap objects. In combination, the two abstractions make it possible to reduce memory-safety proofs to proofs about heap-less imperative programs that can be discharged using off-the-shelf software verification tools without built-in support for heap reasoning. Using an empirical evaluation on a broad range of programs, the paper shows that the reduction approach can effectively verify memory safety for sequential and concurrent programs operating on different kinds of linked data structures, including singly-linked, doubly-linked, and nested lists as well as trees.

Arithmetizing Shape Analysis

TL;DR

This paper tackles automatic memory-safety verification for heap-manipulating programs by arithmetizing shape analysis through a reduction-based approach that combines flow abstraction and view abstraction. By decorating heap objects with flow information and reasoning about a bounded view of stack-referenced objects, the authors reduce memory-safety proofs to checking heap-free imperative programs with off-the-shelf backends, enabling automatic verification for both sequential and concurrent data structures. The core contributions include a novel flow-based view abstraction, its formal grounding via Galois connections, and an implementation (triceratops) that demonstrates broad applicability to singly-, doubly-linked, and nested structures as well as trees, with competitive empirical results against specialized tools. This work broadens the applicability of shape reasoning by decoupling heap reasoning from verification backends, offering a flexible, scalable path to memory-safety verification across diverse data structures and concurrency settings.

Abstract

Memory safety is an essential correctness property of software systems. For programs operating on linked heap-allocated data structures, the problem of proving memory safety boils down to analyzing the possible shapes of data structures, leading to the field of shape analysis. This paper presents a novel reduction-based approach to memory safety analysis that relies on two forms of abstraction: flow abstraction, representing global properties of the heap graph through local flow equations; and view abstraction, which enable verification tools to reason symbolically about an unbounded number of heap objects. In combination, the two abstractions make it possible to reduce memory-safety proofs to proofs about heap-less imperative programs that can be discharged using off-the-shelf software verification tools without built-in support for heap reasoning. Using an empirical evaluation on a broad range of programs, the paper shows that the reduction approach can effectively verify memory safety for sequential and concurrent programs operating on different kinds of linked data structures, including singly-linked, doubly-linked, and nested lists as well as trees.
Paper Structure (29 sections, 10 theorems, 28 equations, 9 figures, 2 tables)

This paper contains 29 sections, 10 theorems, 28 equations, 9 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. Contribution
  4. Flow abstraction
  5. View abstraction
  6. Organization
  7. Heap Programs
  8. Semantics.
  9. View Abstraction
  10. Abstract Domain and Transformer
  11. Characterization of Best Abstract Transformer
  12. Flow-based View Abstraction
  13. Flows and Flow Graphs
  14. Abstract Domain and Transformer
  15. Local Abstract Transformer
  16. ...and 14 more sections

Key Result

proposition 1

$\langle \alpha^{\mathsf{v}},\gamma^{\mathsf{v}} \rangle$ form a Galois connection.

Figures (9)

  • Figure 1: A program $P$ that non-deterministically allocates a singly-linked list and then deallocates it again. The right side depicts a state reachable at $\ell_2$.
  • Figure 2: Operational semantics of basic commands.
  • Figure 3: View semantics of basic commands. Some rules are omitted.
  • Figure 4: Illustration of updates following the scheme outlined in \ref{['lem:frame-preserving-update']}. The heap $h_0$ (left) is updated to $h'$ (right) without affecting the interface: node $a_2$ receives a combined flow value of $1$ before and after the update and the locality condition for the update is satisfied.
  • Figure 5: Local flow-based view semantics of basic commands. Some rules are omitted.
  • ...and 4 more figures

Theorems & Definitions (10)

  • proposition 1
  • lemma 1: Characterization of $\alpha^{\mathsf{v}}$
  • corollary 1
  • theorem 1
  • lemma 2
  • proposition 2
  • corollary 2
  • lemma 3
  • theorem 2
  • lemma 4