Distributed Non-Interference
share
Information flow security properties were defined some years ago (see, e.g., the surveys <cit.>) in terms of suitable equivalence checking problems. These definitions were provided by using sequential models of computations (e.g., labeled transition systems <cit.>), and interleaving behavioral equivalences (e.g., bisimulation equivalence <cit.>). More recently, the distributed model of Petri nets has been used to study non-interference in <cit.>, but also in these papers an interleaving semantics was used. We argue that in order to capture all the relevant information flows, truly-concurrent behavioral equivalences must be used. In particular, we propose for Petri nets the distributed non-interference property, called DNI, based on branching place bisimilarity <cit.>, which is a sensible, decidable equivalence for finite Petri nets with silent moves. Then we focus our attention on the subclass of Petri nets called finite-state machines, which can be represented (up to isomorphism) by the simple process algebra CFM <cit.>. DNI is very easily checkable on CFM processes, as it is compositional, so that it does does not suffer from the state-space explosion problem. Moreover, we show that DNI can be characterized syntactically on CFM by means of a type system.
READ FULL TEXT