一句话：将寻找正确 free 语句集合归约为精确覆盖问题，自动修复 C 程序中的内存释放错误，并保证不引入新错误。
C 程序依赖手动内存管理，开发者常因未能正确释放内存对象而引入内存泄漏、双重释放和释放后使用等错误。MemFix 提出一种自动修复技术，其核心洞见是：寻找一组能够正确释放所有已分配对象、且不引发双重释放和释放后使用的 free 语句，等价于求解由一种 typestate 静态分析变体导出的精确覆盖（exact cover）问题。作者形式化描述了该技术，并在开源程序上开展实验，表明 MemFix 能够修复真实存在的内存释放错误。由于该方法建立在可靠（sound）的静态分析之上，所生成的补丁保证修复原有错误，且不会引入新的错误。
We present MemFix, an automated technique for fixing memory deallocation errors in C programs. MemFix aims to fix memory-leak, double-free, and use-after-free errors, which occur when developers fail to properly deallocate memory objects. MemFix attempts to fix these errors by finding a set of free-statements that correctly deallocate all allocated objects without causing double-frees and use-after-frees. The key insight behind MemFix is that finding such a set of deallocation statements corresponds to solving an exact cover problem derived from a variant of typestate static analysis. We formally present the technique and experimentally show that MemFix is able to fix real errors found in open-source programs. Because MemFix is based on a sound static analysis, the generated patches guarantee to fix the original errors without introducing new errors.
DOI 原文 ·
@inproceedings{paperbot4622,
title = {MemFix: static analysis-based repair of memory deallocation errors for C},
author = {Junhee Lee and Seongjoon Hong and Hakjoo Oh},
booktitle = {FSE},
year = {2018},
doi = {10.1145/3236024.3236079}
}