CS 5430 Homework 4: Information Flow

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

Due Thursday, March 17, 5pm. No late assignments will be accepted.

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

• Use 10 point or larger font.
• Start each problem's solution on a new page.
• Use at most 1 page per problem.

Problem 1: Noninterference

The security policy noninterference for confidentiality can be informally stated as,

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

(In lecture, we referred to this policy simply as noninterference.) 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. You may assume that covert channels (e.g., timing and termination) are unobservable; or equivalently, that these channels are allowed to leak information. All systems have four channels: SI (secret in), SO (secret out), PI (public in), PO (public out).

1. System U copies all input from SI to SO, from PI to PO, and additionally echoes all data from PI to SO.
2. After receiving an input x on SI and an input y on PI, system V outputs y on PO if x is even, or y^y on PO if x is odd, where ^ denotes string concatenation.
3. Upon receiving plaintext x on SI, such that |x|=32 where |x| is the length of x in bits, system W generates a uniformly random number k such that |k|=32, then outputs x XOR k on PO.
4. System X receives plaintext m on SI and RSA public key K on PI, then outputs the RSA encryption of m with K—that is, m^e mod n, where K=(e,n)—on PO.

Problem 2: Type System

1. The assignment rule has "Γ(x) = τ" as a premise (i.e., an assumption). Suppose we replaced that premise with "Γ ⊢ x : τ exp", so that the resulting rule were:

   Γ ⊢ x : τ exp      Γ ⊢ e : τ exp

   Γ ⊢ x:=e : τ cmd

   Unfortunately, this rule is broken: with it, the type system would no longer enforce noninterference (for confidentiality). Exhibit an example program, and corresponding proof tree, that is accepted by the type system with this broken rule, but not by the original type system, such that the program violates noninterference.
2. The rule for arithmetic and Boolean expressions (named OP in the handout distributed in class) can be used to type check many arithmetic expressions, including addition, subtraction, etc., and ensure that those expressions satisfy noninterference when used as part of a program. Can the OP rule be used to securely type-check division? Why or why not?
3. The subtyping rule for commands includes the premise τ' ≤ τ. Suppose that this premise were changed to τ ≤ τ', which is the same premise that is used in the subtyping rule for expressions. Would the type system still enforce noninterference? Why or why not?

Problem 3: Arrays

In class, we built a type system that enforced noninterference for confidentiality. The programming language we used was very simple. Suppose we add heap-allocated arrays (as in Java) to that language. So, we may have assignment statements of the following forms:

  a[i] := j;
     j := a[i];
     a := b;

In the final statement above, a and b are both arrays. The effect of the statement is to cause both a and b to refer to the same array on the heap; that is, the array is aliased by a and b. Thus, if "a := b; b[j] := i;" is executed, then both a[j] and b[j] will be equal to i. Assume throughout this problem that all array indices are always within bounds.

1. Examine the following three statements. Explain which statements satisfy noninterference, which don't, and why. Variables c, d, e, and f are arrays; m, n, o, and p are integers. Assume that typing context Γ assigns types to variables as follows: Γ(c) = Γ(f) = Γ(p) = S, and Γ(d) = Γ(e) = Γ(m) = Γ(n) = Γ(o) = P, where S denotes secret and P denotes public.

   1. c[m] := n;
   2. o := d[p];
   3. e := f;

2. Suppose we add arrays to our programming language. We now allow expressions to include array element selection a[e], and we allow assignment to array elements, as in a[e1] := e2. The three rules given below are perhaps the most obvious type system rules we could use to type check information flow for arrays. The first rule shows how to type check array element selection expressions. The second rule is our standard assignment rule, unchanged. But note that expression e could now include array element selection. Also note that variables may now be arrays or scalars (i.e., non-arrays). In the second rule, x may be either an array variable or a scalar variable, but (of course) it may not be an array element selection. The third rule shows how to type check assignment to array elements. In it, a must be an array.

   Γ(a) = τ         Γ ⊢ e : τ exp		Γ(x) = τ         Γ ⊢ e : τ exp		Γ(a) = τ         Γ ⊢ e1 : τ exp         Γ ⊢ e2 : τ exp
   Γ ⊢ a[e] : τ exp		Γ ⊢ x := e : τ cmd		Γ ⊢ a[e1] := e2 : τ cmd

   Unfortunately, these rules do not enforce noninterference. Exhibit an example program and argue that it satisfies the rules yet does not satisfy noninterference. Your program must leak information through overt, not covert, channels.

Problem 4. Integrity

The security policy noninterference for integrity can be informally stated as,

"Changes in untrusted inputs do not cause changes in trusted outputs."

Intuitively, untrusted (i.e., tainted) information should not be allowed to corrupt trusted (i.e., untainted) information.

1. Examine the following statements. Explain which statements satisfy noninterference for integrity, which don't, and why. A security type τ can now be either T, for Trusted, or U, for Untrusted. Assume that typing context Γ assigns types to variables as follows: Γ(x) = Γ(y) = T, and Γ(v) = Γ(z) = U.

   1. x := y + z;
   2. v := y + z;
   3. if (x) then y := x; else v := z;
   4. if (v) then y := x; else v := z;

2. We will now reformulate the type system from lecture, which enforced only noninterference for confidentiality, to make it enforce both noninterference for confidentiality and noninterference for integrity.

   1. Let a security type τ now be a pair of a confidentiality type and an integrity type—for example, if Γ(x) = (S,T), then variable x contains information that is both secret and trusted. Define the ≤ relation for these extended security labels. τ1 ≤ τ2 should hold if and only if information at level τ1 is allowed to flow to level τ2.
   2. Give syntax-directed inference rules for assignment and if statements that enforce both noninterference for confidentiality and noninterference for integrity. You should give a single rule for each kind of statement (so two rules total), and your rules should forbid implicit flows.