15th IEEE Computer Security Foundations Workshop (CSFW'02)
Information Flow Security in Dynamic Contexts
Cape Breton, Nova Scotia, Canada
June 24-June 26
ISBN: 0-7695-1689-0
We study a security property for processes in dynamic contexts, i.e., contexts that can be reconfigured at run-time. The security property that we propose in this paper, named Persistent BNDC, is such that a process is "secure" when every state reachable from it satisfies a basic Non-Interference property. We define a suitable bisimulation based equivalence relation among processes, that allows us to express the new property as a single equivalence check, thus avoiding the universal quantifications over all the reachable states (required by Persistent BNDC) and over all the possible hostile environments (implicit in the basic Non-Interference property we adopt). We show that the novel security property is compositional and we discuss how it can be efficiently checked.