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.

翻译：空间内存安全违规仍是C程序的主要问题。Checked-C是C语言的一种安全方言，通过扩展检查指针类型和注解，以向后兼容的方式保证空间内存安全，允许混合使用检查指针和常规（未检查）指针类型。然而，未检查代码的漏洞可能破坏检查代码的空间安全性。我们提出CheckedCBox，通过将污染类型引入Checked-C类型系统，为Checked-C添加了灵活的类型导向程序划分机制。这种机制允许将程序灵活划分为检查区域和未检查区域，使得未检查区域代码不会影响检查区域的空间安全性。我们形式化了类型系统，并证明了良类型CheckedCBox程序具有无崩溃和无泄露属性。我们以可配置方式实现了CheckedCBox，从而能够利用现有沙箱机制（如WebAssembly）执行程序。通过这种方式，CheckedCBox通过高效的程序划分成功防御了四个已知漏洞。