Axiomatising an information flow logic based on partial equivalence relations
Research output: Contribution to journal › Journal article › Research › peer-review
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.
Original language | English |
---|---|
Journal | International Journal on Software Tools for Technology Transfer |
ISSN | 1433-2779 |
DOIs | |
Publication status | E-pub ahead of print - 2024 |
Bibliographical note
Publisher Copyright:
© The Author(s) 2024.
- Formal semantics, Hoare logic, Information flow, Verification
Research areas
ID: 402440885