Information flow vs. resource access in the asynchronous pi-calculus

摘要: We propose an extension of the asynchronous π-calculus in which a variety security properties may be captured using types. These are input/output types for I/O capabilities assigned specific levels. The main innovation is uniform typing system that, by varying slightly allowed set types, captures different notions security.We first define that ensures processes running at level σ cannot access resources with higher than σ. notion control guaranteed this formalized terms Type Safety Theorem.We then show restricting our prohibits implicit information flow from high-level to low-level processes. prove behavior can not influenced changes behavior. This as noninterference theorem respect testing.