SoftBound: Highly Compatible and Complete Spatial Memory Safety for C

SoftBound is a compile-time transformation for enforcing spatial safety of C. Inspired by our group's prior work on HardBound, a previously proposed hardware-assisted approach. SoftBound similarly records base and bound information for every pointer as disjoint metadata. This decoupling enables SoftBound to provide spatial safety without requiring changes to C source code. Unlike HardBound, SoftBound is a software-only approach and performs metadata manipulation only when loading or storing pointer values.

Source Code

Download SoftBound v1.1.1 (Second public release, released late-September 2009)

Publication

SoftBound: Highly Compatible and Complete Spatial Memory Safety for C
Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, Steve Zdancewic
In the Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2009

People

Students

Faculty

Mailing Lists

Subscribe to SoftBound announcement list - a low-volume mailing list for announcements related to SoftBound releases
Subscribe to SoftBound users list - SoftBound users mailing list to enable SoftBound users to interact, ask questions, report bugs, bug fixes, etc.
Or, you may contact the authors directly by sending email to softbound[at]cis[dot]upenn[dot]edu

Formalism of Softbounds's Safety

This is the formalism of Softbound's safety, which has been completely mechanized using the Coq proof assistant. The code runs with Coq 8.1 (Feb. 2007), 8.1pl3 (Dec. 2007) and 8.2beta4 (Aug. 2008).

The formalism includes:

A non-standard operational semantics for C programs. This semantics tracks information about which memory addresses have been allocated and the (run-time) types of values. Crucially, this semantics yields an "error" state whenever a bad C program would cause a spatial-safety violation. The approach adopted is similar to CCured's formalism, but the C language considered here includes the address-of operator & and a named structure type to define recursive types.
A predicate that models the invariants of stack and memory enforced by the Softbound instrumentation and meta-data propagation process.
A proof about the preservation and progress (safety) of the type system.

The code in softbound-proof.tgz is the formalism of softbound. The code in softbound-proof++.tgz defines and proves a system more than the implementation of softbound. Softbound has only one sort representation of pointers with the base and bound metadata information. This formalism also contains a SAFE pointer and a SEQ pointer, which are similar to CCured's pointer categories. SAFE pointers are not involved in any pointer arithmetic and in casts. SEQ pointers are not involved in any casts. The pointer representation of Softbound is called TAME pointer in this proof. TAME pointers can be involved in any pointer atithmetic and in casts. The proof proves the safety of a system more complicated than Softbound. The system defaults to Softbound if all pointers are TAME pointers.