We found a match
Your institution may have rights to this item. Sign in to continue.
- Title
Axiomatising an information flow logic based on partial equivalence relations.
- Authors
Filinski, Andrzej; Larsen, Ken Friis; Jensen, Thomas P.
- Abstract
We present a relational program logic for reasoning about information flow properties formalised in an assertion language based on partial equivalence relations. We define and prove the soundness of the logic, a proof technique for precise, logic-based information flow properties. The logic extends Hoare logic and its unary state predicates to binary PER-based predicates for relating observationally equivalent states. A salient feature of the logic is that it is capable of reasoning about programs that test on secret data in a secure manner.
- Subjects
SEMANTICS
- Publication
International Journal on Software Tools for Technology Transfer, 2024, Vol 26, Issue 4, p445
- ISSN
1433-2779
- Publication type
Article
- DOI
10.1007/s10009-024-00756-z