To Memory Safety through Proofs

TL;DR

This paper introduces a novel type system based on recursive stateful views and linear logic to ensure memory safety in programs with complex pointer manipulations, supported by formalization and practical implementation.

Contribution

It formalizes a new type system rooted in ATS that guarantees memory safety for pointer-intensive programs using recursive stateful views.

Findings

Formalization of the type system for memory safety

Implementation demonstrating practicality

Examples illustrating recursive stateful views

Abstract

We present a type system capable of guaranteeing the memory safety of programs that may involve (sophisticated) pointer manipulation such as pointer arithmetic. With its root in a recently developed framework Applied Type System (ATS), the type system imposes a level of abstraction on program states through a novel notion of recursive stateful views and then relies on a form of linear logic to reason about such stateful views. We consider the design and then the formalization of the type system to constitute the primary contribution of the paper. In addition, we also mention a running implementation of the type system and then give some examples in support of the practicality of programming with recursive stateful views.