!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
SoftBound/CETS Webpage
Redirects to the SoftBound/CETS web page.
SoftBound + CETS: Complete and Compatible Full Memory Safety for C
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
Publication
- Formalizing the LLVM Intermediate Representation for Verified Program Transformations
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic
In the Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), January, 2012
- CETS: Compiler Enforced Temporal Safety for C
Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, Steve Zdancewic
In the Proceedings of International Symposium on Memory Management (ISMM), June 2010
- 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
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:
- 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.