We define several security properties for the analysis of probabilistic noninterference as a conservative extension of a classical, nondeterministic, process-algebraic approach to information flow theory. We show that probabilistic covert channels (that are not observable in the nondeterministic setting) may be revealed through our approach and that probabilistic information can be exploited to give an estimate of the amount of confidential information flowing to unauthorized users. Finally, we present a case study showing that the expressiveness of the calculus we adopt makes it possible to model and analyze real concurrent systems.

A Process Algebraic Approach for the Analysis of Probabilistic Non-Interference / A.Aldini; M.Bravetti; R.Gorrieri. - In: JOURNAL OF COMPUTER SECURITY. - ISSN 0926-227X. - STAMPA. - 12(2):(2004), pp. 191-246. [10.3233/JCS-2004-12202]

A Process Algebraic Approach for the Analysis of Probabilistic Non-Interference

BRAVETTI, MARIO;GORRIERI, ROBERTO
2004

Abstract

We define several security properties for the analysis of probabilistic noninterference as a conservative extension of a classical, nondeterministic, process-algebraic approach to information flow theory. We show that probabilistic covert channels (that are not observable in the nondeterministic setting) may be revealed through our approach and that probabilistic information can be exploited to give an estimate of the amount of confidential information flowing to unauthorized users. Finally, we present a case study showing that the expressiveness of the calculus we adopt makes it possible to model and analyze real concurrent systems.
2004
A Process Algebraic Approach for the Analysis of Probabilistic Non-Interference / A.Aldini; M.Bravetti; R.Gorrieri. - In: JOURNAL OF COMPUTER SECURITY. - ISSN 0926-227X. - STAMPA. - 12(2):(2004), pp. 191-246. [10.3233/JCS-2004-12202]
A.Aldini; M.Bravetti; R.Gorrieri
File in questo prodotto:
Eventuali allegati, non sono esposti

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/11585/6516
 Attenzione

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

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