Introduction

These are notes for the mechanized proof of a formal model for CETS. As described in our ISMM10 paper, CETS temporal safety properties can only be guaranteed if spatial safety is also enforced. The formal model builds on the prior formalization for spatial safety in SoftBound and shows that the combination completely captures both spatial and temporal safety. These claims have been mechanized using the Coq proof assistant, and all the Coq proof developments are available online.

Without obscuring the formalism with the size and complexity of the full CETS implementation, we are focused on the key components of CETS' mechanisms---metadata propagation and memory-safety checking, and a fragment of C (types and syntax) that covers almost all of CETS' features, including the address-of operator &, malloc, free, and named structure types, which permit recursive data structures. We also support a simple form of function call that has no arguments or results, but does allow stack pointers to escape via the heap. The formalism does not model CETS' checking of function pointers or capture its shrinking of bounds for detecting sub-object spatial violations.

The presentation proceeds in three steps. First, we formalize a memory model that includes global variables, heap, and stack, with axiomatization of the C runtime primitives for accessing memory: read, write, malloc, free, function frame allocation and deallocation. With these utilities we develop a non-standard operational semantics for (simplified, straight-line, and single-threaded) C programs that tracks information about which memory addresses have been allocated. Crucially, this semantics is partial---it is undefined whenever a bad C program would cause a memory-safety violation; for programs without spatial or temporal memory errors, this semantics agrees with C.

Second, we augment the operational semantics so that it both propagates the metadata and performs memory-safety assertions, aborting the program upon assertion failure, with augmented memory model and runtime primitives that manipulate metadata. This step abstractly models the results of combined spatial and temporal safety instrumentation of the C program.

Finally, we define a well-formedness predicate on syntax that captures invariants ensured by a combination of the C compiler and CETS instrumentation. Standard preservation and progress results then establish that, starting from awell-formed initial program state, the CETS instrumented version will either terminate without any memory violation, cause a system error (exhausting memory, deallocating an invalid memory, etc), or abort---it will never get stuck trying to access memory that is both spatial-safe and temporal-safe. This approach is similar to those used in both CCured's and Cyclone's formal developments. We also prove that if a CETS instrumented program terminates successfully, the original C program will not cause any memory violation. The rest of these notes explains this proof strategy in more detail.

In these notes, we use the following metavariable names:

Metavariable Names

Metavariables	Usage
a	Atomic Types
p	Pointer Types
s	Anonymous Struct Types
n	Named Struct Types
t	Types
f	Functions
lhs	LHS expressions
rhs	RHS expressions
c	Commands
G	Globals
S	Stacks
fr	Framse
x	variable
v	value
l	location
M	Memory
B	Allocated Memory Regions
E	Environments
Meta	Metadata
L, RI	lock table
nk, rev	next key
b	base
e	bound
k, r	key
la, ri	lock address
r	Evaluation Results