Lightweight Shape Analysis based on Physical Types
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 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 11:50
|Relational String Abstract DomainsRemote|
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
|Lightweight Shape Analysis based on Physical TypesInPerson|
|A Flow-Insensitive-Complete Program RepresentationRemote|