Outline for February 17, 2012

Reading: §8.2

  1. Deterministic noninterference
    1. Model of system
    2. Example
    3. Relationship of output to states
    4. Projections and purge functions
  2. Alternative definition of security policy
    1. Output-consistent
    2. Security policy
    3. Alternate projection function
    4. Noninterference-secure with respect to the policy $r$
  3. Unwinding Theorem
    1. Locally respects
    2. Transition-consistent
    3. Unwinding theorem

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
A PDF version is available here.
UC Davis sigil
ECS 235B, Foundations of Computer and Information Security
Winter Quarter 2012