Formalism of Softbound+CETS's Safety

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

• 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 safety violation. The approach adopted is similar to CCured's formalism, but the C language considered here includes the address-of operator &, a named structure type to define recursive types, 'free' and a simple form of function call that has no arguments or results, but does allow stack pointers to escape via the heap.
• A predicate that models the invariants of memory (global+heap+stack) enforced by the Softbound+CETS instrumentation and meta-data propagation process.
• A proof about the preservation and progress (safety) of the type system.

Technical Report

Code:

• The code in softbound+cets.tgz is the formalism of Softbound+CETS.
• The code in softbound.tgz is the formalism of Softbound.
• README

Publication:

• CETS: Compiler Enforced Temporal Safety for C
  Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin and Steve Zdancewic
  To appear in the proceedings of International Conference on Memory Management (ISMM 2010), June, 2010
• SoftBound: Highly Compatible and Complete Spatial Memory Safety for C
  Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin and Steve Zdancewic
  In the Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2009

NOTE: The code in softbound++.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 arithmetic 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.