Show simple item record

dc.contributor.authorAmin, Nadaen
dc.contributor.authorRompf, Tiarken
dc.date.accessioned2018-11-16T00:30:56Z
dc.date.available2018-11-16T00:30:56Z
dc.date.issued2017-05-11en
dc.identifier.issn0362-1340
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/285136
dc.description.abstractPerformance 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.languageenen
dc.titleLMS-Verify: abstraction without regret for verified systems programmingen
dc.typeConference Object
prism.endingPage873
prism.issueIdentifier1en
prism.publicationDate2017en
prism.publicationNameACM SIGPLAN Noticesen
prism.startingPage859
prism.volume52en
dc.identifier.doi10.17863/CAM.32507
rioxxterms.versionofrecord10.1145/3093333.3009867en
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserveden
rioxxterms.licenseref.startdate2017-05-11en
dc.identifier.eissn1558-1160
rioxxterms.typeConference Paper/Proceeding/Abstracten
rioxxterms.freetoread.startdate2018-12-25


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record