Toward a Lingua Franca for Memory Safety

By: Dimitri Racordon, Aurélien Coet, Didier Buchs

Abstract

Memory safety checking seeks to protect programs from a wide spectrum of software problems related to memory access and management, such as using unallocated or uninitialized buffers. Despite decades of research, it remains an active and fruitful research topic, as issues of scalability and adoption continue to present open challenges. A popular approach to overcome these obstacles is to rely on type checking. Types are arguably one of the most scalable techniques to reason about a program’s structural properties. They also offer a convenient tool to impose restrictions on source code, either to prohibit undesirable behaviors or to facilitate other analyses. Within the plethora of type systems that have been proposed to combat memory bugs, one recurrent trend is to leverage uniqueness and/or immutability to limit the impact of mutation, to support local reasoning. Unfortunately, bringing these properties to existing languages is often met with a deterring engineering effort. Unlike many other features and mechanisms, these are difficult to encode within a host language via simple syntactic extensions or clever meta-programming. Instead, they require a deeper understanding of the program’s semantics, which can only be obtained through preliminary analysis. This paper presents results in our effort to address this difficulty. We introduce Fuel, a compiler framework designed to guarantee uniqueness and immutability properties in arbitrary programs with explicit memory management. Fuel is centered around a source and platform agnostic low-level intermediate representation, equipped with a capability-based type system, which can be targeted by compilers for higher level languages. It is able to guarantee freedom from invalid dereference and duplicate deallocations, and offers partial support to detect memory leaks. It also advocates for the use of dynamic checks to recover static type assumptions in places where static reasoning is either impractical or impossible. We present Fuel informally through a short series of examples and formalize a subset of its intermediate language.

Keywords

Type capabilities, memory safety, aliasing, uniqueness, immutability, borrowing, compiler toolchains, intermediate languages.

Cite as:

Dimitri Racordon, Aurélien Coet, Didier Buchs, “Toward a Lingua Franca for Memory Safety”, Journal of Object Technology, Volume 21, no. 2 ( 2022), pp. 2:1-11, doi:10.5381/jot.2022.21.2.a3.