Jeremy Singer (University of Glasgow), Alice Miller (University of Glasgow) and Zheng Wang (University of Leeds)
Memory bugs are a major cause of application security vulnerabilities, making up 70% of critical software flaws, often resulting from mismanagement of dynamic memory. Effective memory allocation is essential for efficient execution, as a significant portion of program execution time deals with low-level memory management. Hence memory allocation is vital for both security and performance.
Recent hardware innovations, such as secure CPU extensions, offer improved security by preventing various hacker exploits. However, leveraging these innovations currently requires extensive software developer effort.
The M4Secure project will create an open-source framework for customisable memory management libraries that meet formal user requirements for security and performance. Instead of labour-intensive manual development, M4Secure will develop an automated approach that synthesizes efficient memory management code based on specified attributes, including security properties. The project will ensure code correctness through the application of model-checking techniques, accommodating a wide range of processor architectures, including hardware security features like Arm Memory Tagging Extension (MTE), CHERI capabilities, and Intel Control-flow Enforcement Technology (CET).
A key enabling technology of M4Secure is the combination of deep learning and formal verification techniques to generate memory allocator code to match security specifications, guaranteeing correctness and security. This strongly aligns with the research vision of VeTSS by developing techniques to model hardware security features and reason about software behaviour. This work will provide novel scientific methods and a new, exciting application domain to support the development of trustworthy and high-performance software systems through verification and deep learning techniques.