ETAPS 2019 (series) / POST 2019 (series) / POST 2019 /
A Dependently Typed Library for Static Information-Flow Control in Idris
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 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Thu 11 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:30 | |||
10:30 30mTalk | Foundations for Parallel Information Flow Control Runtime Systems POST Marco Vassena Chalmers University of Technology, Gary Soeller , Peter Amidon , Matthew Chan , John Renner University of California, San Diego, Deian Stefan University of California San Diego Link to publication | ||
11:00 30mTalk | A Formal Analysis of Timing Channel Security via Bucketing POST Link to publication | ||
11:30 30mTalk | A Dependently Typed Library for Static Information-Flow Control in Idris POST Simon Oddershede Gregersen Aarhus University, Søren Eller Thomsen Aarhus University, Aslan Askarov Aarhus University Link to publication | ||
12:00 30mTalk | Achieving Safety Incrementally with Checked C POST Andrew Ruef , Leonidas Lampropoulos University of Pennsylvania, Ian Sweet , David Tarditi , Michael Hicks University of Maryland, College Park Link to publication | ||