LLM Assistance for Memory Safety

Memory safety violations in low-level code, written in languages like C, continues to remain one of the major sources of software vulnerabilities. One method of removing such violations by construction is to port C code to a safe C dialect. Such dialects rely on programmer-supplied annotations to guarantee safety with minimal runtime overhead. This porting, however, is a manual process that imposes significant burden on the programmer and, hence, there has been limited adoption of this technique. The task of porting not only requires inferring annotations, but may also need refactoring/rewriting of the code to make it amenable to such annotations. In this paper, we use Large Language Models (LLMs) towards addressing both these concerns. We show how to harness LLM capabilities to do complex code reasoning as well as rewriting of large codebases. We also present a novel framework for whole-program transformations that leverages lightweight static analysis to break the transformation into smaller steps that can be carried out effectively by an LLM. We implement our ideas in a tool called MSA that targets the CheckedC dialect. We evaluate MSA on several microbenchmarks, as well as real-world code ranging up to 20K lines of code. We showcase superior performance compared to a vanilla LLM baseline, as well as demonstrate improvement over a stateof-the-art symbolic (non-LLM) technique. • We present MSA, the first LLM-based assistant for porting C to Checked-C. MSA performs transformations that are out-of-reach of existing (symbolic-only) assistants. • We present a novel recipe for breaking a whole program transformation into smaller tasks that can fit into LLM prompts. • We evaluate MSA on real world C-programs, ranging up to 20K lines of code, showing that it can successfully infer 86% of the required annotations correctly. We plan to open-source the implementation of MSA, along with all the prompt templates that it uses. 1 The rest of this paper is organized as follows. Section II provides a background on Checked C, followed by examples that illustrate the challenges of the porting process from C code. Section III provides background on the state-of-the-art symbolic tool for Checked C inference. Our technical contributions follow next. We provide our generic recipe for whole program transformations using LLMs (Section IV) and then we show how MSA instantiates this recipe to overcomes the challenges in the porting process (Section V). We evaluate MSA (Section VI), discuss threats to validity (Section VII), and survey related work (Section VIII).