M4Secure: Making Memory Management More Secure

内存管理是计算软件的一个基本特征。在执行期间，程序将经常调用内存分配器库来请求计算机内存上的空间来存储数据。不幸的是，内存管理系统是脆弱的。根据微软和谷歌最近的研究，内存漏洞占关键软件漏洞的70%，这些漏洞可能导致我们重要的IT基础设施崩溃，泄露机密和个人数据。这些问题通常是由动态分配内存的管理（错误）引起的。同时，内存分配对性能也很重要。程序执行时间的很大一部分用于内存管理例程。硬件行业通过向主流处理器系列添加安全扩展来应对严重的内存漏洞。这些新的硬件设施为更安全的内存分配器提供了基本机制。尽管如此，由于编写或优化内存管理代码库需要大量开发人员的努力，以及将代码重新定位于新架构的进一步努力，它们的全部好处尚未得到体现。例如，最先进的smallloc安全内存分配器包含25,000行代码，这些代码是由领先的行业从业者在四年多的时间里精心开发的。然而，它只支持一小部分硬件安全特性。危机正在逼近——如果没有解决方案，要么安全机制的硬件创新将因软件无法适应而停滞不前，要么我们将不得不继续忍受由于内存错误而频繁出现的安全问题。这种危机要求我们从根本上重新思考如何实现内存管理库。这个项目将开发一种全新的方式来构建内存分配器。它旨在大规模减少开发和优化内存管理库的人力投入，以适应各种硬件架构。我们的方法包括指定所需的内存管理属性，然后综合性能内存管理代码来满足这些规范。我们的方法通过使用模型检查技术来验证生成的代码是否符合预期的行为和增强的安全需求，从而确保这些代码是正确的。此外，我们将支持一系列处理器后端，这些后端具有最近提出的针对硬件架构的新颖安全扩展。我们的工作得益于最近在代码生成的深度学习和大型软件系统建模的形式化方法方面的进展。最近机器学习在生成新的更好的矩阵乘法实现方面的突破，以及它在游戏、自然语言处理和自治系统中的有效性，使我们有信心现在可以生成正确和高性能的内存管理库。如果人工智能能够学会驾驶汽车，它必须能够对精心设计的安全属性和原语进行推理，以生成内存分配器代码。这个雄心勃勃的项目如果成功，将对我们如何设计内存管理库产生革命性的影响。我们的软件原型将是开源的，并应用于现实生活中的应用。鉴于硬件安全设计的加速和中断变化以及软件和硬件之间的巨大不匹配，该项目的成功将对提供硬件IP和软件开发工具的公司感兴趣，英国在这两个领域处于世界领先地位。它还将有助于减少与内存相关的错误数量，提高应用程序性能，从而使公众能够从更安全、更高效的计算机系统中受益。我们相信我们有团队、合作伙伴和工作计划来实现这一雄心勃勃的目标。我们有理想的位置来进行拟议的研究，拥有在内存管理，形式验证和基于ml的代码合成和优化的主要研究领域的关键技能。

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.