POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 16:30 - 16:55 at Auditorium - Security and Privacy Chair(s): Cătălin Hriţcu

Performance critical software is almost always developed in C, as programmers do not trust high-level languages to deliver the same reliable performance. This is bad because low-level code in unsafe languages attracts security vulnerabilities and because development is far less productive, with PL advances mostly lost on programmers operating under tight performance constraints. High-level languages provide memory safety out of the box, but they are deemed too slow and unpredictable for serious system software.

Recent years have seen a surge in staging and generative programming: the key idea is to use high-level languages and their abstraction power as glorified macro systems to compose code fragments in first-order, domain-specific, intermediate languages, from which fast C can be emitted. But what about security? Since the end result is still C code, the safety guarantees of the high-level host language are lost.

In this paper we extend this generative approach to emit ACSL specifications along with C code. We demonstrate that staging achieves ``abstraction without regret'' for verification: we show how high-level programming models, in particular higher-order composable contracts from dynamic languages, can be used at generation time to compose and generate first-order specifications that can be statically checked by existing tools. We also show how type-classes can be used to automatically attach specifications to data types.

We evaluate our system on several case studies, including an HTTP parser that is (1) fast (2) high-level: implemented using staged parser combinators (3) secure: with verified memory safety. This result is significant, as input parsing is a key attack vector, and vulnerabilities related to HTTP parsing have been documented in all widely-used web servers.

Fri 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:30 - 17:45
Security and PrivacyPOPL at Auditorium
Chair(s): Cătălin Hriţcu Inria Paris
LMS-Verify: Abstraction Without Regret for Verified Systems Programming
Nada Amin EPFL, Tiark Rompf Purdue University
Hypercollecting Semantics and its Application to Static Analysis of Information Flow
Mounir Assaf Stevens Institute of Technology, David Naumann Stevens Institute of Technology, Julien Signoles CEA LIST, Éric Totel CentraleSupélec, Frédéric Tronel CentraleSupélec
LightDP: Towards Automating Differential Privacy Proofs
Danfeng Zhang Pennsylvania State University, Daniel Kifer Dept. of Computer Science and Engineering, Penn State University