kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
On Compositional Information Flow Aware Refinement
Ericsson Research Security, Kista, Sweden.ORCID iD: 0000-0003-4889-8326
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-8069-6495
Helmholtz Center for Information Security (CISPA), Saarbrücken, Germany.ORCID iD: 0000-0001-9251-3679
2021 (English)In: 2021 IEEE 34Th Computer Security Foundations Symposium (CSF 2021), Institute of Electrical and Electronics Engineers (IEEE) , 2021, p. 17-32Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE) , 2021. p. 17-32
Series
Proceedings IEEE Computer Security Foundations Symposium, ISSN 1940-1434
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-306541DOI: 10.1109/CSF51468.2021.00010ISI: 000719322000002Scopus ID: 2-s2.0-85123687961OAI: oai:DiVA.org:kth-306541DiVA, id: diva2:1621271
Conference
34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021
Projects
trustfullCERCES
Note

Part of conference proceedings ISBN 978-1-7281-7607-9

QC 20211217

Available from: 2021-12-17 Created: 2021-12-17 Last updated: 2024-03-18Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Baumann, ChristophDam, MadsGuanciale, RobertoNemati, Hamed

Search in DiVA

By author/editor
Baumann, ChristophDam, MadsGuanciale, RobertoNemati, Hamed
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 120 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf