Distributed Non-Interference

TL;DR

This paper introduces a new distributed non-interference property for Petri nets using branching place bisimilarity, which is decidable and efficiently checkable for finite-state machines, advancing information flow security analysis.

Contribution

It proposes DNI based on branching place bisimilarity for Petri nets and provides a syntactic characterization for finite-state machines, improving decidability and compositional analysis.

Findings

DNI is decidable for finite Petri nets with silent moves.

DNI can be checked efficiently on CFM processes due to its compositional nature.

A type system characterizes DNI syntactically on CFM processes.

Abstract

Information flow security properties were defined some years ago (see, e.g., the surveys \cite{FG01,Ry01}) in terms of suitable equivalence checking problems. These definitions were provided by using sequential models of computations (e.g., labeled transition systems \cite{GV15}), and interleaving behavioral equivalences (e.g., bisimulation equivalence \cite{Mil89}). More recently, the distributed model of Petri nets has been used to study non-interference in \cite{BG03,BG09,BC15}, 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 {\em branching place bisimilarity} \cite{Gor23b}, 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 {\em finite-state machines}, which can be represented (up to isomorphism) by the simple process algebra CFM \cite{Gor17}. 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.