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).The formalism includes:
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.