Foundations of Database Access Control

Members

Prof. Dr. David Basin
Marco Guarnieri
Srdjan Marinovic

Existing SQL access control mechanisms are extremely limited. Attackers can leak information and escalate their privileges using advanced database features such as views, triggers, and integrity constraints. This is not merely a problem of vendors lagging behind the state-of-the-art. The theoretical foundations for database access control are inadequate for evaluating security of modern database systems. They ignore advanced database features, and they fail to define a precise access control semantics, the attacker model, and the security properties that the enforcement mechanisms ought to satisfy. As a result, existing access control mechanisms are implemented in an ad hoc fashion, with neither precise security guarantees nor the means to verify them. It is not surprising, thus, that existing access control mechanisms are open to abuse.

Objective

Enlarged view: Access control mechanisms must be designed to be provably secure

This project’s goal is to (1) research and develop solid theoretical foundations for access control in modern database systems, and (2) leverage these foundations to design database access control mechanisms that are provably secure. More strongly, we argue that all database access control mechanisms must offer security proofs to clearly state what attacks and attackers they are designed to thwart. Our approach is to (1) formally define realistic attacker models and adequate security properties, complemented by a formal operational semantics of databases as a basis for the security proofs, and (2) develop access control mechanisms and prove their security. As a result, the resulting mechanisms will provide precise security guarantees and provably prevent attacks.

Contributions

Formal Semantics

We developed an operational semantics for databases that supports SQL's core features, as well as triggers, views, and integrity constraints. Our semantics models both the security-critical aspects of these features and the database's dynamic behaviour at the level needed to capture realistic attacks, and it can be used as a basis for the security proofs. An executable version of our operational semantics, implemented in the Maude framework, is available Downloadhere (GZ, 27 KB). The executable model acts as a reference implementation for our semantics. Given the complexity of databases and their features, having an executable version semantics provides a way to validate it against existing database systems.

Attacker Model

Attacker models should be studied and formalized for databases. Rather than being implicit, the relevant models must be made explicit, just like when analyzing security in other domains. In this respect, we formalized a concrete attacker model that accounts for modern database features, such as triggers and views, as well as attacker inference capabilities. In more detail, our attacker can use SQL's core features as well as advanced features such as triggers, views, and integrity constraints. He can also infer information from the database's behaviour based on the semantics of these features. Note that our attacker model can capture attacks that defeat existing database access control mechanisms. An executable version of our attacker model, implemented in the Maude framework, is available Downloadhere (GZ, 27 KB).

Security Properties

We developed two security definitions that reflect principal security requirements for database access control: integrity and confidentiality. In contrast to existing security notions, which are adequate only for the static setting where the security policy and the database are fixed, our definitions consider the database dynamics. There is a natural and intuitive relationship between our definitions and the attacks that existing databases are vulnerable to. We thus argue that our definitions provide a strong measure of whether a given access control mechanism prevents our attacker from exploiting modern SQL databases.

A Provably Secure Database Access Control Mechanism

We designed a novel database access control mechanism that prevents a number of integrity and confidentiality attacks that existing access control mechanisms are vulnerable to. By leveraging the formal foundations we developed for database access control, we formally proved that our mechanism is secure with respect to our strong, realistic attacker model and security definitions. A prototype of our mechanism can be found Downloadhere (GZ, 5.9 MB).

Theoretical Limitations of Database Access Control

We formalized Security-Aware Query Processing, the task of computing answers to queries in the presence of access control policies, and we studied the existence of optimal Security-Aware Query Processing algorithms, i.e., those algorithms that provide maximal confidentiality and data availability. We proved that there are no optimal algorithms for the relational calculus, whereas optimal algorithms exist for some of its fragments, such as the existential fragment.

Relationships between different access control semantics

We investigated the connections between two different semantics for database access control, called Truman and Non-Truman models, which have been previously presented in the literature as distinct. For optimal Security-Aware Query Processing, we proved that the Non-Truman model is a special case of the Truman model for boolean queries in the relational calculus, whereas the two models coincide for more powerful languages, such as the relational calculus with aggregation operators. In contrast, these two models are distinct for non-boolean queries.

Protecting Databases from Probabilistic Inferences

We developed foundations for database inference control in the presence of probabilistic data dependencies. Our foundations are based on Problog, a state-of-the-art probabilistic logic programming language. We leverage these foundations to develop ANGERONA, a database inference control mechanism that secures databases against attackers exploiting probabilistic dependencies. ANGERONA (available Downloadhere (GZ, 53.5 MB)) provides precise security, completeness, and tractability guarantees by exploiting a tractable inference algorithm for a practically relevant fragment of Problog.

Publications

Marco Guarnieri, Srdjan Marinovic, David A. Basin
Securing Databases from Probabilistic Inferences
in Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF 2017)
[BIB | DownloadPDF (PDF, 521 KB) | DOI | external pageExtended Version]
Marco Guarnieri, Srdjan Marinovic, and David Basin
Strong and Provably Secure Database Access Control
In Proceedings of the 1st IEEE European Symposium on Security and Privacy (EuroS&P 2016)
[DownloadBIB (BIB, 266 Bytes) | DownloadPaper (PDF, 479 KB) | DownloadExtended Version (PDF, 1 MB)]
Marco Guarnieri and David Basin
Optimal Security-Aware Query Processing
In Proceedings of the VLDB Endowment, Volume 7, Issue 12
[DownloadBIB (BIB, 365 Bytes) | DownloadPaper (PDF, 602 KB) | external pageURL]

Software and Models

Prototype of the inference-control mechanism developed in the paper "Securing Databases from Probabilistic Inference" [Downloadlink (GZ, 53.5 MB)]
Prototype of the provably secure enforcement mechanism developed in the paper "Strong and Provably Secure Database Access Control" [Downloadlink (GZ, 5.9 MB)]
Executable versions of the operational semantics and the attacker model formalized in the paper "Strong and Provably Secure Database Access Control" [Downloadlink (GZ, 27 KB)]