Repository logo
 

LMS-Verify: abstraction without regret for verified systems programming

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Amin, Nada 
Rompf, Tiark 

Abstract

jats:pPerformance 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.</jats:p>jats:pRecent 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, potentially 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.</jats:p>jats:pIn 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 automatically attach invariants to data types, reducing the need for repetitive manual annotations.</jats:p>jats:pWe evaluate our system on several case studies that varyingly exercise verification of memory safety, overflow safety, and functional correctness. We feature 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.</jats:p>

Description

Keywords

4613 Theory Of Computation, 46 Information and Computing Sciences, 4612 Software Engineering

Journal Title

ACM SIGPLAN Notices

Conference Name

POPL 2017

Journal ISSN

0362-1340
1558-1160

Volume Title

52

Publisher

Association for Computing Machinery (ACM)