SAT-based Verification of Data-Independent Access Control Security Systems
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 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, the authors modeled it as a satisfiability 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.