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: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30: Covert Channels and Information FlowPOST at MOON
10:30 - 11:00
Talk
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
POST
Tachio TerauchiWaseda University, Timos AntonopoulosYale University
Link to publication
11:30 - 12:00
Talk
POST
Simon GregersenAarhus University, Søren Eller ThomsenAarhus University, Aslan AskarovAarhus University
Link to publication
12:00 - 12:30
Talk
POST
Andrew Ruef, Leonidas LampropoulosUniversity of Pennsylvania, Ian Sweet, David Tarditi, Michael HicksUniversity of Maryland, College Park
Link to publication