Outline for May 11, 2000

1. Greetings and felicitations!
   1. Worm in restricted area
2. Confinement problem
   1. Legitimate channels
   2. Storage channels
   3. Covert channels
3. Covert channels
   1. What are they; note probabilistic distribution
   2. Storage vs. timing; give examples
   3. Resource matrix
   4. Formal methods
4. Information flow
   1. Deals with right to disseminate information.
   2. Assume lattice-structured information flow policy (à la BLP); represent as (SC, ≤)
   3. Explicit vs. implicit information flows
5. Program statements; define when "secure"
   1. assignment
   2. compound
   3. alternation
   4. iteration
   5. function call
   6. goto; control flow graph and immediate forward dominator (first block that lies on all paths from the block under consideration and the exit)
   7. composition of above; show compile/parse tree
6. Give examples (copy)
7. Execution-Based with Fixed Classes
   1. verify flows at times of explicit assignment to object
   2. cannot report attempted security violations
8. Execution-Based with Variable Classes
   1. Change variable's class to allow flow
   2. Fails for implicit
9. Compiler-Based Mechanisms
   1. assures secure execution of each statement
   2. may reject secure mechanisms (not precise)
   3. procedures
   4. arrays
   5. gotos (blocks)
   6. errors

Examples of Compiler-Based Information Flow Enforcement Mechanisms

Here are some examples.

copy2

procedure copy2(x: integer class {x};
             var	y: integer class {x});
    "copy x to y"
    var z: integer class {x});
    begin
        z := 1;                    Low <= z
        y := -1;                   Low <= y
        while z = 1 do             z <= glb(y, z)
            begin
                y := y + 1;        y <= y
                if y = 0           y <= z
                    then z := x    x <= z
                    else z := 0	   Low <= z
            end
    end
end copy2.

copy2 with goto

procedure copy2(x: integer class {x};
             var y: integer class {x});
    "copy x to y"
    var z: integer class {x});
    begin
----------------------------------------------
1:  z := 1;                     b1
    y := -1;
----------------------------------------------
2:  if z = 1 then goto 6;      b2
----------------------------------------------
3:  y := y + 1;                 b3
    if y = 0 then goto 5;
----------------------------------------------
4:  z := x;                     b4
    goto 2;
----------------------------------------------
5:  z := 0;                     b5
    goto 2;
----------------------------------------------
6:  end
end copy2.

IFD(b₁) = b₂
IFD(b₂) = b₆
IFD(b₃) = IFD(b₄) = IFD(b₅) = b₂