ECOOP 2024
Mon 16 - Fri 20 September 2024 Vienna, Austria
co-located with ISSTA/ECOOP 2024
Mon 16 Sep 2024 13:45 - 14:00 at EI 7 - Types 1

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 using local security theories.

Mon 16 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
13:30
15m
Talk
Behavioral up/down casting for statically typed languages
Technical Papers
Lorenzo Bacchiani University of Bologna, Mario Bravetti Università di Bologna, Marco GIUNTI University of Oxford, João Mota NOVA School of Science and Technology, António Ravara Nova University of Lisbon
13:45
15m
Talk
Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency
Technical Papers
Farzaneh Derakhshan Illinois Institute of Technology, Stephanie Balzer Carnegie Mellon University, Yue Yao Carnegie Mellon University
14:00
15m
Talk
Ozone: Fully Out-of-Order Choreographies
Technical Papers
Dan Plyukhin University of Southern Denmark, Marco Peressotti University of Southern Denmark, Fabrizio Montesi University of Southern Denmark
Pre-print
14:15
15m
Talk
Information Flow Control in Cyclic Process Networks
Technical Papers
Bas van den Heuvel Karlsruhe University of Applied Sciences, University of Freiburg, Farzaneh Derakhshan Illinois Institute of Technology, Stephanie Balzer Carnegie Mellon University
14:30
15m
Talk
Formalizing, Mechanizing, and Verifying Class-based Refinement Types
Technical Papers
Ke Sun Peking University, Di Wang Peking University, Sheng Chen UL Lafayette, Meng Wang University of Bristol, Dan Hao Peking University
14:45
15m
Talk
Pure methods for roDOT
Technical Papers
Vlastimil Dort Charles University, Yufeng Li University of Waterloo, Ondřej Lhoták University of Waterloo, Pavel Parizek Charles University

Information for Participants
Mon 16 Sep 2024 13:30 - 15:00 at EI 7 - Types 1
Info for room EI 7:

Map: https://tuw-maps.tuwien.ac.at/?q=CDEG13

Room tech: https://raumkatalog.tiss.tuwien.ac.at/room/15417