2026-07-22T13:11:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18222 2024-03-06T11:01:25Z ddc:004 open_access

Semantics for Noninterference with Interaction Trees Silver, Lucas He, Paul Cecchetti, Ethan Hirsch, Andrew K. Zdancewic, Steve verification information-flow denotational semantics monads 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lucas Silver and Paul He and Ethan Cecchetti and Andrew K. Hirsch and Steve Zdancewic 2023 Is Part Of LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2023.29 urn:nbn:de:0030-drops-182227 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.29 eng https://creativecommons.org/licenses/by/4.0/legalcode