We present a general unwinding framework for the definition of information flow security properties of concurrent programs, described in a simple imperative language enriched with parallelism and atomic statement constructors. We study different classes of programs obtained by instantiating the general framework and we prove that they entail the noninterference principle. Accurate proof techniques for the verification of such properties are defined by exploiting the Tarski decidability result for first-order formulae over the reals. Moreover, we illustrate how the unwinding framework can be instantiated in order to deal with intentional information release and we extend our verification techniques to the analysis of security properties of programs admitting downgrading. © IOS Press and the authors. All rights reserved.

Compositional information flow security for concurrent programs

PIAZZA, Carla;
2007

Abstract

We present a general unwinding framework for the definition of information flow security properties of concurrent programs, described in a simple imperative language enriched with parallelism and atomic statement constructors. We study different classes of programs obtained by instantiating the general framework and we prove that they entail the noninterference principle. Accurate proof techniques for the verification of such properties are defined by exploiting the Tarski decidability result for first-order formulae over the reals. Moreover, we illustrate how the unwinding framework can be instantiated in order to deal with intentional information release and we extend our verification techniques to the analysis of security properties of programs admitting downgrading. © IOS Press and the authors. All rights reserved.
File in questo prodotto:
File Dimensione Formato  
jcs2007.pdf

non disponibili

Tipologia: Documento in Pre-print
Licenza: Non pubblico
Dimensione 212.2 kB
Formato Adobe PDF
212.2 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
jcs07.pdf

non disponibili

Descrizione: Editorial version
Tipologia: Versione Editoriale (PDF)
Licenza: Non pubblico
Dimensione 420.26 kB
Formato Adobe PDF
420.26 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/689009
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 20
  • ???jsp.display-item.citation.isi??? ND
social impact