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.

BOSSI, Annalisa;FOCARDI, Riccardo;ROSSI, Sabina
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:
File Dimensione Formato  
main.ps

non disponibili

Tipologia: Abstract
Licenza: Accesso chiuso-personale
Dimensione 389.33 kB
Formato Postscript
389.33 kB Postscript   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: https://hdl.handle.net/10278/39178
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 32
  • ???jsp.display-item.citation.isi??? 21
social impact