SAT-based Verification of Role-based Access Control Systems with Slicing method
碩士 === 國立中正大學 === 資訊工程研究所 === 102 === 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, re...
Main Authors: | , |
---|---|
Other Authors: | |
Format: | Others |
Language: | en_US |
Published: |
2014
|
Online Access: | http://ndltd.ncl.edu.tw/handle/x6n4dp |
id |
ndltd-TW-102CCU00392033 |
---|---|
record_format |
oai_dc |
spelling |
ndltd-TW-102CCU003920332019-05-15T21:22:56Z http://ndltd.ncl.edu.tw/handle/x6n4dp SAT-based Verification of Role-based Access Control Systems with Slicing method 針對以角色為基底的存取控制系統 - 以切割方法輔助對可滿足性為基底的驗證 Jui-Lung Yao 姚瑞隆 碩士 國立中正大學 資訊工程研究所 102 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. Pao-Ann Hsiung 熊博安 2014 學位論文 ; thesis 43 en_US |
collection |
NDLTD |
language |
en_US |
format |
Others
|
sources |
NDLTD |
description |
碩士 === 國立中正大學 === 資訊工程研究所 === 102 === 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.
|
author2 |
Pao-Ann Hsiung |
author_facet |
Pao-Ann Hsiung Jui-Lung Yao 姚瑞隆 |
author |
Jui-Lung Yao 姚瑞隆 |
spellingShingle |
Jui-Lung Yao 姚瑞隆 SAT-based Verification of Role-based Access Control Systems with Slicing method |
author_sort |
Jui-Lung Yao |
title |
SAT-based Verification of Role-based Access Control Systems with Slicing method |
title_short |
SAT-based Verification of Role-based Access Control Systems with Slicing method |
title_full |
SAT-based Verification of Role-based Access Control Systems with Slicing method |
title_fullStr |
SAT-based Verification of Role-based Access Control Systems with Slicing method |
title_full_unstemmed |
SAT-based Verification of Role-based Access Control Systems with Slicing method |
title_sort |
sat-based verification of role-based access control systems with slicing method |
publishDate |
2014 |
url |
http://ndltd.ncl.edu.tw/handle/x6n4dp |
work_keys_str_mv |
AT juilungyao satbasedverificationofrolebasedaccesscontrolsystemswithslicingmethod AT yáoruìlóng satbasedverificationofrolebasedaccesscontrolsystemswithslicingmethod AT juilungyao zhēnduìyǐjiǎosèwèijīdǐdecúnqǔkòngzhìxìtǒngyǐqiègēfāngfǎfǔzhùduìkěmǎnzúxìngwèijīdǐdeyànzhèng AT yáoruìlóng zhēnduìyǐjiǎosèwèijīdǐdecúnqǔkòngzhìxìtǒngyǐqiègēfāngfǎfǔzhùduìkěmǎnzúxìngwèijīdǐdeyànzhèng |
_version_ |
1719112497683759104 |