论文标题

C到3C检查C

C to Checked C by 3C

论文作者

Machiry, Aravind, Kastner, John, McCutchen, Matt, Eline, Aaron, Headley, Kyle, Hicks, Michael

论文摘要

由于继续使用C(和C ++),因此违反空间安全性(例如缓冲区溢出)仍然构成了当今最危险和最普遍的安全漏洞之一。为了应对这些违规行为,检查的C扩展了C延长C限制的检查指针类型。检查的C本质上是一种逐渐键入的空间安全的C-检查指针与传统指针兼容,并且该语言允许它们零散地添加,而不必一次添加所有语言,因此安全改装可以逐步添加。本文提出了一个半自动化的过程,用于将传统C程序移植以检查C. C.该过程以3C为中心,这是一种基于静态分析的注释工具。 3C使用两种新颖的静态分析算法-YTYP3C和BOUN3C-以注释遗产指针作为检查指针,并推断需要对需要它们的指针的阵列界限。 3C执行根本原因分析,将人类开发人员引导到应重构的代码。完成后,可以重新运行3C来推断进一步的注释(并更新的根本原因)。总计319Kloc的11个程序的实验显示3C可以有效地推断检查的指针类型,并且与以前的新移植代码相结合时,与以前的新移植代码相结合时,3C可以很好地工作。

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.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源