Nowadays, most of the main database management systems offer, in one way or another, the possibility of protecting data using _ne-grained access control (FGAC) policies, i.e., policies that depend on dynamic properties of the system state. Reasoning about FGAC policies typically amounts to answering questions about whether a security-related property holds in a (possibly infinite) set of system states. To carry out this reasoning, we propose a novel, tool-supported methodology, which consists in transforming the aforementioned questions about FGAC policies into satisfiability problems in first-order logic. In addition, we report on our experience using the Z3 Satisfiability Modulo Theory (SMT) solver for automatically checking the satisfiability of the first-order formulas generated by the tool implementing our methodology, called SecProver, for a non-trivial set of examples.
|Cite as: de Dios, M.A.G., Dania, C. and Clavel, M. (2015). Formal Reasoning about Fine-Grained Access Control Policies. In Proc. 11th Asia-Pacific Conference on Conceptual Modelling (APCCM 2015) Sydney, Australia. CRPIT, 165. Saeki, M. and Kohler, H. Eds., ACS. 91-100 |