SoftBound + CETS: Complete and Compatible Full Memory Safety for C

SoftBound and CETS are compile-time transformations for enforcing spatial safety and temporal safety for C. Together, SoftBound + CETS provide full memory safety for C. The key features are SoftBound + CETS are (1) use of pointer based checking with bounds and identifier metadata with every pointer, (2) use of disjoint metadata for pointers in memory, and (3) metadata propagation and manipulation only with pointer values leveraging the intermediate representation (IR) type information in LLVM. Defining pointer based checking in the LLVM IR reduces the overhead of such pointer based checking significantly.

Source Code



Mailing Lists

Formalism of CETS+SoftBound's Safety

This is the formalism of CETS+SoftBound's memory safety, completely mechanized usign Coq proof assistant. A detailed report about the proof is avaliable here
Entire source code of CETS+SoftBound's proof of memory safety is available here

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:

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.