These days, many people define security properties based on some form of intransitive information flow specification. But in the ’90s, Fred Schneider and others were working on security automata that would monitor the execution of the program and terminate it if the program violated the security specification. For example, a specification might say that if a program has read a file containing a secret, it cannot then open a network connection.
This paper builds on work on Typed Assembly Language to develop rich, expressive type systems to capture security properties in a type system instead of via some more ad hoc approach.
At first sight, this merely repeats the work of Schneider in a different formalism: they enforce the security policy by inserting the automata and the checks into the code and then they optimize away any of the checks that they can show will not fail. But the key benefit of doing this within a typesystem is that the transformed code and each step in the optimization can be typechecked to show that it still enforces the security policy. That is, when a check is removed, the system is required to leave enough of a residue in the code that you can see why the check was not required. As a result of this, anyone who receives the code can confirm that the code will obey the security policy just by typechecking the code.