Dynamics and secure information flow for a higher-order pi-calculus

Abstract

We show how a type system for secure information flow for a π-calculus with higher-order λ-abstractions can be extended with dynamics without weakening the non-interference guarantees. The type system for the π-calculus ensures that the traffic on high channels does not influence the traffic on low channels. λ-abstractions make it possible to send processes over channels. Dynamics make it possible to send processes and other data of different types over the same channel, making communication between processes easier. If dynamics are used, the types of some expressions or channels may depend on type variables that are instantiated at run time. To make it still possible to statically check secure information flow, we ensure that instantiating a type variable in an expression also instantiates it in the type of the expression. © 2013 Springer-Verlag.