DSLs, Annotations, and Dynamic Instrumentation: Specifying the Memory Layout of a Memory Manager to Detect Bugs with Typestate

Abstract

Thesis Defense:

In this talk I present the design, implementation, and study the efficacy of three interrelated tools for debugging memory safety errors in modern memory management algorithms. First is the design and implementation of the core semantics of Floorplan, a domain-specific language for describing the memory layout of a heap, targeting memory managers written in Rust. The key factor was to provide rich grammatical layout constructs which can compile to idiomatic and identically performant memory management code. Second, I reconfigured Floorplan to target C/C++ memory management code with a focus on building a typestate-based dynamic memory safety analysis toolchain called Permchecker. Permchecker’s annotation, instrumentation, and dynamic checking facilities allow for the systematic application of Floorplan typestates to legacy and new memory managers alike. Finally, I formalize a class of typestate assertions capable of detecting a broader class of memory safety errors than with Permchecker alone. These assertions use a novel subtypestate relation, similar to a subtyping relation, to detect allocation hierarchy violations. I show that in practice hierarchy violations include the most difficult to diagnose memory corruption errors, colloquially known as “memory stomping”.

Join meeting via Zoom:https://tufts.zoom.us/j/95330175375

Password: see colloquium email

Dial-in option not available.