CS5430 Homework 5: Information Flow

General Instructions. You are expected to work alone on this assignment.

Due 5/5 at 11:59pm. Late assignments will be penalized.

Submit your solution using CMS. Prepare your solution as .doc, .docx, or .pdf, as follows:


  1. An informal description of non-interference for confidentiality is

    "Changes in secret inputs do not cause changes in public outputs."

    Do the following systems satisfy this policy? Argue why or why not. Your interpretation of this informal condition may affect your answer, so the clarity and precision of your rationale is important.

    All systems have four channels: SI (secret in), SO (secret out), PI (public in), PO (public out).

    1. System U outputs on SO the sum of inputs on SI and PI, and U outputs on PO the sum of inputs on SI.

    2. System U outputs on SO the sum of inputs on PI, and U outputs on PO the same as it outputs on SO.

    3. System U outputs on PO the sum of inputs on PI only if the sum of inputs on SI is even.

    4. System U outputs outputs on PO an encrypted version of the inputs on PI using a key read from SI.

  2. The formal definition of noninterference for a program that produces state F(s) when execution is started in a state s is:
    FOR ALL stats s and s':
     states s and s' being L-equivalent
     IMPLIES
     states F(s) and F(s') are L-equivalent.
    
    Here, states involve variables that store H-values (secret information) and L-values (public information).

    Give informal and formal definitions describing a flow property for integrity that is analogous to noninterference (for confidentiality).


  3. Consider a simple programming language with the usual statements: assignment "x:= Expr", sequential composition "S1; S2; ...; Sn", conditional "if B then S1 else S2", and iteration "while B do S end". Every program variable is labeled either H (for secret) or L (for public). An attacker can read from variables with label L (but not with label H) before and after execution of every statement. For example, during execution of the statement "S1; S2; S3" the attacker can read L-variables before and after execution of S1, before and after execution of S2, as well as before and after execution of S3.

    We are interested in confidentiality.

    1. Give a formal definition of noninterference for this setup. That is, a program that satisfies your revised definition of noninterference should be one in which an attacker is prevented from learning information about values stored in variables with label H.

    2. Give an example of a program that satisfies the classical definition of noninterference (i.e., the form discussed in class) but does not satisfy your revised definition of noninterference.

    3. Is it possible for a program to satisfy the revised definition of noninterference but not satisfy the classical definition? Either give an example of such a program or explain why no example exists.

    4. Consider the following program.
      x := 0;
      y := 0;
      IF s= 1 THEN  x := 1;   y := 2
              ELSE  y := 2;   x := 1
      
      For the eight possible label assignments to s, x, and y explain whether and why the program satisfies both the classical definition of noninterference and your revised definition of noninterference.


  4. Consider the following program Pgm, where Method1 and Method2 always terminate.
    Pgm:  call Method1;
          call Method2
    

    1. If Method1 and Method2 both satisfy (classical) noninterference does that imply that Pgm does? Explain why or give a counter-example.

    2. If Pgm satisfies (classical) noninterference does that imply that Method1 does? Explain why or give a counter-example.