Achieving Safety Incrementally with Checked C
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 AprDisplayed 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 |