License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2023.29
URN: urn:nbn:de:0030-drops-182227
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18222/
Silver, Lucas ;
He, Paul ;
Cecchetti, Ethan ;
Hirsch, Andrew K. ;
Zdancewic, Steve
Semantics for Noninterference with Interaction Trees
Abstract
Noninterference is the strong information-security property that a program does not leak secrets through publicly-visible behavior. In the presence of effects such as nontermination, state, and exceptions, reasoning about noninterference quickly becomes subtle. We advocate using interaction trees (ITrees) to provide compositional mechanized proofs of noninterference for multi-language, effectful, nonterminating programs, while retaining executability of the semantics. We develop important foundations for security analysis with ITrees: two indistinguishability relations, leading to two standard notions of noninterference with adversaries of different strength, along with metatheory libraries for reasoning about each. We demonstrate the utility of our results using a simple imperative language with embedded assembly, along with a compiler into that assembly language.
BibTeX - Entry
@InProceedings{silver_et_al:LIPIcs.ECOOP.2023.29,
author = {Silver, Lucas and He, Paul and Cecchetti, Ethan and Hirsch, Andrew K. and Zdancewic, Steve},
title = {{Semantics for Noninterference with Interaction Trees}},
booktitle = {37th European Conference on Object-Oriented Programming (ECOOP 2023)},
pages = {29:1--29:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-281-5},
ISSN = {1868-8969},
year = {2023},
volume = {263},
editor = {Ali, Karim and Salvaneschi, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18222},
URN = {urn:nbn:de:0030-drops-182227},
doi = {10.4230/LIPIcs.ECOOP.2023.29},
annote = {Keywords: verification, information-flow, denotational semantics, monads}
}
