cispa_all_3213.pdf (493.72 kB)

On Compositional Information Flow Aware Refinement

Download (493.72 kB)
conference contribution
posted on 2023-11-29, 18:15 authored by Christoph Baumann, Mads Dam, Roberto Guanciale, Hamed Nemati
The concepts of information flow security and refinement are known to have had a troubled relationship ever since the seminal work of McLean. In this work we study refinements that support changes in data representation and semantics, including the addition of state variables that may induce new observational power or side channels. We propose a new epistemic approach to ignorance-preserving refinement where an abstract model is used as a specification of a system’s permitted information flows, that may include the declassification of secret information. The core idea is to require that refinement steps must not induce observer knowledge that is not already available in the abstract model. Our study is set in the context of a class of shared variable multi-agent models similar to interpreted systems in epistemic logic. We demonstrate the expressiveness of our framework through a series of small examples and compare our approach to existing, stricter notions of information-flow secure refinement based on bisimulations and noninterference preservation. Interestingly, noninterference preservation is not supported “out of the box” in our setting, because refinement steps may introduce new secrets that are independent of secrets already present at abstract level. To support verification, we first introduce a “cube-shaped” unwinding condition related to conditions recently studied in the context of value-dependent noninterference, kernel verification, and secure compilation. A fundamental problem with ignorance-preserving refinement, caused by the support for general data and observation refinement, is that sequential composability is lost. We propose a solution based on relational pre- and post-conditions and illustrate its use together with unwinding on the oblivious RAM construction of Chung and Pass.


Preferred Citation

Christoph Baumann, Mads Dam, Roberto Guanciale and Hamed Nemati. On Compositional Information Flow Aware Refinement. In: IEEE Computer Security Foundations Symposium (CSF). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

IEEE Computer Security Foundations Symposium (CSF)

Legacy Posted Date


Open Access Type

  • Unknown


@inproceedings{cispa_all_3213, title = "On Compositional Information Flow Aware Refinement", author = "Baumann, Christoph and Dam, Mads and Guanciale, Roberto and Nemati, Hamed", booktitle="{IEEE Computer Security Foundations Symposium (CSF)}", year="2021", }

Usage metrics


    No categories selected


    Ref. manager