By Kenji Miyamoto and Atsushi Igarashi. In Proceedings of Workshop on Foundations of Computer Security (FCS'04), pages 187-203. July 2004.
Information flow analysis is a program analysis that detects possible illegal information flow such as the leakage of (partial information on) passwords to the public. Recently, several type-based techniques for information flow analysis have been proposed for various kinds of programming languages. Details of those type systems, however, vary substantially and even their core parts are often slightly different, making the essence of the type system unclear.
In this paper we propose a typed lambda calculus \lambda_s^\Box as a foundation for information flow analysis. The type system is developed so that it corresponds to a proof system of an intuitionistic modal logic of validity by the Curry-Howard isomorphism. The calculus enjoys the properties of subject reduction, confluence, and strong normalization. Moreover, we show that the noninterference property, which guarantees that, in a well-typed program, no information on confidential data is leaked to the public, can be proved in a purely syntactic and very simple manner. We also demonstrate that a core part of the SLam calculus by Heintze and Riecke can be encoded into \lambda_s^\Box.
$Date: 2005-12-24 00:37:08 +0900 (Sat, 24 Dec 2005) $