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

POPL-2017-papers
16:30 - 17:45: POPL - Security and Privacy at Auditorium
Chair(s): Cătălin HriţcuInria Paris
POPL-2017-papers16:30 - 16:55
Talk
Nada AminEPFL, Tiark RompfPurdue University
POPL-2017-papers16:55 - 17:20
Talk
Mounir AssafStevens Institute of Technology, David NaumannStevens Institute of Technology, Julien SignolesCEA LIST, Éric TotelCentraleSupélec, Frédéric TronelCentraleSupélec
POPL-2017-papers17:20 - 17:45
Talk
Danfeng ZhangPennsylvania State University, Daniel KiferDept. of Computer Science and Engineering, Penn State University