Oregon Programming Languages Summer School 2019
Security-Typed Languages
June 17–20, 2019
Andrew Myers

[ Lectures and Notes | Readings | Homework ]

Lectures and Notes


The following are papers mentioned during the lectures.

Homework problems

  1. Suppose that we extended our IMP language with first order functions with a single integer argument and result. Our programs would start with a series of function (really, procedure) declarations and then give a "main program" command:

        f1(x1) { c1; return a1 }
        f2(x2) { c2; return a2 }
        fn(xn) { cn; return an }

    We extend commands to include procedure calls:

    c ::= ... | x1 := f (x2)

    Let's extend the type system to handle these procedures. We need to add bindings to our context Γ, giving the type of the procedures fi. The security types of the procedures need to include three components. Two are obvious: the label of the argument and the label of the result. The third is an upper bound on the pc label at the caller. Let's write Γ(f) = lapc lr to represent these three components.

    1. Give a typing rule for checking procedure declarations.

    2. Give a typing rule for checking procedure calls.

    3. Use your rules to show that the following insecure programs cannot type-check for any type of f, assuming li:L and h:H and H⋢L:

          f(x) { l3 := true; return l3 }
          if (h) {
      	l1 := f(l2)

          f(x) { skip; return x }
          l1 := f(h)
  2. Prove the high-pc lemma mentioned in the course notes for Lecture 2. Hint: use the same induction principle as for the main noninterference proof.