LMS-Verify: abstraction without regret for verified systems programming
View / Open Files
Authors
Amin, Nada
Rompf, Tiark
Publication Date
2017-05-11Journal Title
ACM SIGPLAN Notices
Conference Name
POPL 2017
ISSN
0362-1340
Publisher
Association for Computing Machinery (ACM)
Volume
52
Issue
1
Pages
859-873
Language
en
Type
Conference Object
Metadata
Show full item recordCitation
Amin, N., & Rompf, T. (2017). LMS-Verify: abstraction without regret for verified systems programming. ACM SIGPLAN Notices, 52 (1), 859-873. https://doi.org/10.1145/3093333.3009867
Abstract
<jats:p>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.</jats:p>
<jats:p>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, 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:p>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 automatically attach invariants to data types, reducing the need for repetitive manual annotations.</jats:p>
<jats:p>We 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>
Identifiers
External DOI: https://doi.org/10.1145/3093333.3009867
This record's URL: https://www.repository.cam.ac.uk/handle/1810/285136
Rights
Licence:
http://www.rioxx.net/licenses/all-rights-reserved
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.