Oregon Programming Languages Summer School 2012
Short course on language-based security
Andrew Myers

[ Notes | Readings | Homework ]



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)