Persistent BNDC (P BNDC for short) is an information-flow security property 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.

Transforming processes to check and ensure Information Flow Security

BOSSI, Annalisa;FOCARDI, Riccardo;ROSSI, Sabina
2002

Abstract

Persistent BNDC (P BNDC for short) is an information-flow security property 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.
Algebraic Methodology and Software Technology
File in questo prodotto:
File Dimensione Formato  
amast.pdf

non disponibili

Tipologia: Documento in Pre-print
Licenza: Accesso chiuso-personale
Dimensione 229.16 kB
Formato Adobe PDF
229.16 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/10278/32668
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact