Information flow security in dynamic contexts

Article type: Research Article

Authors: Focardi, Riccardo^{; *} | Rossi, Sabina

Affiliations: Dipartimento di Informatica, Università Ca' Foscari di Venezia via Torino 155, 30172 Venezia, Italy. E-mail: [email protected], [email protected]

Correspondence: [*] Corresponding author.

Abstract: We study information flow security in the setting of mobile agents. We propose a sufficient condition to security named Persistent_BNDC. A process is Persistent_BNDC when every of its reachable states satisfies a basic Non-Interference property called BNDC. By imposing that security persists during process execution, one is guaranteed that every potential migration is performed in a stable, secure state. 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 BNDC). We prove that Persistent_BNDC is a sufficient condition to the security of mobile agents by (i) giving a sound and complete characterization of Persistent_BNDC in terms of dynamic contexts, i.e., execution contexts that can non-deterministically change at run-time, abstractly modelling arbitrary migrations; (ii) showing that Persistent_BNDC implies information flow security when agent mobility is explicitly expressed in the calculus.

Keywords: Information flow, Non-Interference, process calculi, mobility, bisimulation

DOI: 10.3233/JCS-2006-14103

Journal: Journal of Computer Security, vol. 14, no. 1, pp. 65-110, 2006