A uniform type structure for secure information flow

Abstract

The -calculus is a process calculus in which we can compositionally represent dynamics of major programming constructs by decomposing them into a single communication primitive, the name passing. This work reports our experience in using a linear/aÆne typed -calculus for the analysis and development of type-based analyses for programming languages, focussing on secure information ow 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 callby- 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.