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. Persistent_BNDC (P_BNDC, for short) is an information-flow security property which is suitable to deal with processes in dynamic contexts. In this work we show that P_BNDC is compositional with respect to the replication operator. Then, by exploiting the compositionality properties of the class of P_BNDC processes, we define a proof system which provides a very efficient technique for the stepwise development and the verification of recursively defined P_BNDC processes.

Information Flow Security and Recursive Systems

PIAZZA, Carla;
2003-01-01

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. Persistent_BNDC (P_BNDC, for short) is an information-flow security property which is suitable to deal with processes in dynamic contexts. In this work we show that P_BNDC is compositional with respect to the replication operator. Then, by exploiting the compositionality properties of the class of P_BNDC processes, we define a proof system which provides a very efficient technique for the stepwise development and the verification of recursively defined P_BNDC processes.
2003
3540202161
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS 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: https://hdl.handle.net/11390/685365
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact