基于Petri网的非演绎安全模型的分析与验证

王精明，江怡顺

（1.滁州学院 计算机与信息工程学院，安徽 滁州239012；2.华东理工大学 计算机科学与工程系，上海 200237）

基于Petri网的非演绎安全模型的分析与验证

王精明1，2，江怡顺1

（1.滁州学院 计算机与信息工程学院，安徽 滁州239012；2.华东理工大学 计算机科学与工程系，上海 200237）

就刻画安全的本质而言，基于非演绎信息流安全模型较之与基于访问控制的安全模型更为确切。文章在基于迹语义对非演绎信息流安全模型进行分析的基础上，给出了基于扩展Petri网的非演绎模型的形式化描述，进一步基于Petri网的形式化描述给出非演绎模型的验证算法且开发相应的验证工具，最后通过实例说明该算法的正确性和验证工具的方便适用性。

迹语义；Petri网；信息流安全模型；非演绎模型

信息的机密性是分级安全系统研究的核心问题之一，安全模型的两个主要分支是基于信息流的安全模型和基于访问控制安全模型［1］。基于访问控制安全模型主要侧重于定义怎样做才能保证系统是安全的，而信息流安全模型侧重于安全是什么，从这点上说，就刻画安全的性质而言，基于信息流的安全模型较基于访问控制的安全模型更为确切和本质［2］。自Sutherland于1986年首次提出非演绎（non－deducibility）信息流安全模型以来，基于非演绎模型的研究不断深入，且其应用也越来越广泛，如［3－6］。

本文第一个工作在介绍相关概念和定义基础上以Petri网作为工具来形式化描述非演绎安全模型。因为Petri网在表示真并发方面既有直观的图形表示又有严格的形式化定义，另外为了刻画分级安全系统中不同等级的动作，本文借鉴［7－8］中的方法扩展了基本Petri网，即对Petri网变迁进行划分，使其具有刻画和描述非演绎信息流安全模型的能力。

本文第二个工作基于迹语义和Petri网对非演绎信息流安全模型进行了分析和描述，然后基于扩展Petri网给出了非演绎模型的形式化描述，并且给出了非演绎模型的验证算法且开发了相应的验证工具，最后通过实例说明了该算法的正确性和验证工具的方便适用性。

1 相关定义和概念

1.1 标识变迁系统

作为并发语言操作语义描述的首选模型，标识变迁系统Labeled Transition Systems（缩写为LTS）［9］可以理解为可能具有无穷状态的自动机。本文仍然采用标识变迁系统表示文中涉及到的操作语义。

定义1 标识变迁系统

标识变迁系统可以理解为一个三元组＜S，T，→＞，其中：①S表示状态集合；

②T表示动作集合；

——S和T分别表示有穷库所和变迁集，且无交集

——F⊆（S×T）∪（T×S）表示流关系

库所集合S上的多重集表示表示m，约定对于任意一个标识m和库所s，m（s）表示库所s中的标识（token）数。

设x∈S∪T，x＝｛y｜F（y，x）｝表示x的前置集，x＝｛y｜F（x，y）｝表示x的后置集。如果t⊆m，我们说变迁t在标志m处是可触发的，若变迁t触发了，我们称系统从一个状态到达了另一个状态，此时的系统的标识为m′，且m′＝（m＼t）⊕t，其中＼表示减法操作，⊕表示加法操作，记做m［t〉m′。

（N，m0）表示一个网系统，N是网，m0称为初始标识，在不产生歧义的情况下，有时也用（S，T，F，m0）表示网系统。

我们用［m〉表示m的可达标识集，定义如下：

——m∈［m〉

—— 如果m′∈［m〉，且存在某个变迁t使得，m′［t〉m″，那么m″∈［m〉，则m″∈［m〉

对于网系统（S，T，F，m0），可执行变迁序列递归定义如下：

——m0是一个可执行变迁序列

——如果m0［t1〉m1…［tn〉mn是一个可执行变迁，且mn［tn＋1〉mn＋1，那么m0［t1〉m1…［tn〉mn［tn＋1〉mn＋1也是一个可执行变迁，其中称t1t2…tn为变迁序列？TS（N）表示变迁序列的集合。

如果网系统（S，T，F，m0）中任意一个库所的标识数在任何一个标志下均小于等于1则称网系统是安全网，本文在安全网系统的范围内分析和验证非演绎模型目的是为了限制系统在运行过程中的任何时刻均能接受输入，其目的是在不影响所得结论的前提下降低所讨论问题的复杂性，其依据为任何一个Petri网均能化为安全网系统［8］。

2 Petri网及扩展后的操作

为刻画分级安全系统，本文将Petri网的变迁操作分为两个等级H和L，分别表示高级变迁和和低级变迁，分别对应于分级安全系统的高级用户和低级用户，又因为非演绎安全模型涉及到对系统高级输入的保护，进而将H划分为HI和HO，分别对应系统的高级输入和高级输出。

非演绎安全模型是基于系统的低用户视角来加以刻画和描述，所谓低级用户视角是指低级用户所能观察到的动作范围。高级用户一般有较高权限，能观察到系统的所有动作行为，非演绎安全模型其本质就是为了防止低级用户能够推断出高级用户的输入动作。一般认为系统的不安全是因为系统的输入导致的，非演绎安全模型认为保护了系统的高级输入也就保护了系统的安全。简单扩展Petri网后的变迁序列操作定义如下。

定义4N＝（S，H，L，F，m0）是一个网系统，变迁序列的操作定义如下：

其中ε表示空变迁，δ表示任意变迁序列，同理，HI、HO上变迁序列操作可类似定义，本文不再赘述。

3 非演绎信息流安全模型的形式化表示

非演绎信息流安全模型由Sutherland［10］于1986年首次提出，其原始定义如下，信息从函数f1流到函数f2当且仅当（∃σ∈Σ）（∃Z—：f－12（Z—）≠λ），∀¯σ∈Σ：f1（σ）＝f1（¯σ），（f2（¯σ）≠Z－）。取该定义的否定形式，很容易得到信息不会从函数f1流到函数f2，当且仅当（∀σ∈Σ）（∀Z—：f－12（Z－）≠λ），∃¯σ∈Σ：f1（σ）＝f1（¯σ）∧（f2（¯σ）＝Z－），具体推理如下：

所谓系统是非演绎安全的是指对系统的低级动作的观察是不能推导出任何高级输入事件的是否发生。换句话说，一个系统是非演绎安全的，如果系统的任意高级输入动作的是否发生不会改变低级动作是否发生，即任何高级输入动作与低级动作是兼容的。基于迹语义非演绎信息流安全模型描述如下：

其中ActL表示低级动作集合，ActHI表示高级输入动作集合，表示限制操作符号，如系统E＝L1H1L2H2，EL＝L1L2，τ、τ＇和ξ为系统的迹，关于T（E）的定义见文1.2节。

可将上式写成下述的等价的基于Petri网的描述式，系统满足非演绎安全模型，当且仅当

分级安全系统是将系统的低级动作映射为对非机密数据的处理，将系统的高级动作映射为对机密数据的处理。非演绎安全模型要求对于系统的任何低级观察，任意的高级输动作的发生均不会改变系统的任意低级观察，这样使得低级用户不会推导出系统的高级用户的任何信息，从另外一层意义上说也就保护了高级输入动作的安全性，防止了机密信息泄密从而达到了安全。

从这个层面上说，相对于访问控制安全模型来说其刻画安全更为本质，因为访问控制安全模型如BLP模型是通过事先制定访问权限及相应规则来达到保证系统的安全性，所以访问控制安全模型强调如何才能保证安全，而非演绎安全模型则强调的是安全是什么。

4 非演绎信息流安全模型的验证算法

图1 系统E1的Petri网描述

图2 系统E2的Petri网描述

图3 Set1的生成算法

图4 Nondeducibility验证算法

设n表示系统的Petri网系统表示的分支个数，也就是系统可能执行的迹的个数，τlow代表各个可能执行的迹在低级动作集上限制操作所得到的结果，τ［i］或τ［j］表示系统可能执行的迹。集合Set1代表系统E在高级输入动作集上限制操作所得到的变迁序列集合，集合Set2由判断是否满足非演绎安全模型的高级输入动作组成的集合。为清晰起见，集合Set1的生成算法用流程图1阐述，流程图2为判断系统E是否满足非演绎安全模型的算法。

5 安全模型检查工具NDChecker

根据上述算法，本文使用Java语言开发了非演绎安全模型验证工具NDChecker，图4为NDChecker验证工具的界面。验证工具界面由系统的Petri网的可执行迹表达式的输入部分、结果显示以及OK按钮3部分组成。系统根据输入的表达式进程验证，如果满足非演绎安全模型则结果输出true，否则输出false并且会给出一个反例。

图5 NDChecker演示结果1

图6 NDChecker演示结果2

为了规范化输入，输入格式规定高级动作用H和h表示，其中H表示高级输入动作，h表示高级输入动作，L表示低级动作。“＋”表示可执行迹的选择操作，“.”表示动作之间的连接操作符，0表示结束符。如图4中进程表达式E＝L1.L2.0＋H1.L1.h1.L2.0满足非演绎安全特性，验证结果为true，如图5所示系统E＝L1.L2.0＋H1.L1.h1.0则不满足非演绎安全模型，输出结果为false，且给出了个反例，反例表明观察者通过观察L1.L2.0低级动作，如果观察到L2动作的发生，必然能推倒出H1动作没有发生，从而导致了隐通道的不安全。

6 结束语

基于非演绎信息流安全模型相对于与基于访问控制的安全模型在刻画信息流安全方面显的更为确切和本质，然而基于不同的语义模型，如何检测系统的信息流安全模型以及相应的检测工具开发仍然是一个难题和挑战。本文基于迹语义和Petri网讨论了非演绎信息流安全模型的形式化描述和定义，并且给出了非演绎模型的一个验证算法，进一步基于Java语言实现了该算法，开发出了安全模型验证工具NDChecker，最后通过实例显示其操作的正确性和易用性。

［1］周 伟，尹 青，王清贤.计算机安全中的经典模型［J］.计算机科学，2004，31（3）：195－200.

［2］Ryan PYA，Schneider SA.Process algebra and non－interference［J］.Journal of Computer Security.2001，9（1，2）：75－103.

［3］McCullough D.Noninterference and the composition of security properties.In：Proc.of the IEEE Symposium on Research in Security and Privacy［C］.1988.177－186.

［4］HanTang，B.McMillin.Security of information flow in the electric power grid［J］.Critical Infrastructure Protection，2007（253）：43－56.

［5］周 伟，尹 青，郭金庚.计算机安全中的无干扰模型［J］.计算机科学，2005，32（2）：159－165.

［6］Ravi Akella，Han Tang，Bruce M.Mcmillin.Analysis of information flow security in cyber－physical systems［J］.International Journal of Critical Infrastructure Protection，2010，3，157－173.

［7］Nadia Busi，Roberto Gorrieri.A Survey on Non－interference with Petri Nets［C］.Lecture Notes in Computer Science，2004，3098，91－113.

［8］陈 松，周从华，鞠时光，等.基于Petri网的信息流安全属性的分析与验证［J］.计算机应用研究，2010，21（12）：4639－4642.

［9］RMilner Communication and Concurrency［M］.Prentice－Hall，1989.

［10］D.Sutherland.A model of information［C］.In Proceeding of the 9th National Computer Security Conference，Baltimore，MD，September，1986.175－183.

Petri Net-based Analysis and Verification of Non-deducibility Security Model

Wang Jingming， Jiang Yishun

In characterizing security，non－deducibility security model captures more essence than access control security models.This paper describes and formally defines non－deducibility model based on trace semantics and Petri net.Furthermore，this paper provides the verification algorithm for non－deducibility security model based on Petri net and offers the verification tools with several examples.

Trace Semantics；Petri net；Information Flow Security Model；Non－deducibility Model

TP309

A

1673-1794（2012）02-0021-04

王精明（1979－），男，安徽岳西人，博士生，研究方向：信息流安全模型、形式化方法。

安徽省高校省级自然科学研究基金项目（KJ2011Z279）；滁州学院重点自然科学基金项目（2010kj008Z）

2011-09-22