[TYPES] Paper Announcement: Three Papers on Secure Information Flow Analysis

[Nobuko Yoshida]

The following three papers on Secure Information Flow Analysis
are available. The first two use typed pi-calculi. The third 
uses a different method, a program logic, but is related.
 
   http://www.doc.ic.ac.uk/~yoshida/pi_security.html
 
   1. A Uniform Type Structure for Secure Information Flow
      (a full version of a paper at POPL 2002) (update: Sep 2004)
   2. Noninterference through Flow Analysis
      (to appear in Journal of Functional Programming) (update: Aug 2004) 
   3. Program Logic and Program Analysis
      (draft: Aug 2004)
 
We shall be grateful for any comments and suggestions from you.
 
Kohei Honda (kohei at dcs.qmul.ac.uk)
Martin Berger (martinb at dcs.qmul.ac.uk)
Nobuko Yoshida (yoshida at doc.ic.ac.uk)
 
----------------------------------------------------------
 
A Uniform Type Structure for Secure Information Flow (98 pages)
 
Kohei Honda and Nobuko Yoshida
 
Abstract:
 
The pi-calculus is a process calculus in which we can compositionally
represent dynamics of various algorithmic entities, among others major
programming constructs, by decomposing them into name passing. This
work reports our experience in using a linear/affine typed pi-calculus
for the analysis and development of type-based analyses for
programming languages, focussing on secure information flow
analysis. After presenting a basic typed calculus for secrecy, we
demonstrate its usage by a sound embedding of the dependency core
calculus (DCC) and the development of the call-by-value version of
DCC. The secrecy analysis is then extended to stateful computation,
using which we develop a novel type discipline for imperative
programming language which extends a secure multi-threaded imperative
language by Smith and Volpano with general references and higher-order
procedures. In each analysis, the embedding gives a simple proof of
noninterference.
 
This paper is a full version of its earlier version in POPL'02, with
detailed proofs. The emphasis is on illustrating, through concrete
examples, how the typed pi-calculus can be used for developing and
justifying a non-trivial type-based analysis of programming languages.
Along this spirit, the presentation of the call-by-value version of
DCC and the extended version of Smith-Volpano language is considerably
simplified from the POPL'02 version by reformulation of encodings and
a simplification of the linear/affine pi-calculus with state. The
present version also gives more comparisons with related work,
including a formal conservative extention result with respect to
Smith's recent secure imperative language.
 
--------------------------------------------------------------------
 
Noninterference through Flow Analysis (58 pages)
 
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 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.
 
-----------------------------------------------------------------
 
Program Logic and Program Analysis (82 pages)
 
Kohei Honda, Nobuko Yoshida and Martin Berger
 
Abstract:
 
One of the central merits of compositional program logics as a
foundation of software engineering is their potential ability to
describe a large class of properties of programs relative to a chosen
notion of observability.  One open issue in achieving such descriptive
power has been the lack of a precise logical treatment of
pragmatically significant language features such as higher-order
procedures, expressions with side effects and shared mutable data
structures.
 
This paper introduces a compositional program logic for a higher-order
polymorphic imperative language with local state. A central feature of
the logic is its systematic use of names and operations on them.
Assertions in the logic describe all and only observable properties of
programs in the sense that valid assertions for a program precisely
characterise its behaviour up to the observational congruence. After
illustrating the logic through examples, we demonstrate its
descriptive power by presenting a logical justification of a
type-based secure information flow analysis. The key idea is to
translate typability in the secrecy typing to an assertion in the
logic which directly describes non-interference. This has the
following merits: (1) a precise logical description of the
noninterference property; (2) a very short, mechanical correctness
proof of the secrecy typing via soundness of the logic; and (3)
generalisation and classification of secrecy analyses on a uniform
logical basis.
 
-----------------------------------------------------------------