Access Hoare Logic

TL;DR

This paper introduces access Hoare logic, a formal system for reasoning about access security in computer programs, establishing its soundness, completeness, and relation to standard Hoare logic.

Contribution

It presents a new formalism called access Hoare logic, demonstrating its usefulness, fundamental differences from Hoare logic, and connection to other approaches like incorrectness logic.

Findings

Proves soundness and completeness of access Hoare logic.

Provides examples demonstrating its usefulness.

Shows fundamental differences from other approaches.

Abstract

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.