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.
|Data di pubblicazione:||2002|
|Titolo:||Transforming processes to check and ensure Information Flow Security|
|Titolo del libro:||Algebraic Methodology and Software Technology|
|Appare nelle tipologie:||4.1 Articolo in Atti di convegno|
File in questo prodotto:
|amast.pdf||Documento in Pre-print||Accesso chiuso-personale||Riservato|