We study bisimulation-based information flow security properties which are persistent, in the sense that if a system is secure then all of its reachable states are secure too. We show that such properties can be characterized in terms of bisimulation-like equivalence relations, between the full system and the system prevented from performing confidential actions. Moreover, we provide a characterization of such properties in terms of unwinding conditions which demand properties of individual actions. These two different characterizations naturally lead to efficient methods for the verification and construction of secure systems. We also prove several compositionality results, that allow us to check the security of a system by only verifying the security of its subcomponents.

Verifying Persistent Security Properties

PIAZZA, Carla;
2004-01-01

Abstract

We study bisimulation-based information flow security properties which are persistent, in the sense that if a system is secure then all of its reachable states are secure too. We show that such properties can be characterized in terms of bisimulation-like equivalence relations, between the full system and the system prevented from performing confidential actions. Moreover, we provide a characterization of such properties in terms of unwinding conditions which demand properties of individual actions. These two different characterizations naturally lead to efficient methods for the verification and construction of secure systems. We also prove several compositionality results, that allow us to check the security of a system by only verifying the security of its subcomponents.
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/849642
 Attenzione

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

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 32
  • ???jsp.display-item.citation.isi??? 21
social impact