CheckedCBox: Type Directed Program Partitioning with Checked C for Incremental Spatial Memory Safety

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 CheckedCBox in a configurable manner, which enables us to use existing sandbox mechanisms (eg WebAssembly) to execute programs. Consequently, in doing so, CheckedCBox has prevented four known vulnerabilities by efficiently partitioning the program.