Noninterference Analysis of Bounded Labeled Petri Nets

This paper focuses on a fundamental problem on information security of bounded labeled Petri nets: non-interference analysis. As in hierarchical control, we assume that a system is observed by users at different levels, namely high-level users and low-level users. The output events produced by the firing of transitions are also partitioned into high-level output events and low-level output events. In general, high-level users can observe the occurrence of all the output events, while low-level users can only observe the occurrence of low-level output events. A system is said to be non-interferent if low-level users cannot infer the firing of transitions labeled with high-level output events by looking at low-level outputs. In this paper, we study a particular non-interference property, namely strong non-deterministic non-interference (SNNI), using a special automaton called SNNI Verifier, and propose a necessary and sufficient condition for SNNI.