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.
Compositional information flow security for concurrent programs
BOSSI, Annalisa;ROSSI, Sabina
2007-01-01
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.File | Dimensione | Formato | |
---|---|---|---|
JCS07.pdf
non disponibili
Tipologia:
Documento in Pre-print
Licenza:
Licenza non definita
Dimensione
420.26 kB
Formato
Adobe PDF
|
420.26 kB | Adobe PDF | Visualizza/Apri |
I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.