A Uniform Type Structure for Secure Information Flow 
<p>
Kohie Honda and Nobuko Yoshida
<br> 
<p>
<br>The pi-calculus is a formalism of computing in which we can
<br>compositionally represent dynamics of major programming constructs by
<br>decomposing them into a single communication primitive, the name passing. 
<br>This work reports our experience in using a linear/affine
<br>typed pi-calculus for analysis and development of type systems of
<br>programming languages, focusing on secure information flow
<br>analysis. After presenting a basic typed calculus, its type structure
<br>is instrumented to capture secrecy. We demonstrate the usage of the
<br>resulting calculus by a sound embedding of the dependency core
<br>calculus (DCC) and by development of a novel type discipline for
<br>imperative programs which properly extends both a secure
<br>multi-threaded imperative language by Volpano and Smith and 
<br>(a call-by-value version of) DCC.  In each case, the embedding gives a
<br>simple proof of noninterference.
<br>
<br>This paper is a full version of its earlier version in POPL'02, with 
<br>detailed proofs. The emphasis is on illustrating, through concrete 
<br>examples, how the typed pi-calculus can be used for developing and 
<br>justifying a non-trivial type-based analysis of programming languages. 
<br>Along this spirit, the presentation of the call-by-value version of 
<br>DCC and the extended version of Smith-Volpano language is considerably 
<br>simplified from the POPL'02 version by reformulation of encodings and 
<br>a simplification of the linear/affine pi-calculus with state. The 
<br>present version also gives more comparisons with related work, 
<br>including a formal conservative extenstion result with respect to 
<br>Smith's recent secure imperative language.