ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Thu 11 Apr 2019 11:30 - 12:00 at MOON - Covert Channels and Information Flow

Safely integrating third-party code in applications while protecting the confidentiality of information is a long-standing problem. Pure functional programming languages, like Haskell, make it possible to enforce lightweight information-flow control through libraries like MAC by Russo. This work presents DepSec, a MAC inspired, dependently typed library for static information- flow control in Idris. We showcase how adding dependent types increases the expressiveness of state-of-the-art static information-flow control libraries and how DepSec matches a special-purpose dependent information-flow type system on a key example. Finally, we show novel and powerful means of specifying statically enforced declassification policies.

Thu 11 Apr
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30: Covert Channels and Information FlowPOST at MOON
10:30 - 11:00
Talk
Foundations for Parallel Information Flow Control Runtime Systems
POST
Marco VassenaChalmers University of Technology, Gary Soeller, Peter Amidon, Matthew Chan, John RennerUniversity of California, San Diego, Deian StefanUniversity of California San Diego
Link to publication
11:00 - 11:30
Talk
A Formal Analysis of Timing Channel Security via Bucketing
POST
Tachio TerauchiWaseda University, Timos AntonopoulosYale University
Link to publication
11:30 - 12:00
Talk
A Dependently Typed Library for Static Information-Flow Control in Idris
POST
Simon Oddershede GregersenAarhus University, Søren Eller ThomsenAarhus University, Aslan AskarovAarhus University
Link to publication
12:00 - 12:30
Talk
Achieving Safety Incrementally with Checked C
POST
Andrew Ruef, Leonidas LampropoulosUniversity of Pennsylvania, Ian Sweet, David Tarditi, Michael HicksUniversity of Maryland, College Park
Link to publication