  Information flow control type systems statically restrict the propagation of
sensitive data to ensure end-to-end confidentiality. The property to be shown
is noninterference, asserting that an attacker cannot infer any secrets from
made observations. Session types delimit the kinds of observations that can be
made along a communication channel by imposing a protocol of message exchange.
These protocols govern the exchange along a single channel and leave
unconstrained the propagation along adjacent channels. This paper contributes
an information flow control type system for linear session types. The type
system stands in close correspondence with intuitionistic linear logic.
Intuitionistic linear logic typing ensures that process configurations form a
tree such that client processes are parent nodes and provider processes child
nodes. To control the propagation of secret messages, the type system is
enriched with secrecy levels and arranges these levels to be aligned with the
configuration tree. Two levels are associated with every process: the maximal
secrecy denoting the process' security clearance and the running secrecy
denoting the highest level of secret information obtained so far. The
computational semantics naturally stratifies process configurations such that
higher-secrecy processes are parents of lower-secrecy ones, an invariant
enforced by typing. Noninterference is stated in terms of a logical relation
that is indexed by the secrecy-level-enriched session types. The logical
relation contributes a novel development of logical relations for session typed
languages as it considers open configurations, allowing for more nuanced
equivalence statement.
