Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Transforming Processes to Check and Ensure Information Flow Security*

Annalisa BossiContact Information, Riccardo FocardiContact Information, Carla PiazzaContact Information and Sabina RossiContact Information

(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).

Contact Information Annalisa Bossi
Email: bossi@dsi.unive.it

Contact Information Riccardo Focardi
Email: focardi@dsi.unive.it

Contact Information Carla Piazza
Email: piazza@dsi.unive.it

Contact Information Sabina Rossi
Email: srossi@dsi.unive.it
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.107 • Server: mpweb24
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)