Search Results

Documents authored by Derakhshan, Farzaneh

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.11
Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency

Authors: Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Noninterference guarantees that an attacker cannot infer secrets by interacting with a program. Information flow control (IFC) type systems assert noninterference by tracking the level of information learned (pc) and disallowing communication to entities of lesser or unrelated level than the pc. Control flow constructs such as loops are at odds with this pattern because they necessitate downgrading the pc upon recursion to be practical. In a concurrent setting, however, downgrading is not generally safe. This paper utilizes session types to track the flow of information and contributes an IFC type system for message-passing concurrent processes that allows downgrading the pc upon recursion. To make downgrading safe, the paper introduces regrading policies. Regrading policies are expressed in terms of integrity labels, which are also key to safe composition of entities with different regrading policies. The paper develops the type system and proves progress-sensitive noninterference for well-typed processes, ruling out timing attacks that exploit the relative order of messages. The type system has been implemented in a type checker, which supports security-polymorphic processes.
Cite as

Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao. Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 11:1-11:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{derakhshan_et_al:LIPIcs.ECOOP.2024.11,
  author =	{Derakhshan, Farzaneh and Balzer, Stephanie and Yao, Yue},
  title =	{{Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{11:1--11:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan 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.2024.11},
  URN =		{urn:nbn:de:0030-drops-208602},
  doi =		{10.4230/LIPIcs.ECOOP.2024.11},
  annote =	{Keywords: Regrading policies, session types, progress-sensitive noninterference}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.40
Information Flow Control in Cyclic Process Networks

Authors: Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Protection of confidential data is an important security consideration of today’s applications. Of particular concern is to guard against unintentional leakage to a (malicious) observer, who may interact with the program and draw inference from made observations. Information flow control (IFC) type systems address this concern by statically ruling out such leakage. This paper contributes an IFC type system for message-passing concurrent programs, the computational model of choice for many of today’s applications such as cloud computing and IoT applications. Such applications typically either implicitly or explicitly codify protocols according to which message exchange must happen, and to statically ensure protocol safety, behavioral type systems such as session types can be used. This paper marries IFC with session typing and contributes over prior work in the following regards: (1) support of realistic cyclic process networks as opposed to the restriction to tree-shaped networks, (2) more permissive, yet entirely secure, IFC control, exploiting cyclic process networks, and (3) considering deadlocks as another form of side channel, and asserting deadlock-sensitive noninterference (DSNI) for well-typed programs. To prove DSNI, the paper develops a novel logical relation that accounts for cyclic process networks. The logical relation is rooted in linear logic, but drops the tree-topology restriction imposed by prior work.
Cite as

Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer. Information Flow Control in Cyclic Process Networks. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 40:1-40:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{vandenheuvel_et_al:LIPIcs.ECOOP.2024.40,
  author =	{van den Heuvel, Bas and Derakhshan, Farzaneh and Balzer, Stephanie},
  title =	{{Information Flow Control in Cyclic Process Networks}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{40:1--40:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan 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.2024.40},
  URN =		{urn:nbn:de:0030-drops-208891},
  doi =		{10.4230/LIPIcs.ECOOP.2024.40},
  annote =	{Keywords: Cyclic process networks, linear session types, logical relations, deadlock-sensitive noninterference}
}
Document
Artifact
DOI: 10.4230/DARTS.10.2.4
Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency (Artifact)

Authors: Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
This artifact is a Docker image containing the snapshot of the source code, a built command-line binary, and an interactive demonstration of the type-checker developed for IFC language of the main paper. This article discusses its scope, contents and methods of use.
Cite as

Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao. Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{derakhshan_et_al:DARTS.10.2.4,
  author =	{Derakhshan, Farzaneh and Balzer, Stephanie and Yao, Yue},
  title =	{{Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency (Artifact)}},
  pages =	{4:1--4:3},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Derakhshan, Farzaneh and Balzer, Stephanie and Yao, Yue},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.4},
  URN =		{urn:nbn:de:0030-drops-209020},
  doi =		{10.4230/DARTS.10.2.4},
  annote =	{Keywords: Regrading policies, session types, progress-sensitive noninterference}
}
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact