CS5430 System Security

CS5430 Homework 6: Information Flow

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

Due Monday April 30, 9am. 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.
Put your name and net id on each page. Failure to do so will result in a grade deduction.

Problem 1:

An informal description of non-interference for confidentiality is

"Changes in secret inputs do not cause changes to 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).

System U copies all input from SI to SO, from PI to PO, and additionally echoes all data from PI to SO.

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.

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:

In class, we built a type system that enforced non-interference for confidentiality. The programming language was quite simple. We now explore a richer language, which supports heap-allocated arrays (as in Java). So, we might have assignment statements of the following forms, where a and b are arrays and i is an index that is guaranteed to be in-bounds for the array:

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

Note. The effect of executing the final 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.

Suppose variables c, d, e, and f are arrays; m, n, o, and p are integers. In addition, assume that

c, f, and p are declared secret, and
d, e, m, n, and o are declared public.

Which of the following assignment statements satisfy non-interference. Explain

c[m] := n;

o := d[p];

e := f;

Problem 3: [Extra Credit]

Recall the rule given in class for ordinary assignment statements:

    Gamma |- e : tau exp
    Gamma |- v : tau var
  -------------------------
  Gamma |- v := e : tau cmd

Describe extensions to the type system and inference rule(s) that would allow certification of assignment statements that include array elements (on the left- and/or right-hand side) involving a single subscript. So your extensions should handle assignments like:

  v[i] := ...  

  w := ... v[i] ...

Note, if you introduce an additional new class of phrases (e.g., type "tau index") then be sure to give (1) the coercion properties of that phrase and (2) any additional rules required for reasoning about the new phrase type.