The downgrading semantics of memory safety (Extended version)

TL;DR

This paper introduces a semantic framework for memory safety focusing on allocator-dependent issues, extending noninterference concepts to include downgrading in low-level memory models.

Contribution

It proposes a notion of gradual allocator independence that captures allocator-specific memory safety aspects, extending the noninterference connection with downgrading mechanisms.

Findings

Defines a formal notion of gradual allocator independence.

Extends noninterference to account for allocator limitations and pointer casts.

Provides a technical treatment of downgrading using information flow machinery.

Abstract

Memory safety is traditionally characterized in terms of bad things that cannot happen. This approach is currently embraced in the literature on formal methods for memory safety. However, a general semantic principle for memory safety, that implies the negative items, remains elusive. This paper focuses on the allocator-specific aspects of memory safety, such as null-pointer dereference, use after free, double free, and heap overflow. To that extent, we propose a notion of gradual allocator independence that accurately captures the allocator-dependent aspects of memory safety. Our approach is inspired by the previously suggested connection between memory safety and noninterference, but extends that connection in a fundamentally important direction towards downgrading. We consider a low-level language with access to an allocator that provides malloc and free primitives in a flat memory model. Pointers are just integers, and as such it is trivial to write memory-unsafe programs. The basic intuition of gradual allocator independence is that of noninterference, namely that allocators must not influence program execution. This intuition is refined in two important ways that account for the allocators running out-of-memory and for programs to have pointer-to-integer casts. The key insight of the definition is to treat these extensions as forms of downgrading and give them satisfactory technical treatment using the state-of-the-art information flow machinery.