Title: Non-interference analysis of bounded labeled Petri nets Show Chinese title

Title: 有界标记Petri网的非干扰性分析

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. Show Chinese abstract

Abstract: 本文专注于有界标记Petri网信息安全的一个基本问题：非干扰性分析。 如同分层控制一样，我们假设系统被不同级别的用户观察，即高级用户和低级用户。 由转换触发产生的输出事件也被划分为高级输出事件和低级输出事件。 一般来说，高级用户可以观察所有输出事件的发生，而低级用户只能观察低级输出事件的发生。 如果低级用户无法通过查看低级输出来推断出标记为高级输出事件的转换的触发，则该系统被认为是无干扰的。 在本文中，我们使用一种称为SNNI验证器的特殊自动机来研究一种特定的非干扰性属性，即强非确定性非干扰（SNNI），并提出了SNNI的必要且充分条件。