王精明，江怡順

（1.滁州學(xué)院 計算機與信息工程學(xué)院，安徽 滁州239012；2.華東理工大學(xué) 計算機科學(xué)與工程系，上海 200237）

基于Petri網(wǎng)的非演繹安全模型的分析與驗證

王精明1，2，江怡順1

（1.滁州學(xué)院 計算機與信息工程學(xué)院，安徽 滁州239012；2.華東理工大學(xué) 計算機科學(xué)與工程系，上海 200237）

就刻畫安全的本質(zhì)而言，基于非演繹信息流安全模型較之與基于訪問控制的安全模型更為確切。文章在基于跡語義對非演繹信息流安全模型進行分析的基礎(chǔ)上，給出了基于擴展Petri網(wǎng)的非演繹模型的形式化描述，進一步基于Petri網(wǎng)的形式化描述給出非演繹模型的驗證算法且開發(fā)相應(yīng)的驗證工具，最后通過實例說明該算法的正確性和驗證工具的方便適用性。

跡語義；Petri網(wǎng)；信息流安全模型；非演繹模型

信息的機密性是分級安全系統(tǒng)研究的核心問題之一，安全模型的兩個主要分支是基于信息流的安全模型和基于訪問控制安全模型［1］?；谠L問控制安全模型主要側(cè)重于定義怎樣做才能保證系統(tǒng)是安全的，而信息流安全模型側(cè)重于安全是什么，從這點上說，就刻畫安全的性質(zhì)而言，基于信息流的安全模型較基于訪問控制的安全模型更為確切和本質(zhì)［2］。自Sutherland于1986年首次提出非演繹（non－deducibility）信息流安全模型以來，基于非演繹模型的研究不斷深入，且其應(yīng)用也越來越廣泛，如［3－6］。

本文第一個工作在介紹相關(guān)概念和定義基礎(chǔ)上以Petri網(wǎng)作為工具來形式化描述非演繹安全模型。因為Petri網(wǎng)在表示真并發(fā)方面既有直觀的圖形表示又有嚴格的形式化定義，另外為了刻畫分級安全系統(tǒng)中不同等級的動作，本文借鑒［7－8］中的方法擴展了基本Petri網(wǎng)，即對Petri網(wǎng)變遷進行劃分，使其具有刻畫和描述非演繹信息流安全模型的能力。

本文第二個工作基于跡語義和Petri網(wǎng)對非演繹信息流安全模型進行了分析和描述，然后基于擴展Petri網(wǎng)給出了非演繹模型的形式化描述，并且給出了非演繹模型的驗證算法且開發(fā)了相應(yīng)的驗證工具，最后通過實例說明了該算法的正確性和驗證工具的方便適用性。

1 相關(guān)定義和概念

1.1 標(biāo)識變遷系統(tǒng)

作為并發(fā)語言操作語義描述的首選模型，標(biāo)識變遷系統(tǒng)Labeled Transition Systems（縮寫為LTS）［9］可以理解為可能具有無窮狀態(tài)的自動機。本文仍然采用標(biāo)識變遷系統(tǒng)表示文中涉及到的操作語義。

定義1 標(biāo)識變遷系統(tǒng)

標(biāo)識變遷系統(tǒng)可以理解為一個三元組＜S，T，→＞，其中：①S表示狀態(tài)集合；

②T表示動作集合；

——S和T分別表示有窮庫所和變遷集，且無交集

——F?（S×T）∪（T×S）表示流關(guān)系

庫所集合S上的多重集表示表示m，約定對于任意一個標(biāo)識m和庫所s，m（s）表示庫所s中的標(biāo)識（token）數(shù)。

設(shè)x∈S∪T，x＝｛y｜F（y，x）｝表示x的前置集，x＝｛y｜F（x，y）｝表示x的后置集。如果t?m，我們說變遷t在標(biāo)志m處是可觸發(fā)的，若變遷t觸發(fā)了，我們稱系統(tǒng)從一個狀態(tài)到達了另一個狀態(tài)，此時的系統(tǒng)的標(biāo)識為m′，且m′＝（m＼t）⊕t，其中＼表示減法操作，⊕表示加法操作，記做m［t〉m′。

（N，m0）表示一個網(wǎng)系統(tǒng)，N是網(wǎng)，m0稱為初始標(biāo)識，在不產(chǎn)生歧義的情況下，有時也用（S，T，F(xiàn)，m0）表示網(wǎng)系統(tǒng)。

我們用［m〉表示m的可達標(biāo)識集，定義如下：

——m∈［m〉

—— 如果m′∈［m〉，且存在某個變遷t使得，m′［t〉m″，那么m″∈［m〉，則m″∈［m〉

對于網(wǎng)系統(tǒng)（S，T，F(xiàn)，m0），可執(zhí)行變遷序列遞歸定義如下：

——m0是一個可執(zhí)行變遷序列

——如果m0［t1〉m1…［tn〉mn是一個可執(zhí)行變遷，且mn［tn＋1〉mn＋1，那么m0［t1〉m1…［tn〉mn［tn＋1〉mn＋1也是一個可執(zhí)行變遷，其中稱t1t2…tn為變遷序列？TS（N）表示變遷序列的集合。

如果網(wǎng)系統(tǒng)（S，T，F(xiàn)，m0）中任意一個庫所的標(biāo)識數(shù)在任何一個標(biāo)志下均小于等于1則稱網(wǎng)系統(tǒng)是安全網(wǎng)，本文在安全網(wǎng)系統(tǒng)的范圍內(nèi)分析和驗證非演繹模型目的是為了限制系統(tǒng)在運行過程中的任何時刻均能接受輸入，其目的是在不影響所得結(jié)論的前提下降低所討論問題的復(fù)雜性，其依據(jù)為任何一個Petri網(wǎng)均能化為安全網(wǎng)系統(tǒng)［8］。

2 Petri網(wǎng)及擴展后的操作

為刻畫分級安全系統(tǒng)，本文將Petri網(wǎng)的變遷操作分為兩個等級H和L，分別表示高級變遷和和低級變遷，分別對應(yīng)于分級安全系統(tǒng)的高級用戶和低級用戶，又因為非演繹安全模型涉及到對系統(tǒng)高級輸入的保護，進而將H劃分為HI和HO，分別對應(yīng)系統(tǒng)的高級輸入和高級輸出。

非演繹安全模型是基于系統(tǒng)的低用戶視角來加以刻畫和描述，所謂低級用戶視角是指低級用戶所能觀察到的動作范圍。高級用戶一般有較高權(quán)限，能觀察到系統(tǒng)的所有動作行為，非演繹安全模型其本質(zhì)就是為了防止低級用戶能夠推斷出高級用戶的輸入動作。一般認為系統(tǒng)的不安全是因為系統(tǒng)的輸入導(dǎo)致的，非演繹安全模型認為保護了系統(tǒng)的高級輸入也就保護了系統(tǒng)的安全。簡單擴展Petri網(wǎng)后的變遷序列操作定義如下。

定義4N＝（S，H，L，F(xiàn)，m0）是一個網(wǎng)系統(tǒng)，變遷序列的操作定義如下：

其中ε表示空變遷，δ表示任意變遷序列，同理，HI、HO上變遷序列操作可類似定義，本文不再贅述。

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

非演繹信息流安全模型由Sutherland［10］于1986年首次提出，其原始定義如下，信息從函數(shù)f1流到函數(shù)f2當(dāng)且僅當(dāng)（?σ∈Σ）（?Z—：f－12（Z—）≠λ），?ˉσ∈Σ：f1（σ）＝f1（ˉσ），（f2（ˉσ）≠Z－）。取該定義的否定形式，很容易得到信息不會從函數(shù)f1流到函數(shù)f2，當(dāng)且僅當(dāng)（?σ∈Σ）（?Z—：f－12（Z－）≠λ），?ˉσ∈Σ：f1（σ）＝f1（ˉσ）∧（f2（ˉσ）＝Z－），具體推理如下：

所謂系統(tǒng)是非演繹安全的是指對系統(tǒng)的低級動作的觀察是不能推導(dǎo)出任何高級輸入事件的是否發(fā)生。換句話說，一個系統(tǒng)是非演繹安全的，如果系統(tǒng)的任意高級輸入動作的是否發(fā)生不會改變低級動作是否發(fā)生，即任何高級輸入動作與低級動作是兼容的。基于跡語義非演繹信息流安全模型描述如下：

其中ActL表示低級動作集合，ActHI表示高級輸入動作集合，表示限制操作符號，如系統(tǒng)E＝L1H1L2H2，EL＝L1L2，τ、τ＇和ξ為系統(tǒng)的跡，關(guān)于T（E）的定義見文1.2節(jié)。

可將上式寫成下述的等價的基于Petri網(wǎng)的描述式，系統(tǒng)滿足非演繹安全模型，當(dāng)且僅當(dāng)

分級安全系統(tǒng)是將系統(tǒng)的低級動作映射為對非機密數(shù)據(jù)的處理，將系統(tǒng)的高級動作映射為對機密數(shù)據(jù)的處理。非演繹安全模型要求對于系統(tǒng)的任何低級觀察，任意的高級輸動作的發(fā)生均不會改變系統(tǒng)的任意低級觀察，這樣使得低級用戶不會推導(dǎo)出系統(tǒng)的高級用戶的任何信息，從另外一層意義上說也就保護了高級輸入動作的安全性，防止了機密信息泄密從而達到了安全。

從這個層面上說，相對于訪問控制安全模型來說其刻畫安全更為本質(zhì)，因為訪問控制安全模型如BLP模型是通過事先制定訪問權(quán)限及相應(yīng)規(guī)則來達到保證系統(tǒng)的安全性，所以訪問控制安全模型強調(diào)如何才能保證安全，而非演繹安全模型則強調(diào)的是安全是什么。

4 非演繹信息流安全模型的驗證算法

圖1 系統(tǒng)E1的Petri網(wǎng)描述

圖2 系統(tǒng)E2的Petri網(wǎng)描述

圖3 Set1的生成算法

圖4 Nondeducibility驗證算法

設(shè)n表示系統(tǒng)的Petri網(wǎng)系統(tǒng)表示的分支個數(shù)，也就是系統(tǒng)可能執(zhí)行的跡的個數(shù)，τlow代表各個可能執(zhí)行的跡在低級動作集上限制操作所得到的結(jié)果，τ［i］或τ［j］表示系統(tǒng)可能執(zhí)行的跡。集合Set1代表系統(tǒng)E在高級輸入動作集上限制操作所得到的變遷序列集合，集合Set2由判斷是否滿足非演繹安全模型的高級輸入動作組成的集合。為清晰起見，集合Set1的生成算法用流程圖1闡述，流程圖2為判斷系統(tǒng)E是否滿足非演繹安全模型的算法。

5 安全模型檢查工具NDChecker

根據(jù)上述算法，本文使用Java語言開發(fā)了非演繹安全模型驗證工具NDChecker，圖4為NDChecker驗證工具的界面。驗證工具界面由系統(tǒng)的Petri網(wǎng)的可執(zhí)行跡表達式的輸入部分、結(jié)果顯示以及OK按鈕3部分組成。系統(tǒng)根據(jù)輸入的表達式進程驗證，如果滿足非演繹安全模型則結(jié)果輸出true，否則輸出false并且會給出一個反例。

圖5 NDChecker演示結(jié)果1

圖6 NDChecker演示結(jié)果2

為了規(guī)范化輸入，輸入格式規(guī)定高級動作用H和h表示，其中H表示高級輸入動作，h表示高級輸入動作，L表示低級動作。“＋”表示可執(zhí)行跡的選擇操作，“.”表示動作之間的連接操作符，0表示結(jié)束符。如圖4中進程表達式E＝L1.L2.0＋H1.L1.h1.L2.0滿足非演繹安全特性，驗證結(jié)果為true，如圖5所示系統(tǒng)E＝L1.L2.0＋H1.L1.h1.0則不滿足非演繹安全模型，輸出結(jié)果為false，且給出了個反例，反例表明觀察者通過觀察L1.L2.0低級動作，如果觀察到L2動作的發(fā)生，必然能推倒出H1動作沒有發(fā)生，從而導(dǎo)致了隱通道的不安全。

6 結(jié)束語

基于非演繹信息流安全模型相對于與基于訪問控制的安全模型在刻畫信息流安全方面顯的更為確切和本質(zhì)，然而基于不同的語義模型，如何檢測系統(tǒng)的信息流安全模型以及相應(yīng)的檢測工具開發(fā)仍然是一個難題和挑戰(zhàn)。本文基于跡語義和Petri網(wǎng)討論了非演繹信息流安全模型的形式化描述和定義，并且給出了非演繹模型的一個驗證算法，進一步基于Java語言實現(xiàn)了該算法，開發(fā)出了安全模型驗證工具NDChecker，最后通過實例顯示其操作的正確性和易用性。

［1］周 偉，尹 青，王清賢.計算機安全中的經(jīng)典模型［J］.計算機科學(xué)，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］.計算機科學(xué)，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網(wǎng)的信息流安全屬性的分析與驗證［J］.計算機應(yīng)用研究，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－），男，安徽岳西人，博士生，研究方向：信息流安全模型、形式化方法。

安徽省高校省級自然科學(xué)研究基金項目（KJ2011Z279）；滁州學(xué)院重點自然科學(xué)基金項目（2010kj008Z）

2011-09-22