Distributed Noninterference

Noninterference is the classic information flow property that establishes the absence of illegal information flows. Legality of flows is originally defined with respect to a single security setting that is based on a security lattice that orders security levels according to their confidentiality and/or integrity. This paper proposes a natural generalization of noninterference to a distributed security setting where each computation domain establishes its own local security lattice. Referred to as distributed noninterference (DNI), the new security property implies that information flows respect the allowed flow policy of the domains where they are computed. The semantic coherence between DNI and other information flow related properties for distributed settings is established. We present a type and effect system that enforces DNI for an expressive distributed higher-order lambda-calculus with imperative features and code migration.