Pervasive Memory Safety through Ownership Types

Memory safety is an important property of a programming language or runtime environment that prevents programs from accessing or modifying memory in unintended ways, such as unauthorised or invalid pointer access, use-after-free errors, double-free errors, and buffer overflows.

Despite most popular languages being memory safe, memory safety issues still account for most of the known vulnerabilities.

The use of memory unsafe languages is primarily driven by performance needs, particularly at the low levels of the software stack.

The tension between safety and performance is critical as bugs at the lower levels can be exploited to attack software above it.

The implementation of runtime techniques for memory safety, such as garbage collection, complicates reasoning about and controlling performance.

Recent advances in compile-time memory management allow programming languages to deliver memory safety without unpredictable runtime behaviour. However, two obstacles to widespread adoption remain: expressivity and usability.

As a result, developers resort to using unsafe code to circumvent these limitations and achieve the desired functionality.The goal of this research is to advance the state of the art in memory safety, and in particular, to improve the security of programs by eliminating the need for unsafe code.

The proposed approach has the potential to benefit a wide range of applications in cybersecurity, where memory-related vulnerabilities are a significant concern.