1 Search Results for "Cecchetti, Ethan"

Document
DOI: 10.4230/LIPIcs.ECOOP.2023.29
Semantics for Noninterference with Interaction Trees

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

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

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.
Cite as

Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic. Semantics for Noninterference with Interaction Trees. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 29:1-29:29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.ECOOP.2023.29},
  URN =		{urn:nbn:de:0030-drops-182227},
  doi =		{10.4230/LIPIcs.ECOOP.2023.29},
  annote =	{Keywords: verification, information-flow, denotational semantics, monads}
}
  • Refine by Author
  • 1 Cecchetti, Ethan
  • 1 He, Paul
  • 1 Hirsch, Andrew K.
  • 1 Silver, Lucas
  • 1 Zdancewic, Steve

  • Refine by Classification
  • 1 Security and privacy → Information flow control
  • 1 Security and privacy → Logic and verification
  • 1 Theory of computation → Denotational semantics

  • Refine by Keyword
  • 1 denotational semantics
  • 1 information-flow
  • 1 monads
  • 1 verification

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact