Noninterference Analysis of Bounded Petri Nets Using Basis Reachability Graph

In this article, we deal with two problems related to security and privacy of bounded Petri nets, namely, noninterference 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 noninterferent if low-level users cannot infer the occurrence of those events that are observable only by high-level users. In this article, we deal with the problems of analysis and enforcement of a particular noninterference property, namely, strong nondeterministic noninterference (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 allow to solve the problems of SNNI analysis and enforcement with clear advantages in terms of computational complexity since they prevent exhaustive marking enumeration.