Outline for May 17, 2013

Reading: §17.2–17.3, 33, [SMB06] (This is available in the Resources area of SmartSite; look in the folder “Handouts”)
Due: Homework #4, due May 24, 2013

1. Isolation: virtual machines
   1. What it is
   2. Example: KVM/370
   3. Example: VAX/VMM
2. Isolation: sandboxes
   1. What it is
   2. Adding mechanisms to libraries or kernel
   3. Modify program or process to be executed
   4. Example: Janus
3. Covert channels
   1. Storage vs. timing
   2. Noise vs. noiseless
   3. Existence
   4. Bandwidth
4. Covert channel detection
   1. Noninterference
   2. Shared Resource Matrix Model
   3. Information flow analysis
   4. Covert flow trees
5. Noninterference
   1. Version of the Unwinding Theorem
   2. Specifications of SAT
   3. Example analysis for SAT
6. Shared resource matrix methodology
   1. Identify shared resources, attributes
   2. Operations accessing those attributes
   3. Building the matrix
   4. Issues about the methodology
7. Covert flow trees
   1. What it is
   2. Node types
   3. Construction
      1. Determine what attributes primitive operations reference, modify, return
      2. Locate covert storage channel that uses some attribute
      3. Construct lists: sequences of operations that modify, recognize modifications
   4. Analysis
8. Capacity and noninterference
   1. When is bandwidth of covert channel 0?
   2. Noninterference sufficient but not necessary
   3. Analysis
   4. Measuring capacity
9. Mitigating covert channels
   1. Preallocation and hold until process terminates
   2. Impose uniformity
   3. Randomize resource allocation
   4. Efficiency/performance vs. security