Preprocessing for controlled query evaluation in complete first-order databases

Abstract

This dissertation investigates a mechanism for confidentiality preservation in first-order logic databases. The logical basis is given by the inference control framework of Controlled Query Evaluation (CQE). Beyond traditional access control, CQE incorporates an explicit representation of a user's knowledge and his ability to reason with information; it hence prevents disclosure of confidential information that would occur due to inferences drawn by the user. This thesis pioneers a new approach in the CQE context: An unprotected database instance is transformed into an inference-proof instance that does not reveal confidential information; the inference-proof instance formally guarantees confidentiality with respect to a representation of user knowledge and a specification of confidential information. Hence, inference-proofness ensures that all user queries can truthfully be answered by the database; no sequence of responses enables the user to infer confidential information. Due to this concept, query evaluation on the inference-proof instance does not incur any performance degradation. As a second design goal, the availability requirement to maintain as much as possible of the correct information in the input database is accounted for by minimization of a distortion distance. The transformation modifies the input instance to provide the user with a consistent view of the data. The algorithm relies on query evaluation on the database to efficiently identify those tuples that are to be added or deleted. Due to undecidability of the general first-order case, appropriate fragments are analyzed. The formalization is started with universal formulas (for which a restriction to allowed formulas is chosen); it moves on to existential formulas and then finishes up with tuple-generating dependencies accompanied by existential and denial formulas. The due proofs of refutation soundness engage a version of Herbrand's theorem with semantic trees. An effort was made to present a broad background of related work. Last but not least, exposition and analysis of a prototypical implementation prove practicality of the approach.