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

Filinski, A, Larsen, KF & Jensen, TP 2024, 'Axiomatising an information flow logic based on partial equivalence relations', International Journal on Software Tools for Technology Transfer. https://doi.org/10.1007/s10009-024-00756-z

APA

Filinski, A., Larsen, K. F., & Jensen, T. P. (2024). Axiomatising an information flow logic based on partial equivalence relations. International Journal on Software Tools for Technology Transfer. https://doi.org/10.1007/s10009-024-00756-z

Vancouver

Filinski A, Larsen KF, Jensen TP. Axiomatising an information flow logic based on partial equivalence relations. International Journal on Software Tools for Technology Transfer. 2024. https://doi.org/10.1007/s10009-024-00756-z

Author

Filinski, Andrzej ; Larsen, Ken Friis ; Jensen, Thomas P. / Axiomatising an information flow logic based on partial equivalence relations. In: International Journal on Software Tools for Technology Transfer. 2024.

Bibtex

@article{6cc3192e9b934c91bec0d78483cedb40,
title = "Axiomatising an information flow logic based on partial equivalence relations",
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.",
keywords = "Formal semantics, Hoare logic, Information flow, Verification",
author = "Andrzej Filinski and Larsen, {Ken Friis} and Jensen, {Thomas P.}",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2024.",
year = "2024",
doi = "10.1007/s10009-024-00756-z",
language = "English",
journal = "Software-Concepts and Tools",
issn = "1433-2779",
publisher = "Springer",

}

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