dc.contributor.author Amin, Nada en dc.contributor.author Rompf, Tiark en dc.date.accessioned 2018-11-16T00:30:56Z dc.date.available 2018-11-16T00:30:56Z dc.date.issued 2017-05-11 en dc.identifier.issn 0362-1340 dc.identifier.uri https://www.repository.cam.ac.uk/handle/1810/285136 dc.description.abstract 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, 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. 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. 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. dc.language en en dc.title LMS-Verify: abstraction without regret for verified systems programming en dc.type Conference Object prism.endingPage 873 prism.issueIdentifier 1 en prism.publicationDate 2017 en prism.publicationName ACM SIGPLAN Notices en prism.startingPage 859 prism.volume 52 en dc.identifier.doi 10.17863/CAM.32507 rioxxterms.versionofrecord 10.1145/3093333.3009867 en rioxxterms.licenseref.uri http://www.rioxx.net/licenses/all-rights-reserved en rioxxterms.licenseref.startdate 2017-05-11 en dc.identifier.eissn 1558-1160 rioxxterms.type Conference Paper/Proceeding/Abstract en rioxxterms.freetoread.startdate 2018-12-25
﻿