Sun 16 Jan 2022 10:50 - 11:20 at Salon I - Static Analysis and Abstract Interpretation Chair(s): Thomas Wies

To understand and detect possible errors in programs manipulating memory, static analyses of various levels of precision have been introduced, yet it remains hard to capture both information about the byte-level layout and precise global structural invariants. Classical pointer analyses struggle with the latter whereas advanced shape analyses incur a higher computational cost. In this paper, we propose a new memory analysis by abstract interpretation that summarizes the heap by means of a type invariant, using a novel kind of physical types, which express the byte-level layout of values in memory. In terms of precision and expressiveness, our abstraction aims at a middle point between typical pointer analyses and shape analyses, hence the lightweight shape analysis name. We pair this summarizing abstraction with a focusing abstraction which refines information about the memory regions that are in use, hereby allowing strong updates without introducing disjunctions. We show that this combination of abstractions suffices to verify spatial memory safety and non-trivial structural invariants in the presence of low-level constructs such as pointer arithmetic and dynamic memory allocation, on both C and binary code.

Sun 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:20 - 11:50
Static Analysis and Abstract InterpretationVMCAI at Salon I
Chair(s): Thomas Wies New York University
10:20
30m
Paper
Relational String Abstract DomainsRemote
VMCAI
Vincenzo Arceri University of Parma - Department of Mathematical, Physical, and Computer Sciences, Martina Olliaro Ca' Foscari University of Venice - Department of Environmental Sciences, Informatics and Statistics, Agostino Cortesi Università Ca' Foscari Venezia, Pietro Ferrara Università Ca' Foscari, Venezia, Italy
10:50
30m
Paper
Lightweight Shape Analysis based on Physical TypesInPerson
VMCAI
Olivier Nicole CEA LIST, France, Matthieu Lemerre CEA LIST, France, Xavier Rival INRIA/CNRS/ENS Paris
11:20
30m
Paper
A Flow-Insensitive-Complete Program RepresentationRemote
VMCAI
Solène Mirliaz ENS Rennes / IRISA / Inria, David Pichardie Facebook Paris