Andrei Sabelfeld - PER Model of Secure Information Flow
You have received a program from an untrusted source. Let us call it company M. M promises to help you to optimise your personal financial investments, information about which you have stored in a database on your home computer. The software is free (for a limited time), under the condition that you permit a log-file containing a summary of your usage of the program to be automatically emailed back to the developers of the program (who claim they wish to determine the most commonly used features of their tool). Is such a program safe to use? The program must be allowed access to your personal investment information, and is allowed to send information, via the log-file, back to M. But how can you be sure that M is not obtaining your sensitive private financial information by cunningly encoding it in the contents of the innocent-looking log-file? This is an example of the problem of determining that the program has secure information flow. Information about your sensitive ``high-security'' data should not be able to propagate to the ``low-security'' output (the log-file). Traditional methods of access control are of limited use here since the program has legitimate access to the database.
This talk proposes an extensional semantics-based formal specification of secure information-flow properties in sequential programs based on representing degrees of security by partial equivalence relations. The specification clarifies and unifies a number of specific correctness arguments in the literature, and connections to other forms of program analysis. The approach is inspired by (and equivalent to) the use of partial equivalence relations in specifying binding-time analysis, and is thus able to specify security properties of higher order functions and ``partially confidential data'' (e.g. one's financial database could be deemed to be partially confidential if the number of entries is not deemed to be confidential even though the entries themselves are). We show how the approach can be extended to handle nondeterminism, and illustrate how the various choices of powerdomain semantics affect the kinds of security properties that can be expressed, ranging from termination-insensitive properties (corresponding to the use of the Hoare (partial correctness) powerdomain) to probabilistic security properties, obtained when one uses a probabilistic powerdomain.
The talk is based on the paper: Andrei Sabelfeld and David Sands. A Per Model of Secure Information Flow in Sequential Programs. In Proceedings of European Symposium on Programming, LNCS 1576, Amsterdam, March 1999. Springer-Verlag.