Information Flow Control in Cyclic Process Networks
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.
Mon 16 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | Types 1Technical Papers at EI 7 Chair(s): Emilio Tuosto Gran Sasso Science Institute, L'Aquila, Italy | ||
13:30 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 |