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

Lectures and Notes

• Lecture 1

  • Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Video Part 4

  • Scribed notes

• Lecture 2

  • Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3 | Lecture 2, Video Part 4

  • Scribed notes
  • Notes on proving NI with small-step semantics

• 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

• Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3

• Slides on secure hardware description languages
• scribed notes

Readings

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 }
       c
   

   We extend commands to include procedure calls:

   c ::= ... | x₁ := f (x₂)

   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) = l_a→^pc l_r 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 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)
      

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.