Probabilistic confinement in a declarative framework

We show how to formulate and analyse some security notions in the context of declarative programming. We concentrate on a particular class of security properties, namely the so-called confinement properties. Our reference language is concurrent constraint programming. We use a probabilistic version of this language (PCCP) to highlight via simple program examples the difference between probabilistic and nondeterministic confinement. The different role played by variables in imperative and constraint programming hinders a direct translation of the notion of confinement into our declarative setting. Therefore, we introduce the notion of identity confinement which is more appropriate for constraint languages. Finally, we present an approximating probabilistic semantics which can be used as a base for the analysis of confinement properties, and show its correctness with respect to the operational semantics of PCCP.