  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.
