Axiomatising an information flow logic based on partial equivalence relations
Research output: Contribution to journal › Journal article › Research › peer-review
Standard
Axiomatising an information flow logic based on partial equivalence relations. / Filinski, Andrzej; Larsen, Ken Friis; Jensen, Thomas P.
In: International Journal on Software Tools for Technology Transfer, 2024.Research output: Contribution to journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Axiomatising an information flow logic based on partial equivalence relations
AU - Filinski, Andrzej
AU - Larsen, Ken Friis
AU - Jensen, Thomas P.
N1 - Publisher Copyright: © The Author(s) 2024.
PY - 2024
Y1 - 2024
N2 - 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.
AB - 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.
KW - Formal semantics
KW - Hoare logic
KW - Information flow
KW - Verification
U2 - 10.1007/s10009-024-00756-z
DO - 10.1007/s10009-024-00756-z
M3 - Journal article
AN - SCOPUS:85196819900
JO - Software-Concepts and Tools
JF - Software-Concepts and Tools
SN - 1433-2779
ER -
ID: 402440885