DARTS.9.2.6.pdf
- Filesize: 476 kB
- 2 pages
Document
Semantics for Noninterference with Interaction Trees (Artifact)
Authors
Paul He 
,
Ethan Cecchetti ,
Andrew K. Hirsch ,
Steve Zdancewic
-
Part of:
Issue:
Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)
Volume: DARTS, Volume 9 (ECOOP 2023)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-11
Artifact Description
Document Identifiers
Author Details
- University of Maryland, College Park, MD, USA
- University of Wisconsin - Madison, WI, USA
Acknowledgements
This work was funded in part by the NSF under the award 1521539 (Weirich, Zdancewic, Pierce).
Cite As Get BibTex
Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic. Semantics for Noninterference with Interaction Trees (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 6:1-6:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/DARTS.9.2.6
Artifact
DARTS-9-2-6-artifact-b4f158914476b56f95cced770ccc355c.tar.gz
(Filesize: 0.99 GB)
MD5 Sum:
b4f158914476b56f95cced770ccc355c
(Get MD5 Sum)
Artifact Evaluation Policy
The artifact has been evaluated as described in the ECOOP 2023 Call for Artifacts and the ACM Artifact Review and Badging Policy
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Denotational semantics
- Security and privacy → Logic and verification
- Security and privacy → Information flow control
Keywords
- verification
- information-flow
- denotational semantics
- monads
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads