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), sG and zA 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 v1C*
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

A PDF version is available here.
UC Davis sigil
ECS 235B, Foundations of Computer and Information Security
Winter Quarter 2012