一句话：提出基于静态分析的半自动移植工具 3C，为遗留 C 程序推断 Checked C 检查指针类型与数组边界注解。
针对 C/C++ 中缓冲区溢出等空间安全违规，Checked C 以带边界检查的 checked 指针类型实现渐进式空间安全，兼容遗留指针并支持增量改造，但遗留程序移植仍需大量人工。本文提出以 3C 为核心的半自动移植流程：3C 是基于静态分析的注解工具，利用 typ3c 和 boun3c 两种新算法将遗留指针推断为 checked 指针，并为所需指针推断数组边界注解；它还进行根因分析，引导开发者重构代码，之后可重跑以推断更多注解。在 11 个共 319KLoC 的程序上，3C 能有效推断 checked 指针类型；结合人工重构的移植经验表明其效果良好。
Owing to the continued use of C (and C++), spatial safety violations (e.g., buffer overflows) still constitute one of today's most dangerous and prevalent security vulnerabilities. To combat these violations, Checked C extends C with bounds-enforced checked pointer types. Checked C is essentially a gradually typed spatially safe C - checked pointers are backwards-binary compatible with legacy pointers, and the language allows them to be added piecemeal, rather than necessarily all at once, so that safety retrofitting can be incremental. This paper presents a semi-automated process for porting a legacy C program to Checked C. The process centers on 3C, a static analysis-based annotation tool. 3C employs two novel static analysis algorithms - typ3c and boun3c - to annotate legacy pointers as checked pointers, and to infer array bounds annotations for pointers that need them. 3C performs a root cause analysis to direct a human developer to code that should be refactored; once done, 3C can be re-run to infer further annotations (and updated root causes). Experiments on 11 programs totaling 319KLoC show 3C to be effective at inferring checked pointer types, and experience with previously and newly ported code finds 3C works well when combined with human-driven refactoring.
@article{paperbot1534,
title = {C to checked C by 3c},
author = {Aravind Machiry and John Kastner and Matt McCutchen and Aaron Eline and Kyle Headley and Michael Hicks},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA1},
year = {2022},
doi = {10.1145/3527322}
}