M4Secure: Making Memory Management More Secure

M4Secure：让内存管理更安全

• 批准号: EP/X037525/1
• 负责人: Jeremy Singer
• 金额: $ 58.34万
• 依托单位: University of Glasgow
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FX037525%2F1
• 关键词: M4Secure; Making; Memory; Management; More

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.

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