Lambda the Ultimate

I thought this paper was one of the most interesting papers at POPL this year. In it, Malacaria uses information theory to provide a quantitative analysis of how much high-security information is revealed to an attacker by a particular program.

This is extremely interesting work, because without a framework like this I don't think information flow analysis can be used to analyze real programs for security holes. That's because to date it has been all-or-nothing: the analysis flags a warning if any information is leaked to an attacker, and this is much too restrictive a notion. For example, a password routine "leaks information" to an attacker, because if an attacker guesses a password and is blocked, they've learned that the random string they guessed is not the password. But as long as an attacker can't do a brute-force search, the program is actually secure, even though it technically leaks information.

However, in Malacaria's approach, you can make this idea of security more precise, by saying something like "a secure program leaks at most c bits of information", and this makes sense because there's a quantitative measure of information leakage.

Very cool!