| Summary: | 碩士 === 國立中正大學 === 資訊工程研究所 === 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.
|
|---|
