針對以角色為基底的存取控制系統 - 以切割方法輔助對可滿足性為基底的驗證

HRU的問題是，在一套策略規則下，給定初始的保護矩陣，給予存取權限後，對於狀態的可到達性進行驗證。過去三十年，這樣的問題被證明是無解的。然而，Kleiner和Newcomb使用了通訊循序處理單元(CSP)去證明，在無資料相依性下資訊安全的系統中，針對SATL進行模組驗證是有解的。除此之外，受限的KN問題仍然缺少一個自動化的驗證方法。做為一個解決方案，我們將這樣的方法模組化成一個可滿足性的問題，該問題的內容是，對於一套策略規則，可以針對通用的SATL且沒有明確構建狀態模型的先驗去進行模組驗證。這可藉由一個叫做權限繼承的關鍵技術來執行。此外，所提出的方法也支援泛用的以角色為基底的存取控制(RBAC)去定義授權。另一個議題是龐大的問題大小，我們提出切割方法去解決這個問題。實作狀態收斂確保驗證可以中斷，不會進入無窮迴圈。利用兩個真實的例子：員工資訊系統和醫院資訊系統，除了證明了該方法的正確性和中止，也被用來說明該方法的可行性和有效性。在例子EIS中，SRV方法會比S3V方法減少了18個變數。在例子HIS中，切割方法可以加速執行時間0.74秒，並減少所使用的記憶體2280KB。

關鍵字

以角色為基底的存取控制；存取控制；可滿足性；驗證

並列摘要

The Harrison-Ruzzo-Ullman problem is the verification of a set of policy rules, starting from an initial protection matrix, for the reachability of a state in which a generic access right is granted. Three decades ago, it was shown to be undecidable; however, recently Kleiner and Newcomb (KN) used communicating sequential processes (CSP) to prove that the model checking of data-independent security systems against universal safety access temporal logic (SATL) is decidable. Nevertheless, this restricted KN problem still lacks an automatic verification method. As a solution, we modeled it as a satisfiability (SAT) problem such that a set of policy rules can be model checked against a universal SATL property without explicitly constructing the state model a priori. This is made possible by a key technique called permission inheritance. Further, the proposed method also supports the popular role-based access control (RBAC) scheme of authorization. Another issue is the large problem size, we propose a slicing method to address this issue. State convergence was implemented to ensure that the verification stops without infinite looping. Besides proving the correctness and termination of the proposed method, two real cases namely employee information system (EIS) and hospital information system (HIS) are also used to illustrate the feasibility and efficiency of the proposed method. The SRV method reduced 18 literals than S3V method for EIS. The slicing method speeded up the execution time with 0.74s and reduced the memory with 2280KB for HIS.

並列關鍵字

RBAC ； access control ； SAT ； verification

參考文獻

[2] S. William, Computer Security: Principles and Practice. Pearson Education India, 2008.

[7] E. Kleiner and T. Newcomb, “On the decidability of the safety problem for access control policies,” Electronic Notes in Theoretical Computer Science, vol. 185, pp. 107–120, September 2007.

[8] M. Davis and H. Putnam, “A computing procedure for quantification theory,” Journal of the ACM (JACM), vol. 7, no. 3, pp. 201–215, 1960.

[9] E. Clarke, A. Biere, R. Raimi, and Y. Zhu, “Bounded model checking using satisfiability solving,” Formal Methods in System Design, vol. 19, pp. 7–34, July 2001.

[10] R. S. Sandhu, “Role-based access control,” Advances in computers, vol. 46, pp. 237–286, 1998.

國際替代計量

針對以角色為基底的存取控制系統 - 以切割方法輔助對可滿足性為基底的驗證

未授權

主題瀏覽