In this paper, we consider the information flow security properties named Persistent Stochastic Non-Interference (PSNI) and Delimited Persistent Stochastic Non-Interference (D_PSNI) for stochastic cooperating processes described as terms of the Performance Evaluation Process Algebra (PEPA). A PEPA process P that satisfies (D)_PSNI admits only controlled information flows from the high, private, level of confidentiality to the low, public, one. In particular, the downgrading/declassification of information is permitted only when performed by a trusted component. Once a process has been defined one can only check whether it satisfies (D)_PSNI or not. In this work, we contribute to the verification and construction of secure processes in two respects: (i) first we prove new compositionality properties for (D)_PSNI and then (ii) we exploit them in order to introduce a new process algebra which allows the definition of processes which are secure by construction, thus avoiding any further check.

A process algebra for (delimited) persistent stochastic non-interference

Marin A.;Piazza C.;Rossi S.
2019

Abstract

In this paper, we consider the information flow security properties named Persistent Stochastic Non-Interference (PSNI) and Delimited Persistent Stochastic Non-Interference (D_PSNI) for stochastic cooperating processes described as terms of the Performance Evaluation Process Algebra (PEPA). A PEPA process P that satisfies (D)_PSNI admits only controlled information flows from the high, private, level of confidentiality to the low, public, one. In particular, the downgrading/declassification of information is permitted only when performed by a trusted component. Once a process has been defined one can only check whether it satisfies (D)_PSNI or not. In this work, we contribute to the verification and construction of secure processes in two respects: (i) first we prove new compositionality properties for (D)_PSNI and then (ii) we exploit them in order to introduce a new process algebra which allows the definition of processes which are secure by construction, thus avoiding any further check.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
File in questo prodotto:
File Dimensione Formato  
paper.pdf

non disponibili

Descrizione: Articolo principale
Tipologia: Documento in Pre-print
Licenza: Accesso chiuso-personale
Dimensione 358.89 kB
Formato Adobe PDF
358.89 kB Adobe PDF   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: http://hdl.handle.net/10278/3722872
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact