Noninterference Analysis of Bounded Petri Nets Using Basis Reachability Graph

In this paper, we deal with two problems related to security and privacy of bounded Petri nets, namely non-interference analysis and enforcement. A system could be monitored by different types of users, high-level and low-level users, who have access to different information even if both know the structure of the system. Low-level users can observe only the occurrence of a subset of events. On the contrary, high-level users can observe the occurrence of all the events affecting the system dynamics. A system is said non-interferent if low-level users cannot infer the occurrence of those events that are observable only by high-level users. In this paper, we deal with the problems of analysis and enforcement of a particular non-interference property, namely strong non-deterministic non-interference (SNNI). In particular, we show that, under the assumption of acyclicity of the high-level subnet, the notions of basis marking and basis reachability graph (BRG) allow to solve the problems of SNNI analysis and enforcement with clear advantages in terms of computational complexity since they prevent exhaustive marking enumeration.