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

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