SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Thu 8 Dec 2022 10:30 - 11:00 at Seminar Room G007 - Assurance Chair(s): Amal Ahmed

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.

Thu 8 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
AssuranceOOPSLA at Seminar Room G007
Chair(s): Amal Ahmed Northeastern University, USA
10:30
30m
Research paper
C to checked C by 3cDistinguished Paper
OOPSLA
Aravind Machiry Purdue University, John Kastner Amazon, Matt McCutchen , Aaron Eline Amazon, Kyle Headley Amazon, MIchael Hicks Amazon
DOI
11:00
30m
Talk
Solo: A Lightweight Static Analysis for Differential Privacy
OOPSLA
Chike Abuah University of Vermont, David Darais Galois, Joseph P. Near University of Vermont
DOI
11:30
30m
Talk
MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types
OOPSLA
Lionel Parreaux Hong Kong University of Science and Technology, Chun Yin Chau The Hong Kong University of Science and Technology
DOI Pre-print Media Attached File Attached