Access Hoare Logic
This work provides a new foundational framework for access control reasoning, but it is an initial proposal without empirical validation or comparison to existing methods.
The paper introduces Access Hoare Logic, a formalism for reasoning about access security in computer programs, distinct from standard Hoare logic. It proves soundness and completeness and demonstrates its utility through examples.
Following Hoare's seminal invention, now called Hoare logic, to reason about correctness of computer programs, we advocate a related but fundamentally different approach to reason about access security of computer programs such as access control. We define the formalism, which we denote access Hoare logic, and present examples which demonstrate its usefulness and fundamental difference to Hoare logic. We prove soundness and completeness of access Hoare logic, and provide a link between access Hoare logic and standard Hoare logic. We also demonstrate a fundamental difference of access Hoare logic to other approaches, in particular incorrectness logic.