Noninterference through Flow Analysis

Kohei Honda and Nobuko Yoshida

This paper proposes new syntactic inference rules which can directly
extract information flow in a given typed process in the
pi-calculus. In the flow analysis, a flow in a process is captured as
a chain of possible interactions which transform differences in
behaviours from one part of its interface to another part of its
interface. Polarity in types (which is in close correspondence with
polarity in Polarised Linear Logic) plays a fundamental role in the
analysis, which is elucidated via examples. We show that this
inductive flow analysis can be used for giving simple proofs of
noninterference in the secrecy analyses for the pi-calculus with
linear/affine typing, including its concurrent, stateful extensions.