A Process Algebra for (Delimited) Persistent Stochastic Non-Interference

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.