Affiliations: [a] Dipartimento di Informatica, Università Ca' Foscari di Venezia, Italy | [b] Dipartimento di Matematica e Informatica, Università degli Studi di Udine, Italy
Correspondence:
[*]
Corresponding author. Dipartimento di Informatica, Università Ca' Foscari di Venezia, via Torino 155, 30172 Venezia, Italy, Tel.: +39 041 2348422, Fax: +39 041 2348419, E-mail: srossi@dsi.unive.it.
Abstract: Information flow security in a multilevel system aims at guaranteeing that no high level information is revealed to low level users, even in the presence of any possible malicious process. This requirement could be stronger than necessary when some knowledge about the environment (context) in which the process is going to run is available. To relax this requirement we introduce the notion of secure contexts for a class of processes. This notion is parametric with respect to both the observation equivalence and the operation used to characterize the low level view of a process. As observation equivalence we consider the cases of weak bisimulation and trace equivalence. We describe how to build secure contexts in these cases and we show that two well-known security properties, named BNDC and NDC, are just special instances of our general notion.
Keywords: Process algebra, contexts, bisimulation, trace equivalence, noninterference
