2 Search Results for "Hirsch, Andrew K."

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}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2019.11
A Tour of Gallifrey, a Language for Geodistributed Programming

Authors: Mae Milano, Rolph Recto, Tom Magrino, and Andrew C. Myers

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)

Abstract
Programming efficient distributed, concurrent systems requires new abstractions that go beyond traditional sequential programming. But programmers already have trouble getting sequential code right, so simplicity is essential. The core problem is that low-latency, high-availability access to data requires replication of mutable state. Keeping replicas fully consistent is expensive, so the question is how to expose asynchronously replicated objects to programmers in a way that allows them to reason simply about their code. We propose an answer to this question in our ongoing work designing a new language, Gallifrey, which provides orthogonal replication through _restrictions_ with _merge strategies_, _contingencies_ for conflicts arising from concurrency, and _branches_, a novel concurrency control construct inspired by version control, to contain provisional behavior.
Cite as

Mae Milano, Rolph Recto, Tom Magrino, and Andrew C. Myers. A Tour of Gallifrey, a Language for Geodistributed Programming. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 11:1-11:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{milano_et_al:LIPIcs.SNAPL.2019.11,
  author =	{Milano, Mae and Recto, Rolph and Magrino, Tom and Myers, Andrew C.},
  title =	{{A Tour of Gallifrey, a Language for Geodistributed Programming}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.11},
  URN =		{urn:nbn:de:0030-drops-105549},
  doi =		{10.4230/LIPIcs.SNAPL.2019.11},
  annote =	{Keywords: programming languages, distributed systems, weak consistency, linear types}
}
  • Refine by Author
  • 1 Cecchetti, Ethan
  • 1 He, Paul
  • 1 Hirsch, Andrew K.
  • 1 Magrino, Tom
  • 1 Milano, Mae
  • Show More...

  • Refine by Classification
  • 1 Security and privacy → Information flow control
  • 1 Security and privacy → Logic and verification
  • 1 Software and its engineering → Cooperating communicating processes
  • 1 Software and its engineering → Distributed programming languages
  • 1 Software and its engineering → Massively parallel systems
  • Show More...

  • Refine by Keyword
  • 1 denotational semantics
  • 1 distributed systems
  • 1 information-flow
  • 1 linear types
  • 1 monads
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2019
  • 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