Axiomatising an information flow logic based on partial equivalence relations

Research output: Contribution to journalJournal articleResearchpeer-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 languageEnglish
JournalInternational Journal on Software Tools for Technology Transfer
ISSN1433-2779
DOIs
Publication statusE-pub ahead of print - 2024

Bibliographical note

Publisher Copyright:
© The Author(s) 2024.

    Research areas

  • Formal semantics, Hoare logic, Information flow, Verification

ID: 402440885