Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
We investigate the decidability of completely automatic program verification for programs that manipulate heaps, and in particular decision procedures for proving memory safety. The work in [Mathur et al. 2019a] identifies decidable sub-classes of uninterpreted programs, but does not address programs that can update functions, which are crucial to model heap-manipulating programs. We develop a new theory of programs, called alias-aware coherent programs, that admits decidable verification. We apply this theory to develop verification algorithms for memory safety— determining if a heap-manipulating program that allocates/frees memory locations and manipulates heap pointers does not dereference a memory location that is not allocated.
We consider this problem when the initial allocated heap forms a forest data-structure (i.e., a disjoint set of trees and lists). While the problem of checking memory safety of programs whose initial heap is a forest data-structure is undecidable, we identify a class of streaming-coherent programs for which the problem is decidable. Our experimental evaluation demonstrates that common library routines that manipulate forest data-structures using a single pass almost always fall in our decidable class. And show that our decision procedure for these programs is effective in both proving memory safety and in identifying memory safety errors.
|Presentation slides (POPL20-talk.pptx)||2.1MiB|
Wed 22 JanDisplayed time zone: Saskatchewan, Central America change
16:50 - 17:35
|Visualization by Example|
Chenglong Wang University of Washington, USA, Yu Feng University of California, Santa Barbara, Rastislav Bodík University of Washington, Alvin Cheung University of California, Berkeley, Işıl Dillig University of Texas AustinLink to publication DOI Media Attached
|Deciding Memory Safety for Single-Pass Heap-Manipulating Programs|
Umang Mathur University of Illinois at Urbana-Champaign, Adithya Murali University of Illinois at Urbana-Champaign, Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Mahesh Viswanathan University of Illinois at Urbana-ChampaignLink to publication DOI Pre-print Media Attached File Attached