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

Checked C is a new effort working toward a memory-safe C. Its design is distinguished from that of prior efforts by truly being an extension of C: Every C program is also a Checked C program. Thus, one may make incremental safety improvements to existing codebases while retaining backward compatibility. This paper makes two contributions. First, to help developers convert existing C code to use so-called checked (i.e., safe) pointers, we have developed an automated porting tool. Notably, this tool takes advantage of the flexibility of Checked C’s design: The tool need not perfectly classify every pointer, as required of prior all-or-nothing efforts. Rather, it can make a best effort to convert more pointers accurately, without letting inaccuracies inhibit compilation. However, such partial conversion raises the question: If safety violations can still occur, what sort of advantage does using Checked C provide? We draw inspiration from research on migratory typing to make our second contribution: We prove a blame property that renders so-called checked regions blameless of any run-time failure. We formalize this property for a core calculus and mechanize the proof in Coq.

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
30m
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
30m
Talk
A Formal Analysis of Timing Channel Security via Bucketing
POST
Tachio TerauchiWaseda University, Timos AntonopoulosYale University
Link to publication
11:30
30m
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
30m
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