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{Gor21b}, 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.
翻译:信息流安全属性几年前就被定义了(例如,见调查 {cite{FG01,Ry01} ), 以适当的等效检查问题来定义(例如,调查 {cite{FG01,Ry01} ) 。这些定义是通过使用顺序计算模型(例如,标签的过渡系统\cite{GV15}) 和相互分离的行为等同(例如,刺激等效{cite{cite{Mil89}) 提供的。最近, Petrii 网的分布模型被用来研究不干涉\ cite{BG03,BG09,BC15} 的问题,但在这些文件中也使用了互换的语义。我们说,为了捕捉所有相关的信息流(例如,标签的过渡系统\cite{GVV),必须使用真正一致的行为等等同。我们建议Petriwe 将分布的不干预属性(称为DNI), 以 双向位置} \ cite{G21b} 来研究不易被固定的网络与静态移动的C 进程, 。我们把注意力定位的Crembra 放在了C 。