M4Secure: Making Memory Management More Secure

Memory management is an essential feature of computing software. During execution time, a program will frequently call a memory allocator library to request space on the computer memory to store data. Unfortunately, memory management systems are vulnerable. According to recent studies from Microsoft and Google, memory bugs account for 70% of critical software vulnerabilities, which can crash our important IT infrastructures and leak confidential and personal data. Such problems are frequently caused by (mis)management of dynamically allocated memory. At the same time, memory allocation is also significant for performance. A large proportion of program execution time is devoted to memory management routines.

The hardware industry responds to severe memory vulnerabilities by adding secure extensions to mainstream processor families. These new hardware facilities provide fundamental mechanisms for more secure memory allocators. Still, their full benefits are yet to be seen due to the massive developer effort required to write or optimise a memory management codebase and the further effort to re-target the code to new architectures. For example, the state-of-the-art snmalloc secure memory allocator comprises 25,000 lines of code painstakingly developed by leading industrial practitioners over four years. Yet, it only supports a small set of hardware security features.

A crisis is looming - without a solution, either hardware innovation in security mechanisms will stall as software cannot fit, or we will have to continue to suffer from frequent security issues due to memory bugs. Such a crisis requires us to fundamentally rethink how we implement memory management libraries.

This project will develop an entirely new way to build memory allocators. It aims to massively reduce human involvement in developing and optimising memory management libraries to target a diverse range of hardware architectures. Our approach involves specifying the required memory management attributes and then synthesising performant memory management code to satisfy these specifications. Our approach ensures such code is correct by construction by using model-checking techniques to verify the generated code match the expected behaviour and enhanced security requirements. Further, we will support a range of processor backends featuring recently proposed novel secure extensions for hardware architectures.

Our work is enabled by the recent advance in deep learning for code generation and formal methods for modelling large-scale software systems. The recent breakthrough of ML in generating new and better matrix multiplication implementation and its demonstrated effectiveness in game playing, natural language processing and autonomous systems gives us the confidence that it is now possible to generate correct and performant memory management libraries. If AI can learn to drive a car, it must be able to reason about carefully designed security properties and primitives to generate memory allocator code.

This ambitious project, if successful, will have a transformative impact on how we design memory management libraries. Our software prototype will be open-sourced and be applied to real-life applications. Given the accelerated and disrupted changes in hardware security design and the massive mismatch between software and hardware, success in this project will be of interest to companies that provide hardware IP and software development tools, two areas in which the UK is world-leading. It will also help reduce the number of memory-related bugs and improve application performance so that the general public can benefit from more secure and efficient computer systems.

We believe we have the team, partners and work plan to achieve the ambitious goal. We are ideally placed to carry out the proposed research, possessing key skills in the primary research areas of memory management, formal verification and ML-based code synthesis and optimisation.