Outline for February 22, 2012

Reading: §8.2, 8.3

  1. Unwinding Theorem
    1. Locally respects
    2. Transition-consistent
    3. Unwinding theorem
  2. Access Control Matrix interpretation
    1. Model
    2. ACM conditions
    3. Policy conditions
    4. Result
  3. Policies that change over time
    1. Generalization of noninterference
    2. Example

Table of Notation

notation   meaning
Sset of subjects s
Σ set of states σ
Oset of outputs o
Zset of commands z
Cset of state transition commands (s, z), where subject s executes command z
C*set of possible sequences of commands c0, ..., cni
νempty sequence
cssequence of commands
T(c, σi)resulting state when command c is executed in state σi
T*(cs, σi)resulting state when command sequence cs is executed in state σi
P(c, σi)output when command c is executed in state σi
P*(cs, σi)output resulting state when command sequence cs is executed in state σi
proj(s, cs, σi)set of outputs in P*(cs, σi) that subject s is authorized to see
πG,A(cs)subsequence of cs with all elements (s, z), s ∈ G and z ∉ A deleted
dom(c)protection domain in which c is executed
∼dom(c)equivalence relation on system states
π′d(cs)analogue to π above, but with protection domain and subject included
wnv1, …, vn where v1 ∈ C*
wsequence of elements of C leading up to current state
cando(w, s, z)true if s can execute z in current state
pass(s, z)give s right to execute z
prev(w_n)wn−1
last(w_n)vn
A PDF version is available here.
UC Davis sigil
ECS 235B, Foundations of Computer and Information Security
Winter Quarter 2012