Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Non-interference analysis of bounded labeled Petri nets

Ning Ran, Zhengguang Wu, Shaokang Zhang, Zhou He, Carla Seatzu

TL;DR

The paper tackles strong nondeterministic non-interference (SNNI) in bounded labeled Petri nets by modeling hierarchical observation (high-level vs low-level) and showing how low-level outputs should not reveal high-level activity. It introduces the unfolded basis reachability graph (UBRG) to identify explicit sequences whose enabling may depend on high-level transitions and defines the SNNI Verifier (SV) to decide SNNI via a parallel composition of the UBRG with the low-level reachability structure. A necessary and sufficient condition for SNNI is established: the BRG-derived alpha/beta leaf-path sets must coincide with the SV-derived counterparts, leading to a finite, analyzable check with complexity O(x^2). This framework unifies language-projectivity reasoning with automata-based verification and extends prior ILP-based approaches to labeled Petri nets, offering a path toward SNNI enforcement and BSNNI extensions in future work.

Abstract

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.

Non-interference analysis of bounded labeled Petri nets

TL;DR

The paper tackles strong nondeterministic non-interference (SNNI) in bounded labeled Petri nets by modeling hierarchical observation (high-level vs low-level) and showing how low-level outputs should not reveal high-level activity. It introduces the unfolded basis reachability graph (UBRG) to identify explicit sequences whose enabling may depend on high-level transitions and defines the SNNI Verifier (SV) to decide SNNI via a parallel composition of the UBRG with the low-level reachability structure. A necessary and sufficient condition for SNNI is established: the BRG-derived alpha/beta leaf-path sets must coincide with the SV-derived counterparts, leading to a finite, analyzable check with complexity O(x^2). This framework unifies language-projectivity reasoning with automata-based verification and extends prior ILP-based approaches to labeled Petri nets, offering a path toward SNNI enforcement and BSNNI extensions in future work.

Abstract

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.
Paper Structure (12 sections, 4 theorems, 27 equations, 7 figures, 1 table, 3 algorithms)

This paper contains 12 sections, 4 theorems, 27 equations, 7 figures, 1 table, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Petri Nets
  4. Labeled Petri Nets
  5. Nondeterministic Finite Automata
  6. Unfolded Basis Reachability Graph
  7. Basis Reachability Graph
  8. Unfolded Basis Reachability Graph
  9. Strong Non-Deterministic Non-Interference Analysis
  10. The Notion of Strong Non-Deterministic Non-Interference
  11. Strong Non-Deterministic Non-Interference Verifier
  12. Conclusions

Key Result

Proposition 1

Let $(N,m_0,l,A)$ be an LPNS and $G=(\Theta,E,\Delta,m_0)$ be the BRG constructed by Algorithm 1. It holds that

Figures (7)

  • Figure 1: A labeled Petri net system.
  • Figure 2: BRG $G$ of the LPNS in Fig. \ref{['fig1']}.
  • Figure 3: UBRG $G_U$ of the LPNS in Fig. \ref{['fig1']}.
  • Figure 4: The reachability tree of the low-level subnet system of the PN system in Fig. \ref{['fig1']}.
  • Figure 5: SV $G_V$ of the PN system in Fig. \ref{['fig1']}.
  • ...and 2 more figures

Theorems & Definitions (16)

  • Definition 1: 25
  • Example 1
  • Proposition 1: 27
  • Definition 2
  • Remark 1
  • Example 2
  • Definition 3: 19
  • Proposition 2
  • Proposition 3
  • Definition 4
  • ...and 6 more