Outline for May 6, 2013

Reading: §8.2–8.5, [Man02] (This is available in the Resources area of SmartSite; look in the folder “Handouts”)
Due: Homework #3, due May 10, 2013
  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
  4. Access Control Matrix interpretation
    1. Model
    2. ACM conditions
    3. Policy conditions
    4. Result
  5. Policies that change over time
    1. Generalization of noninterference
    2. Example
  6. Composing deterministic, noninterference-secure systems

Table of Notation

notation   meaning
S   set of subjects s
Σ   set of states σ
O   set of outputs o
Z   set of commands z
C   set of state transition commands (s, z), where subject s executes command z
C*   set of possible sequences of commands c0, …, cn
ν   empty sequence
cs   sequence 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 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
You can also obtain a PDF version of this. Version of May 6, 2013 at 10:19PM