Optimising Fine-Grained Access Control Policy Enforcement for Database Queries. A Model-Driven Approach

TL;DR

This paper presents a model-driven methodology to optimize fine-grained access control enforcement in database queries by eliminating unnecessary authorization checks using SMT solvers, improving query efficiency.

Contribution

It introduces a formal approach to optimize generated stored procedures for access control by proving the redundancy of authorization checks with SMT solvers.

Findings

Significant reduction in query execution time.

Effective elimination of unnecessary authorization checks.

Successful case study demonstration.

Abstract

Recently, we have proposed a model-driven approach for enforcing fine-grained access control (FGAC) policies when executing SQL queries. More concretely, we have defined a function SecQuery() that, given an FGAC policy S and a SQL select-statement q, generates a SQL stored-procedure SecQuery(S, q), such that: if a user u with role r is authorised, according to S, to execute q based on the current state of the database, then calling SecQuery(S, q)(u, r) returns the same result as when u executes q; otherwise, if the user u is not authorised, according to S, to execute q based on the current state of the database, then calling SecQuery(S, q)(u, r) signals an error. Not surprisingly, executing the query q takes less time than calling the corresponding stored-procedure SecQuery(S, q). Here we propose a model-based methodology for optimising the stored-procedures generated by the function SecQuery(). The idea is to eliminate authorisation checks in the body of the stored-procedures generated by SecQuery(), when they can be proved to be unnecessary. Based on our previous mapping from the Object Constraint Language (OCL) to many-sorted first-order logic, we can attempt to prove that authorisation checks are unnecessary by using SMT solvers. We include a case study to illustrate and show the applicability of our methodology.