We study bisimulation-based information flow security properties which are persistent, in the sense that if a system is secure, then all states reachable from it are secure too. We show that such properties can be characterized in terms of bisimulation-like equivalence relations between the system and the system itself 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 and discuss a sufficient condition to define refinement operators preserving security.

Bisimulation and Unwinding for Verifying Possibilistic Security Properties

BOSSI, Annalisa;FOCARDI, Riccardo;ROSSI, Sabina
2003-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 states reachable from it are secure too. We show that such properties can be characterized in terms of bisimulation-like equivalence relations between the system and the system itself 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 and discuss a sufficient condition to define refinement operators preserving security.
2003
Verification, Model Checking, and Abstract Interpretation
File in questo prodotto:
File Dimensione Formato  
vmcai03.ps

non disponibili

Tipologia: Documento in Pre-print
Licenza: Accesso chiuso-personale
Dimensione 213.62 kB
Formato Postscript
213.62 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/12642
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 19
  • ???jsp.display-item.citation.isi??? 14
social impact