We study a security property for processes in dynamic contexts, i.e., contexts that can be reconfigured at runtime. 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.
展开▼
