CS 5430 Homework 4: Information Flow

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

Due March 23, 10 am. No late assignments will be accepted.

Submit your solution using CMS. Prepare your solution using Word (.doc) or some ascii editor (.txt), as follows:

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

1. Noninterference

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

"Changes in high inputs do not cause changes in low 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: HI (high in), HO (high out), LI (low in), LO (low out).

System U copies all input from HI to HO, from LI to LO, and additionally echoes all data from LI to HO.
After receiving an input x on HI and an input y on LI, system V outputs y on LO if x is even, and y^y on LO if x is odd, where ^ denotes string concatenation.
Upon receiving plaintext x such that |x|=32 on HI, system W generates a uniformly random one-time pad k such that |k|=32, then outputs the one-time pad encryption of x with k—that is, x XOR k—on LO.
System X receives plaintext m on HI and RSA public key K on LI, then outputs the RSA encryption of m with K—that is, m^e mod n, where K=(e,n)—on LO.

2. Arrays

In lecture, we built a static analysis that enforced noninterference for confidentiality, for a very simple programming language. 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 that all array indices are always within bounds.

Examine the following three statements, whose variables are subscripted by confidentiality labels. 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.
1. c_H[m_L] = n_L;
2. o_L = d_L[p_H];
3. e_L = f_H;

The rules below are proposed to check information flow for arrays. (Recall from lecture that "S sif pc = C" means that program S satisfies noninterference if the label on the program counter is C.) The first rule allows array element selection (e.g., a[i]) as part of expression E. Variables in expressions may be arrays or scalars. In the first rule, x may be either an array variable or a scalar variable, but it may not be an array element selection. In the second rule, a is an array.

C ≤ x E ≤ x		C ≤ a E1 ≤ a E2 ≤ a

x = E; sif pc = C		a[E1] = E2; sif pc = C

Unfortunately, these rules do not enforce noninterference. Exhibit an example program and argue that it satisfies the rules yet does not satisfy noninterference.

3. 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 information should not be allowed to corrupt trusted information.

Examine the following statements, which have integrity labels as subscripts on variables. The labels are T, for Trusted, and U, for Untrusted. Explain which statements satisfy noninterference for integrity, which don't, and why.
1. x_T = y_T + z_U;
2. v_U = y_T + z_U;
3. if (x_T) y_T = x_T; else v_U = z_U;
4. if (v_U) y_T = x_T; else v_U = z_U;
We will now reformulate the static analysis from lecture, which enforced only noninterference for confidentiality, to make it enforce both noninterference for confidentiality and noninterference for integrity.
1. Let a security label now be a pair of a confidentiality label and an integrity label—for example, if x = (H,T), then variable x contains information that is high (i.e., secret) and trusted. Define the ≤ relation for these extended security labels. Recall that L1 ≤ L2 should hold if and only if information at label L1 is allowed to flow to label L2.
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.