Non-interference analysis of bounded labeled Petri nets

TL;DR

This paper analyzes non-interference in bounded labeled Petri nets, proposing a new automaton-based method to verify strong non-deterministic non-interference, ensuring low-level users cannot infer high-level system activities.

Contribution

It introduces a novel automaton called SNNI Verifier and provides a necessary and sufficient condition for verifying strong non-deterministic non-interference in Petri nets.

Findings

Proposes a new automaton-based verification method.

Establishes a necessary and sufficient condition for SNNI.

Enhances understanding of information flow security in Petri nets.

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.