XML語言中命題邏輯的安全策略復合分析

【摘 要】因為網絡系統的異構性，以及個人對安全需求的不同，安全策略多樣性可能導致的不一致和沖突現象使用安全策略分析成為必要，本文從命題邏輯的理論框架和分析算法對策略的一致性和變化影響分析，沖突檢測。能夠實現對安全策略自動分析服務。

【關鍵詞】安全策略；算法；檢測

【中圖分類號】TP309.2 【文獻標識碼】A

【文章編號】2095-3089（2018）33-0007-01

Abstract：Because of the heterogeneity of network systems and the differences in security needs of individuals， it is necessary to use security policy analysis for inconsistencies and conflicts that may result from the diversity of security policies. In this paper， the theoretical framework and analysis algorithm of propositional logic are used to analyze the consistency and variation of policy， and conflict detection. It can automatically analyze the security policy.

Key words：security strategy； algorithm； check

命題演算大概是在所有當前使用的邏輯演算中最簡單的一種，它是使用命題形式把世界抽象成符號的一套語言體系。它的特征是具有強大的表達能力同時非常的簡單。

一、問題描述

網絡中系統的互聯提高了網絡數據資源的共誤享性和協作能力，而資源的擁有者或管理者希望在資源上加上訪問約束，來限制非法用戶的訪問，否則數據資將存在嚴重的安全威脅，這勢必造成同樣的資源上有各方的安全需求，因為每個角色對數據的安全需求并不相同，安全策略會把某些敏感重要的權限分配給了不可知用戶，而檢測這種情況是非常困難的。這可歸為一種潛在的安全威脅。

二、命題邏輯安全策略的分析

1.命題邏輯安全策略分析。

Wijesekera在命題邏輯層次上提出了一種安全策略復合的框架，命題邏輯層次指的是把安全策略看做一些抽象的符號以及把他們的語義看做為指派給主體的許可集的任意轉化器——>如果主體 s 由一個策略指派了許可集中一個集合 x，那么 x 中僅有一個許可集可以指派給 s，但是怎樣選擇那個許可集是隨意的。從這個角度將，此方法的語義跟安全策略中的標準概念有很大的不同，但它是安全訪問策略或許可指派約束的元策略的一種典型，比如義務約束的分離。

一個許可可表示成{object， action}，而許可集就是上述許可的集合。比如{（file1，+read），（file1，-write）}便是一個許可集。而{Alice，PermitSet}指許可集PermitSet 指 派 給 對 象 Alice ， （Alice， {{（file1，+read）， （file1，-write）}，{（file1，-read），（file1，+write）}） 指 Alice 被 指 派 了 許 可 集 或 者 為{（file1，+read），（file1，-write）} ， 或 者 為（file1，-write）}，{（file1，-read），（file1，+write）}，但兩者不可兼得。使用了 T：（s，PermSet） –>（s，PermSet）轉化，意為對 s 的許可集指派從 PermSet 轉化為PermSet。注意 T 可能是不確定的，因為對象 s 可能被指派兩個或更多的許可集。既然策略是一種指派，那么策略操作可以用關系或者幾何理論操作符來表達。它們被分為兩類：外部和內部操作符。大部分操作符如合取和析取都有這兩類的擴展。比如合并，內部合并的結果為兩個策略許可集的許可合并形成的許可集，而外部合并的結果為兩個策略許可集合并成新的包含許可集的許可集集合。運算符有：（外部析取）， （外部合取）， （外部差）， （外部否定）， （內部析取）， （內部合取）， （內部差）， （內部否定），（失效符）， （外部投影），（外部指配）， （順序合并）， （open 完全，指允許所有）， （close 完全，指拒絕所有），min（選擇否定集），max（選擇肯定集），（閉包），（內部指配）。

此方法提供的框架可以合并不一致，不完全，不確定的策略。這主要是通過上述操作符的分類來實現的，它提供四種對不確定策略的支持。策略是否是確定的是可以通過內部操作符來分析的。同時，本方法定義了主體，對象，狀態，動作，授權，來完善命題邏輯復合框架的語義。完善了命題邏輯在安全控制描述方面的語義完整性，通過它可以驗證策略的一致性和檢測策略的沖突。

D. Wijesekera 給出了一個表達和復合舉例，此例說明了在基于角色的安全可控制中集合斷言的需要。

2.命題邏輯安全策略D—Algebra 復合分析。

由于 XACML 在產生決策時缺乏正常的語義，在復合領域 XACML 會產生預料之外的決策結果。那如何解決這個問題呢？明顯的，我們需要找到一種合適的決策建模方法，來彌補 XACML 的缺陷，于是產生了D—代數，它是一種決策復合的方法。

在這里，需要提到一種跟 XACML 有著很深淵源的邏輯代數，即 L∞-代數，因為它支持多值的特性極大的支持了 XACML，但是它有極大的缺陷，而不能直接轉化成 XACML，比如它的讓人無法忍受的計算高復雜性。于是 Qun Ni 等人提出了一種解決辦法，即 D-代數。它滿足了決策建模的需求，能支持 XACML 的合并算法以及其他問題。比如將在第三節講到的投票問題。

通常決策集合加上其上的運算符就可組成 D-代數。它是一種代數的結構，其中不為空的元素集合，0 是其中一個常數元素。﹁為一元運算符，而⊕，二元運算符。﹁為否定，⊕可以理解為析取，而可以定義為：

在D-代數中不支持 x⊕x=x，因為多個跟一個總是不相同的，因為這一點可以應用于下文講到的投票問題。從上述三個運算符，可以衍生出其他常用的運算符，比如⊙， ，其中前者可理解為合取，而后者表示集合的差集，他們都可以用前面的運算符表示出來。比如

D-代數的代數依賴于應用及其規則。比如 XACML，如果相關的屬性信息沒有錯誤，給定一個請求，所有的策略規則將產生下面三個其中的一個決策，permit，deny 或者 notapplicable.它們都被稱為確定的決策。我們用{p}，g0gggggg，{na}來表示。相對的，便有一種不確定的決策，用{p，na}，{d，na}來表示。它們的意思為返回的決策結果是不確定的，或為前者，或為后者。

據此，針對 XACML 的解釋，給定 P-解釋。

涵義與式 1 相同.

從從上述解釋來看，P-解釋是 8 值的（2^3）。Qun Ni 驗證了 D-代數的計算上表達的有效性，即針對每個決策矩陣構造相應的 P-解釋的表達式。決策矩陣類似于真值表，維數可變。

其中，2 維決策矩陣就可表達 XACML 的相應合并算法，比如 permit-overides。維數越大，表達的策略就可越復雜。在語言的問題描述中，本文提到由于 XACML 在一些合并算法中缺少規范的語義，導致了不明確的決策結果。XACML 定義了五種標準的規則合并算法，六種標準的策略合并算法。但是因為“indeterminate”的出現，一些算法，比如 first-applicable 會產生不恰當的結果。D-代數很好的解決了這個問題，它將從每個算法的思想出發，結合 XACML 原有算法，利用自己的解釋，給出更規范的語義定義。比如first-applicable表述如下：

三、結束語

當然，因為其表達的有效性，所有的 XACML 算法，P-解釋都可以容易的表達出來，上圖的First-Applicable 有點復雜。其他的算法表達比較容易。但是，鑒于其精確性和有效性，其在此處鍵入公式。有點已經遠遠大于其表述形式上的表述。命題邏輯應用的是許可集不確定指派的轉化思想來表達策略的效果。

參考文獻

[1]李程程，張永勝，劉廣鈺.一種安全的語義Web服務模型研究.計算機技術與發展，2010.

[2]Qun Ni，Elisa Bertino，Jorge Lobo.D-Algebra Composing Access Control Policy Decisions.ASIACCS09 March 10-12，2009.

[3]張松慧，陸標光.基于XACML的Web服務安全訪問控制.計算機應用研究.

[4]徐金芳，張永勝，隆坤.XCAML中策略/規則組合算法優化.微計算機信息，2009.

[5]D.Wijesekera and S.Jajodia.A propositonal policy algebra for access control .ACM Transactions on Information and System Security （TISS），6（2）：286-325，2003.

作者簡介：張達利（1983-），男，浙江溫嶺人，浙江工商職業技術學院教師 網絡工程師，主要從事計算機網絡方面研究。