Resolving the tension between integrity and security using a theorem prover

Abstract

Some information in databases and knowledge bases often needs to be protected from disclosure to certain users. Traditional solutions involving multi-level mechanisms are threatened by the user's ability to infer higher level information from the semantics of the application. We concentrate on the revelation of secrets through a user running transactions in the presence of database integrity constraints. We develop a method of specifying secrets formally that not only exposes a useful structure and equivalence among secrets but also allows a theorem prover to detect certain security lapses during transaction compilation time.