Transforming Processes to Check and Ensure Information Flow Security
*
Annalisa Bossi6
, Riccardo Focardi6
, Carla Piazza6
and Sabina Rossi6 
| (6) |
Dipartimento di Informatica, Universitá Ca’ Foscari di Venezia, France |
Abstract
Persistent BNDC (P BNDC for short) is an information- flow securitypro perty for processes in dynamic contexts, i.e., contexts that can be reconfigured
at runtime. We propose a method for transforming an arbitrary process into a process satisfying P_BNDC and show that the transformation preserves the “low level” observational semantics for a large class of processes. We also
study how to efficiently verify P_BNDC by exploiting a characterization of it through a suitable notion of weak bisimulation up to high level actions. We define a second transformation over processes which allows us to reduce the problem of checking P_BNDC to the problem of testing a weak bisimulation between two processes. This approach is particularly appealing as it allows
us to perform the P_BNDC check using already existing tools at a low time complexity.
This work has been partiallys upported by the MURST project “Modelli formali per la sicurezza” and the EU Contract IST-2001-32617
“Models and Types for Security in Mobile Distributed Systems” (MyThS).
References secured to subscribers.