Lectures and Notes
Lecture 1
Lecture 2
Lecture 3

Lecture 3, Video Part 1  Lecture 3, Video Part 2  Lecture 3, Video Part 3  Lecture 3, Video Part 4
 Scribed notes forthcoming
Lecture 4
Readings
The following are papers mentioned during the lectures.
Homework problems

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:
f_{1}(x_{1}) { c_{1}; return a_{1} } f_{2}(x_{2}) { c_{2}; return a_{2} } ... f_{n}(x_{n}) { c_{n}; return a_{n} } c
We extend commands to include procedure calls:
c ::= ...  x_{1}
:=
f(
x_{2})
Let's extend the type system to handle these procedures. We need to add bindings to our context Γ, giving the type of the procedures
f_{i}
. 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) = l_{a}→^{pc} l_{r} to represent these three components.Give a typing rule for checking procedure declarations.
Give a typing rule for checking procedure calls.
Use your rules to show that the following insecure programs cannot typecheck for any type of f, assuming l_{i}: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)
 Prove the highpc lemma mentioned in the course notes for Lecture 2. Hint: use the same induction principle as for the main noninterference proof.