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 Jan
|16:50 - 17:12|
Chenglong WangUniversity of Washington, USA, Yu FengUniversity of California, Santa Barbara, Rastislav BodikUniversity of Washington, Alvin CheungUniversity of California, Berkeley, Isil DilligUniversity of Texas AustinLink to publication DOI Media Attached
|17:12 - 17:35|
Umang MathurUniversity of Illinois at Urbana-Champaign, Adithya MuraliUniversity of Illinois at Urbana-Champaign, Paul KrogmeierUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Mahesh ViswanathanUniversity of Illinois at Urbana-ChampaignLink to publication DOI Pre-print Media Attached File Attached