一句话：提出 MSA 框架，用 LLM 结合轻量静态分析将 C 代码移植到 CheckedC，自动推断注解并重构代码。
C 等底层语言中的内存安全违规仍是软件漏洞的主要来源。通过将 C 代码移植到安全的 C 方言可从构造上消除此类违规，但该过程需要程序员手动推断注解并可能重构代码，负担沉重，因而采用有限。本文利用大语言模型（LLM）同时应对注解推断与代码重写两个问题，挖掘 LLM 进行复杂代码推理和大规模代码库重写的能力，并提出一种新颖的整体程序变换框架：借助轻量静态分析将变换分解为更小的步骤，使 LLM 能够有效完成。作者实现了面向 CheckedC 方言的工具 MSA，并在多个微基准以及高达 2 万行的真实代码上评估。结果表明，MSA 优于朴素 LLM 基线，并且相比最先进的符号（非 LLM）技术也有提升。
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.
DOI 原文 ·
@inproceedings{paperbot8794,
title = {LLM Assistance for Memory Safety},
author = {Nausheen Mohammed and Akash Lal and Aseem Rastogi and Rahul Sharma and Subhajit Roy},
booktitle = {ICSE},
year = {2025},
doi = {10.1109/icse55347.2025.00023}
}