Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Enabling Memory Safety of C Programs using LLMs

Nausheen Mohammed, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma

TL;DR

The paper introduces MSA, a tool that blends symbolic analysis with Large Language Models to port C code to Checked-C, aiming to achieve memory-safety with minimal runtime overhead. It presents a general, dependency-graph–driven framework for whole-program transformations and implements three transformation passes (replacing nested arrays with structs, inferring bounds, and annotating globals/struct fields). Evaluations on benchmarks and real-world code show substantial annotation recovery (about $86\%$) and practical end-to-end porting effort on vsftpd, outperforming purely symbolic baselines. The work demonstrates that LLMs can handle complex refactoring and annotation reasoning when guided by static analysis, suggesting broader applicability to formal verification tasks.

Abstract

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 micro-benchmarks, 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 state-of-the-art symbolic (non-LLM) technique.

Enabling Memory Safety of C Programs using LLMs

TL;DR

The paper introduces MSA, a tool that blends symbolic analysis with Large Language Models to port C code to Checked-C, aiming to achieve memory-safety with minimal runtime overhead. It presents a general, dependency-graph–driven framework for whole-program transformations and implements three transformation passes (replacing nested arrays with structs, inferring bounds, and annotating globals/struct fields). Evaluations on benchmarks and real-world code show substantial annotation recovery (about ) and practical end-to-end porting effort on vsftpd, outperforming purely symbolic baselines. The work demonstrates that LLMs can handle complex refactoring and annotation reasoning when guided by static analysis, suggesting broader applicability to formal verification tasks.

Abstract

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 micro-benchmarks, 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 state-of-the-art symbolic (non-LLM) technique.
Paper Structure (17 sections, 10 figures, 3 tables, 1 algorithm)

This paper contains 17 sections, 10 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Challenges in porting C to Checked C
  3. Background on symbolic inference with 3C
  4. Whole-program transformation with LLMs
  5. Dependency Graph Generation
  6. Generic Whole-Program Transformation
  7. MSA Design and Implementation
  8. Replacing Nested Arrays with Structs
  9. Inferring Bounds Annotations
  10. Annotating Globals and Struct Fields
  11. Evaluation
  12. Benchmarking the MSA algorithm
  13. Inferring annotations in real-world codebases
  14. vsftpd: End-to-end case study
  15. Threats to Validity
  16. ...and 2 more sections

Figures (10)

  • Figure 1: Example of a dependency graph
  • Figure 2: Prompt template for Whole-Program Transformation
  • Figure 3: Workflow of porting C code to Checked C with MSA.
  • Figure 4: Task description for replacing nested arrays with structs
  • Figure 5: An example of the transformation ("From" to "To") for nested arrays that is provided to the LLM. The code comments are included as well.
  • ...and 5 more figures