Outline for February 24, 2012

Reading: §8

  1. Composing deterministic, noninterference-secure systems
  2. Nondeducibility
    1. Event system
    2. Deducibly secure
    3. Composing deducibly secure systems
  3. Generalized noninterference
    1. Assumptions and nondeducibility
    2. Composing generalized noninterference systems
    3. Feedback-free systems
  4. Restrictiveness
    1. State machine model
    2. Composing restrictive systems

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