Types for Information Flow Analysis
Information flow analysis consists in determining how a program's inputs influence its output -- or, more generally, its behavior. Such an analysis allows controlling how much information is leaked by letting someone observe the program's output -- or, again, its behavior. Thus, it has a very wide range of potential applications. Yet, it has so far received little practical use, because realistic information flow analyses can be difficult to design, to prove correct, and to automate. Formulating these analyses as type systems seems a promising approach, and has recently allowed a few steps forward.
In this course, I will first give a brief overview of the field's history, and present a number of ways of formally expressing the correctness of an information flow analysis. I will present a way of constructing such analyses for a purely functional language. Then, I will proceed to add side-effects (i.e. references and exceptions) to the programming language at hand, and will explain why this seems to require a slightly different construction. Lastly, I will describe an entirely different approach, developed by Abadi and Blanchet, which allows proving secrecy properties of security protocols expressed in an extension of the spi-calculus with cryptographic operations.
Articles