Provably secure access and inference control in databases

Databases often store and manage sensitive data. Regulating the access to databases is, therefore, essential. To this end, researchers have developed both access control and inference control mechanisms. Ideally, all these mechanisms should come with security proofs clearly stating what attacks they are designed to thwart, as with security mechanisms in other domains. Unfortunately, this is far from reality. Existing mechanisms are implemented in an ad hoc fashion, with neither precise security guarantees nor the means to verify them. This has immediate consequences as existing mechanisms are inadequate to secure modern databases and are susceptible to attacks.

Goals

This project’s goals are (1) research and develop solid theoretical foundations for access and inference control in modern database systems, and (2) leverage these foundations to design security mechanisms that are provably secure. More strongly, we argue that all database security mechanisms must offer security proofs to clearly state what attacks and attackers they are designed to thwart.

Our approach is to 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 develop enforcement mechanisms and prove their security. As a result, the resulting mechanisms will provide precise security guarantees and provably prevent attacks.