Lecture 3 notes: see the tutorial notes below
For Lecture 4, the following is a high-level overview of language-based work on enforcing information flow properties. But a lot has happened since 2003 when it was written!
Language-based information-flow security. IEEE Journal on Selected Areas in Communications, special issue on Formal Methods for Security, 21(1):5–19, January 2003. Andrei Sabelfeld and Andrew C. Myers.
Fred Schneider's paper on trace properties and enforcement mechanisms is a good background to lecture 1 and a good starting point on the literature about what security policies are enforceable. Michael Clarkson's paper with Fred on hyperproperties generalizes trace properties to encompass a broad range of security properties.
Enforceable security policies. ACM TOIS 3(1), February 2000. Fred B. Schneider.
Hyperproperties. Journal of Computer Security, 18(6):1157–1210, 2010. Michael R. Clarkson and Fred B. Schneider.
Here is a tutorial defining a security type system for IMP and showing one way to prove that the type system enforces noninterference. It corresponds roughly to lectures 2 and 3.
Proving noninterference for a while-language using small-step operational semantics. March 2011. Andrew C. Myers.
The following paper is a nice survey of issues in accommodating declassification, and pointers to papers on the topic. It offers principles that declassification mechanisms ought to satisfy and a framework for categorizing different kinds of mechanisms.
Declassification: dimensions and principles. Journal of Computer Security 17(5), 2009. Andrei Sabelfeld and David Sands.
One constraint on declassification (and endorsement) that seems very useful in reasoning about real systems is a notion of robustness, which says that security-relevant operations cannot be influenced by adversaries. The most recent work on robustness instantiates Sabelfeld and Sands' notion of robust endorsement in a knowledge-based framework for information security:
Enforcing robust declassification and qualified robustness. Journal of Computer Security, 14(2):157–196, 2006. Andrew C. Myers, Andrei Sabelfeld and Steve Zdancewic.
Attacker control and impact for confidentiality and integrity. Logical Methods in Computer Science, 7(3), September 2011. Aslan Askarov and Andrew C. Myers.
A second approach to constraining information release is to control which information is released. Relaxed noninterference and delimited release try to capture this idea.
A model for delimited release. 2003 Int'l Symposium on Software Security. LNCS 3233, Springer-Verlag, 2004, pages 174–191. Andrei Sabelfeld and Andrew C. Myers.
Downgrading policies and relaxed noninterference. POPL 2005. Peng Li and Steve Zdancewic.
A third approach is to control when or under what conditions information may be downgraded. Again, various ideas have been tried, even including the use of temporal logic.
End-to-end enforcement of erasure and declassification. CSF'08. Stephen Chong and Andrew C. Myers.
Model checking information flow in reactive systems. VMCAI'12. Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus N. Rabe1, and Helmut Seidl.
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 ::= ... | 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) = la→pc
lr 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 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)