Semantics for Noninterference with Interaction Trees (Artifact)

Authors Lucas Silver, Paul He , Ethan Cecchetti , Andrew K. Hirsch , Steve Zdancewic

Thumbnail PDF

Artifact Description

  • Filesize: 476 kB
  • 2 pages

Document Identifiers

Author Details

Lucas Silver
  • University of Pennsylvania, Philadelphia, PA, USA
Paul He
  • University of Pennsylvania, Philadelphia, PA, USA
Ethan Cecchetti
  • University of Maryland, College Park, MD, USA
  • University of Wisconsin - Madison, WI, USA
Andrew K. Hirsch
  • State University of New York at Buffalo, NY, USA
Steve Zdancewic
  • University of Pennsylvania, Philadelphia, PA, USA


This work was funded in part by the NSF under the award 1521539 (Weirich, Zdancewic, Pierce).

Cite AsGet 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)


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


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
  • verification
  • information-flow
  • denotational semantics
  • monads


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads