CheckedCBox: Type Directed Program Partitioning with Checked C for Incremental Spatial Memory Safety
Liyi Li, Arunkumar Bhattar, Le Chang, Mingwei Zhu, and Aravind Machiry

TL;DR
CheckedCBox enhances Checked-C with a type-directed partitioning system that isolates unchecked code, improving spatial memory safety and preventing vulnerabilities in C programs.
Contribution
It introduces a formal type system with tainted types for safe program partitioning, and implements a configurable system that prevents vulnerabilities.
Findings
Prevents four known vulnerabilities effectively.
Formal proof of safety properties for the type system.
Enables execution with sandbox mechanisms like WebAssembly.
Abstract
Spatial memory safety violation is still a major issue for C programs. Checked-C is a safe dialect of C and extends it with Checked pointer types and annotations that guarantee spatial memory safety in a backward-compatible manner, allowing the mix of checked pointers and regular (unchecked) pointer types. However, unchecked code vulnerabilities can violate the checked code's spatial safety guarantees. We present CheckedCBox, which adds a flexible, type-directed program partitioning mechanism to Checked-C, by enhancing the Checked-C type system with tainted types that enable flexible partitioning of the program into checked and unchecked regions, in a manner such that unchecked region code does not affect the spatial safety in the checked region. We formalize our type system and prove the non-crashing and non-exposure properties of a well-typed CheckedCBox program. We implemented…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Radiation Effects in Electronics · Real-Time Systems Scheduling
