Deciding Memory Safety for Forest Datastructures
share
Memory safety is the problem of 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. Memory safety errors are serious security vulnerabilities that can be exploited systematically to attack systems. In this paper we consider the problem of checking if a program, whose initial allocated heap forms a forest structure (i.e., a disjoint set of trees and lists), is memory safe. While the problem of checking memory safety of programs whose initial heap is a forest structure is undecidable, we identify a class of caching programs for which the problem of checking memory safety is decidable. Our experimental evaluation demonstrates that common library routines that manipulate forest data-structures using a single pass are almost always caching. We show that our decision procedure for such programs is effective in both proving memory safety and in identifying memory safety vulnerabilities.
READ FULL TEXT