Envs




The operational semantics for this C fragment relies on an environmen Env, that has four components:
  • A map, Mem, from addresses to values (modeling memory),
  • a map, Global, from variable names to their addresses and atomic types (modeling global variables),
  • a map, AllocMemBlock, from addresses of allocated memory blocks to size of blocks (modeling runtime memory blocks),
  • and a stack, Stack with the top of the stack, which models function frames, where each frame maps variable names to their addresses and atomic types.
minAddr and maxAddr bound the range of legal memory addresses where program data can reside. minAddr and baseAddr bound the range of global variables. Heap starts from baseAddr, and stack starts from maxAddr.

A memory Mem is defined only for addresses that have been allocated to the program by the C runtime. Our formalism axiomatizes properties of six primitive operations for accessing memory: read accessMem, write storeMem, malloc umalloc, free ufree, function frame allocation ucreateFrame, and function frame deallocation udestroyFrame.

To model the instrumentation behavior, we extend the memory model with three additional components:
  • A map, MMeta, from addresses to metadata (modeling metadata storage),
  • a map, LockTable, from LockAddr to Key (modeling lock table),
  • and a nk, which is the next key.
Each allocated location has associated metadata including a base, bound, Key, and LockAddr. A location with INVALID_KEY (0) indicates an unallocated address. The GLOBAL_KEY (1) is assigned to all global objects along with a unique gri(GLOBAL_LOCK_ADDR). Each frame frame in a stack has its own key and lock address.

CETS instruments the runtime primitives to support temporal-safety metadata. read accessMemMeta and write storeMemMeta can access or store memory with associated metadata. During allocation, malloc or createFrame assigns nk as the key, picks a free lock address for the new storage, and then increases nk. Any pointer contained in this memory area is invalidated by zeroing its metadata. At deallocation, free or destroyFrame must assign zero to the metadata of this storage. free also first ensures that the memory to deallocate is valid by checking if its key equals to the value stored in LockTable at its lock address.

Value


value is the type of contents stored in Mem.
Definition Value := nat.

Arch


The address of Mem:
Definition Loc := Value.
Stack variables are allocated from top to maxAddress; Heap variables are allocted from baseAddress to top; Global variables are allocted from minAddress to baseAddress.
Parameter minAddress : Loc.
Parameter baseAddress : Loc.
Parameter maxAddress: Loc.

Metadata


Definition Base := Loc.
Definition Bound := Loc.
Definition Key := nat.
Definition LockAddr := Loc.
Definition Meta := (Base * Bound * Key * LockAddr)%type.

Storage of metadata:
Definition MMeta := Loc -> Meta.
A table stores keys of memory:
Definition LockTable := LockAddr -> Key.
Lock address for global memory:
Parameter gri : LockAddr.

Variables


Definition Var := c_ident.

Global


Global variables are allocated from minAddress to baseAddress. Global maps each variable to its location and its atomic type.
Record Global : Set := MkGlobal
  { gdata : Var -> option (Loc*AType) }.

Definition lookUpGlobal (G: Global) (v: Var) : option (Loc*AType) :=
  G.(gdata) v.

Mem


Mem is defined as a total mapping, but the memory access primitives (accessMem and storeMem) are partial. A location that is not in the domain of these primitives is unallocated.
Definition Mem := Loc -> Value.

Heap




Heap variables are allocated from baseAddress to top. We do not define Heap explictly.

Stack


Stack variables are allocated from top to maxAddress. frame is a simplied frame, which maps variables to only atomic types, used by the well-formed syntax. uFrame is a C frame, which maps each variable to its type and location, and defines the start address and the end address of frame. All the data in uFrame are from ufrom to uto. Frame is a CETS frame with the key and lock address of this frame which are changed by ucreateFrame and udestroyFrame.

Definition frame := Var -> option AType.

Record uFrame : Set := MkuFrame
  { ufdata : Var -> option (Loc*AType);
     ufrom : Loc;
     uto : Loc
  }.

Record Frame : Set := MkFrame
  { fdata : Var -> option (Loc*AType);
     from : Loc;
     to : Loc;
     fr : Key;
     fri : LockAddr
  }.

Definition Frame2uFrame (F:Frame) :=
  MkuFrame F.(fdata) F.(from) F.(to).

Definition Frames2uFrames (Fs:list Frame) := map Frame2uFrame Fs.

Definition Frame2frame (F: Frame) : frame :=
  fun v =>
    match (fdata F v) with
    | Some (_, t) => Some t
    | None => None
    end.

Definition uFrame2frame (uF: uFrame) : frame :=
  fun v =>
    match (ufdata uF v) with
    | Some (_, t) => Some t
    | None => None
    end.

Definition lookUpFrame (F: Frame) (v: Var) : option (Loc*AType) :=
  F.(fdata) v.

Definition lookUpuFrame (uF: uFrame) (v: Var) : option (Loc*AType) :=
  uF.(ufdata) v.

Record Stack : Set := MkStack
  { frames : list Frame;
      top : Loc;
      sr : Key
  }.

Record uStack : Set := MkuStack
  { uframes : list uFrame;
      utop : Loc
  }.

Definition Stack2uStack (S:Stack) :=
  MkuStack (Frames2uFrames S.(frames)) S.(top).

Definition lookUpStack (S: Stack) (v: Var) : option (Loc*AType*Key*LockAddr) :=
  match (head (frames S)) with
  | Some F =>
    match (lookUpFrame F v) with
    | Some (l, t) => Some (l, t, F.(fr), F.(fri))
    | None => None
    end
  | None => None
  end.

Definition lookUpuStack (uS: uStack) (v: Var) : option (Loc*AType) :=
  match (head (uframes uS)) with
  | Some uF =>
    match (lookUpuFrame uF v) with
    | Some (l, t) => Some (l, t)
    | None => None
    end
  | None => None
  end.

Definition Stack2frame (S: Stack) : frame :=
    match (head (frames S)) with
    | Some F => Frame2frame F
    | None => fun v => None
    end.

Definition uStack2frame (uS: uStack) : frame :=
    match (head (uframes uS)) with
    | Some F => uFrame2frame F
    | None => fun v => None
    end.

Allocated Mem Block


AllocMemBlock stores the memory allocated via malloc, which maps the return address of malloc to the end address of this region. Only the pointers with addresses in the domain of AllocMemBlock can be deallocated via free.

Definition AllocMemBlock := Base -> option Bound.

Definition addAllocMemBlock (amb: AllocMemBlock) (b:Base) e :=
  fun (b0:Base) =>
    match (eq_nat_dec b0 b) with
    | left _ => Some e
    | right _ => amb b0
    end.

Definition removeAllocMemBlock (amb: AllocMemBlock) (b:Base) :=
  fun (b0:Base) =>
    match (eq_nat_dec b0 b) with
    | left _ => None
    | right _ => amb b0
    end.

Env


Record Env : Set := MkEnv {
  mem : Mem;
  mmeta : MMeta;
  amb: AllocMemBlock;
  global : Global;
  stack : Stack;
  revInfo : LockTable;
  rev : Key }.

Record uEnv : Set := MkuEnv {
  umem : Mem;
  uamb: AllocMemBlock;
  uglobal : Global;
  ustack : uStack }.

Definition Env2uEnv (E:Env) :=
  MkuEnv E.(mem) E.(amb) E.(global) (Stack2uStack E.(stack)).

Primitives


The specification of the primitives below is defined in Axioms.v.

Memory allocation and deallocation:
Parameter umalloc : uEnv -> Value -> option (uEnv*Base).
Parameter ufree : uEnv -> Loc -> option uEnv.

Frames allocation and deallocation:
Parameter ucreateFrame : uEnv -> frame -> option uEnv.
Parameter udestroyFrame : uEnv -> option uEnv.

Allocating a new storage in LockTable:
Reading and writing memory locations:
Parameter accessMem : Mem -> Loc-> option Value.
Parameter storeMem : Mem -> Loc -> Value -> option Mem.

Instrumented functions for CETS:
Definition addRI (RI: LockTable) ri r:=
  fun (ri0: LockAddr) =>
    match (eq_nat_dec ri0 ri) with
    | left _ => r
    | right _ => RI ri0
    end.

Definition removeRI (RI: LockTable) ri:=
  fun (ri0: LockAddr) =>
    match (eq_nat_dec ri0 ri) with
    | left _ => 0
    | right _ => RI ri0
    end.

Definition updateMetadata (mm: MMeta) (l:Loc) (me:Meta) :=
  fun (l0:Loc) =>
    match (eq_nat_dec l0 l) with
    | left _ => me
    | right _ => mm l0
    end.

Definition updateMetadatas (mm:MMeta) (from:Loc) (to:Loc) (me:Meta) :=
  fun (l:Loc) =>
    match (le_lt_dec from l) with
    | left _ =>
      match (le_lt_dec to l) with
      | left _ => mm l
      | right _ => updateMetadata mm l me l
      end
    | right _ => mm l
    end.

Definition accessMemMeta m (mm: MMeta) l :=
  match (accessMem m l) with
  | Some v => Some (v, (mm l))
  | None => None
  end.

Definition storeMemMeta m mm l d:=
  match d with
  | (v, me) =>
    match (storeMem m l v) with
    | Some m' => Some (m', updateMetadata mm l me)
    | None => None
    end
  end.

Definition validAddress (m:Mem) (l:Loc) :=
  (exists v, accessMem m l = Some v).

Definition malloc E n :=
  match (getFreshRentry (revInfo E)) with
  | Some ri =>
     match (umalloc (Env2uEnv E) n) with
     | Some (uE', b) =>
           Some (MkEnv (umem uE')
                       (updateMetadatas (mmeta E) b (b+n) (0, 0, 0, 0))
                       (uamb uE')
                       (uglobal uE')
                       (stack E)
                       (addRI (revInfo E) ri (rev E))
                       ((rev E)+1),
                 b,
                 ri)
       | None => None
       end
  | None => None
  end.

Definition free E loc :=
  match (accessMemMeta (mem E) (mmeta E) loc) with
  | Some (v, (b, e, r, ri)) =>
     match (eq_nat_dec v b) with
     | left _ =>
       match (eq_nat_dec (revInfo E ri) r) with
       | left _ =>
          match (ufree (Env2uEnv E) loc) with
          | Some uE' =>
             Some (MkEnv (umem uE')
                         (updateMetadata (mmeta E) loc (0, 0, 0, 0))
                         (uamb uE')
                         (uglobal uE')
                         (stack E)
                         (removeRI (revInfo E) ri)
                         (rev E))
         | None => None
         end
       | right _ => None
       end
     | right _ => None
     end
  | None => None
  end.

Definition createFrame E f :=
  match (getFreshRentry (revInfo E)) with
  | Some ri =>
    match (ucreateFrame (Env2uEnv E) f) with
    | Some uE' =>
       match (head (uE'.(ustack).(uframes))) with
       | Some uF => Some (MkEnv
                           (umem uE')
                           (updateMetadatas (mmeta E) uF.(ufrom) uF.(uto) (0, 0, 0, 0))
                           (uamb uE')
                           (uglobal uE')
                           (MkStack ((MkFrame
                                       uF.(ufdata)
                                       uF.(ufrom)
                                       uF.(uto)
                                       E.(rev)
                                       ri
                                     )::frames (stack E)
                            )
                            (utop (ustack uE'))
                            E.(rev)
                           )
                           (addRI (revInfo E) ri (rev E))
                           (E.(rev) + 1)
                           )
       | None => None
       end
    | None => None
    end
  | None => None
  end.

Definition destroyFrame E :=
  match (head (E.(stack).(frames))) with
  | Some F =>
     match (eq_nat_dec (revInfo E (F.(fri))) F.(fr)) with
     | left _ =>
       match (udestroyFrame (Env2uEnv E)) with
      | Some uE' =>
         let Fs := (tail (E.(stack).(frames))) in
         match (head Fs) with
         | Some F0 => Some (MkEnv (umem uE')
                                  (mmeta E)
                                  (uamb uE')
                                  (uglobal uE')
                                  (MkStack Fs (utop (ustack uE')) F0.(fr))
                                  (removeRI (revInfo E) F.(fri))
                                  (rev E))
         | None =>Some (MkEnv (umem uE')
                              (mmeta E)
                              (uamb uE')
                              (uglobal uE')
                              (MkStack Fs (utop (ustack uE')) 1)
                              (removeRI (revInfo E) F.(fri))
                              (rev E))
         end
       | None => None
       end
     | right _ => None
     end
  | None => None
  end.

WellFormedness

The safety result relies on showing that certain well-formedness invariants are maintained by the instrumented program. A well-formed environment |- Env consists of a well-formed global storage Global, which ensures that global variables are allocated with well-formed type information, a well-formed Stack, which ensures that local variables of a function are allocated at a frame with well-formed type information, and later frames are of larger key than earlier frames, well-formed allocated memory regions AllocMemBlock that must be disjoint to each other, a nk that is larger than 1, and a well-formed memory Mem. A memory Mem is well-formed when the metadata associated with each allocated location l is well-formed. If this location l is accessible, its value v with metadata b, e, k, la satisfies the properties:
  • (k < nk) /\ ((b = 0) \/ ((b <> 0) /\ (k <> 0) /\ (L(la) = k => forall b <= l < e. Mem |- l))). Here, Mem |- l is a predicate that holds when a location l is allocated in memory Mem.
  • If k is equal to the key of another accessible value, then their lock addresses are also equal. Particularly, if k is 1, la must be gri; if k is equal to the key of a frame fr, la is same as the lock address of that frame.
  • The range of global variables is within b and e if and only if k = 1 /\ la = gri. Similarly, the range of a frame on the stack is within b and e, if and only if k and la are equal to the key and lock address of that frame.
  • An allocated memory region in B is with b and e, then for any accessible value v' with metadata b', e', k', and la' that is also within this range, k <> k' => (L(la) <> k \/ L(la') <> k'); If the range of a frame on the stack is within b and e, and k is not equal to the key of that frame, then L(la) <> k.

Definition wfGlobal (G: Global) :Prop :=
  (forall v loc t,
     lookUpGlobal G v = Some (loc, t) ->
     minAddress <= loc /\ loc + sizeOfAType t <= baseAddress
  ) /\
  (forall v loc t,
     lookUpGlobal G v = Some (loc, t) ->
     (forall v' loc' t',
       lookUpGlobal G v' = Some (loc', t') ->
       loc' >= loc + sizeOfAType t \/ loc >= loc' + sizeOfAType t')
  ).

Definition wfFrameNoOverlapped (F: Frame) :Prop :=
  (forall v loc t,
     lookUpFrame F v = Some (loc, t) ->
     (forall v' loc' t',
       lookUpFrame F v' = Some (loc', t') ->
       loc' >= loc + sizeOfAType t \/ loc >= loc' + sizeOfAType t')
  )
  .

Definition wfuFrameNoOverlapped (uF: uFrame) :Prop :=
  (forall v loc t,
     lookUpuFrame uF v = Some (loc, t) ->
     (forall v' loc' t',
       lookUpuFrame uF v' = Some (loc', t') ->
       loc' >= loc + sizeOfAType t \/ loc >= loc' + sizeOfAType t')
  )
  .

Definition wfFrame (M: Mem) (RI: LockTable) (F: Frame) :Prop :=
  (forall v loc t,
     lookUpFrame F v = Some (loc, t) ->
     F.(from) <= loc /\ loc + sizeOfAType t <= F.(to) /\
     validAddress M loc
  ) /\
  wfFrameNoOverlapped F /\
  RI (F.(fri)) = F.(fr) /\ 2 <= F.(fr)
  .

Inductive wfFrms (rev:Key) : Stack -> Prop :=
  | wfFrms_nil :
      rev >= 2 ->
      wfFrms rev (MkStack nil maxAddress 1)
  | wfFrms_cons : forall Fs F r,
      wfFrms rev (MkStack Fs F.(to) r) ->
      r < F.(fr) ->
      baseAddress < F.(from) ->
      F.(from) < F.(to) <= maxAddress ->
      F.(fr) < rev ->
      wfFrms rev (MkStack (F::Fs) F.(from) F.(fr))
  .

Definition wfStack (M: Mem) (RI: LockTable) (rev:Key) (S: Stack) :=
  wfFrms rev S /\
  (forall F, In F (frames S) -> wfFrame M RI F).

Definition wfData (M: Mem) (RI : LockTable) (m:Meta) (rev: Key): Prop :=
  match m with
  | (b, e, r, ri) =>
    (r < rev) /\
         ((
           b <> 0 /\ b >= minAddress /\ b < e <= maxAddress /\
           (r <> 0) /\
           (r = (RI ri)->
            (forall i : nat,
               b <= i < e -> validAddress M i
            ))
         ) \/
         (b = 0))
  end.

Definition wfMem (M: Mem) (MM:MMeta) (RI : LockTable) (rev : Key) :Prop :=
  (forall l,
      match (accessMemMeta M MM l) with
      | Some (_, m) => wfData M RI m rev
      | _ => True
      end
   ).

Definition wfOverlapped E b e r ri :=
  (forall l' v' b' e' r' ri',
    accessMemMeta E.(mem) E.(mmeta) l' = Some (v', (b', e', r', ri')) ->
    ((b <= b' /\ b' < e) \/ (b' <=b /\ b < e')) ->
    minAddress <= b < e -> minAddress <= b' < e' ->
    r <> 0 -> r' <> 0 ->
    ((r <> r' -> E.(revInfo) ri <> r \/ E.(revInfo) ri' <> r') /\
      (r = r' -> ri = ri'))).

Definition wfStackPtr S RI b e r ri:=
  forall F,
    In F (frames S) ->
    r <> 0 ->
    minAddress <= b < e ->
    (b <= F.(from) < e \/ F.(from) <=b < F.(to)) ->
    ((r <> F.(fr) -> RI ri <> r) /\
      (r = F.(fr) -> ri = F.(fri))).

Definition wfGlobalPtr b r ri:=
  minAddress <= b < baseAddress -> r <> 0 -> r = 1 /\ ri = gri.

Definition wfNonGlobalPtr e (r:Key) :=
  r <> 0 ->
  (baseAddress < e <= maxAddress) ->
  r >= 2.

Definition wfNonStackPtr S RI b r (ri:LockAddr) :=
  r <> 0 ->
  RI ri = r ->
  (minAddress <= b < S.(top)) ->
  (forall F ,
     In F S.(frames) ->
     F.(fr) <> r
  )
  .

Definition wfAllocMemBlock M AMB S b e :=
  (baseAddress <= b < e /\ e <= S.(top)) /\
  (forall i, b <= i < e -> validAddress M i) /\
  (forall b' e',
      AMB b' = Some e' ->
      b' <> b ->
      ((b' < b /\ e' <= b)) \/ (b < b' /\ e <= b')).

Definition wfOverlappedAMB E b e r ri :=
  (forall b0 e0 l' v' b' e' r' ri',
    E.(amb) b0 = Some e0 ->
    accessMemMeta E.(mem) E.(mmeta) l' = Some (v', (b', e', r', ri')) ->
    ((b <= b0 /\ b0 < e) \/ (b0 <=b /\ b < e0)) ->
    ((b' <= b0 /\ b0 < e') \/ (b0 <=b' /\ b' < e0)) ->
    minAddress <= b < e -> minAddress <= b' < e' ->
    r <> 0 -> r' <> 0 ->
    ((r <> r' -> E.(revInfo) ri <> r \/ E.(revInfo) ri' <> r') /\
      (r = r' -> ri = ri'))).

Definition wfUniqRentryH E b e r ri :=
  (forall l' v' b' e' r' ri',
    accessMemMeta E.(mem) E.(mmeta) l' = Some (v', (b', e', r', ri')) ->
    minAddress <= b < e -> minAddress <= b' < e' ->
    r <> 0 ->
    r = r' ->
    ri = ri').

Definition wfUniqRentryGS E r ri :=
  r <> 0 ->
  (r = 1 -> ri = gri) /\
  (forall F,
    In F (frames (stack E)) ->
    r= F.(fr) -> ri = F.(fri)).

Definition wfEnv (E:Env) : Prop :=
  wfMem E.(mem) E.(mmeta) E.(revInfo) E.(rev) /\
  wfGlobal E.(global) /\
  wfStack E.(mem) E.(revInfo) E.(rev) E.(stack)/\
  (forall v loc t,
    lookUpGlobal E.(global) v = Some (loc, t) ->
    validAddress E.(mem) loc
  ) /\
  E.(rev) >= 2 /\
  E.(revInfo) gri = 1 /\
  (forall l v b e r ri,
    accessMemMeta E.(mem) E.(mmeta) l = Some (v, (b, e, r, ri)) ->
    wfOverlapped E b e r ri) /\
  (forall l v b e r ri,
    accessMemMeta E.(mem) E.(mmeta) l = Some (v, (b, e, r, ri)) ->
    wfGlobalPtr b r ri) /\
  (forall l v b e r ri,
    accessMemMeta E.(mem) E.(mmeta) l = Some (v, (b, e, r, ri)) ->
    wfStackPtr E.(stack) E.(revInfo) b e r ri) /\
  (forall l v b e r ri,
    accessMemMeta E.(mem) E.(mmeta) l = Some (v, (b, e, r, ri)) ->
    wfNonGlobalPtr e r) /\
  (forall l v b e r ri,
    accessMemMeta E.(mem) E.(mmeta) l = Some (v, (b, e, r, ri)) ->
    wfNonStackPtr E.(stack) E.(revInfo) b r ri) /\
  (forall b e,
    E.(amb) b = Some e ->
    wfAllocMemBlock E.(mem) E.(amb) E.(stack) b e) /\
  (forall l v b e r ri,
    accessMemMeta E.(mem) E.(mmeta) l = Some (v, (b, e, r, ri)) ->
    wfOverlappedAMB E b e r ri) /\
  (forall l v b e r ri,
    accessMemMeta E.(mem) E.(mmeta) l = Some (v, (b, e, r, ri)) ->
    wfUniqRentryH E b e r ri) /\
  (forall l v b e r ri,
    accessMemMeta E.(mem) E.(mmeta) l = Some (v, (b, e, r, ri)) ->
    wfUniqRentryGS E r ri).