Information flow through a program is secure if users' high-security
inputs do not affect low-security behavior of a program, that is, if
an attacker cannot learn any secrets by observing public outputs.
Type systems have been used to guarantee secure information flow: a
language is designed so that only secure programs are well-typed.  We
illustrate the principle with one such language based on monads ---
types used to indicate the presence of side-effects such as
input/output, mutation of a memory store, exceptions, etc.  We show
that monads can also be used to reason about secure information flow.
Prior secure languages tag all values with security levels.  In
contrast, in our language only mutable store locations are tagged, and
monads classify computations according to the security levels of the
locations they access.  Starting from a purely functional language,
ours is a lighter-weight extension that simplifies the task of
reasoning about programs.

An important consideration in the design of a secure programming
language is the interaction of high- and low-security computations.
In our language a new informativeness judgment addresses this problem:
high-security computations may be composed with low-security
computations if their result types are not informative.
Informativeness also gives rise to an equivalence relation on
computations, and non-interference is a confluence theorem modulo this
relation.

This is joint work with Karl Crary and Frank Pfenning.