000227178 001__ 227178
000227178 005__ 20190317000655.0
000227178 0247_ $$2doi$$a10.1145/3009837.3009867
000227178 02470 $$2ISI$$a000401538900062
000227178 02470 $$2ISI$$a000408311200064
000227178 037__ $$aCONF
000227178 245__ $$aLMS-Verify: Abstraction without Regret for Verified Systems Programming’
000227178 269__ $$a2017
000227178 260__ $$bAssoc Computing Machinery$$c2017$$aNew York
000227178 300__ $$a15
000227178 336__ $$aConference Papers
000227178 520__ $$aPerformance 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.
000227178 6531_ $$acontracts
000227178 6531_ $$ablame
000227178 6531_ $$amemory safety
000227178 6531_ $$aFrama-C
000227178 6531_ $$aLMS
000227178 6531_ $$aDSLs
000227178 6531_ $$averification
000227178 6531_ $$asecurity
000227178 700__ $$0246589$$g164625$$aAmin, Nada
000227178 700__ $$0243345$$g185682$$aRompf, Tiark
000227178 7112_ $$dJanuary 15 - 21, 2017$$cParis, France$$aPOPL 2017
000227178 773__ $$tProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
000227178 8564_ $$uhttps://infoscience.epfl.ch/record/227178/files/lms-verify.pdf$$zPostprint$$s273949$$yPostprint
000227178 909C0 $$xU10409$$0252187$$pLAMP
000227178 909CO $$ooai:infoscience.tind.io:227178$$qGLOBAL_SET$$pconf$$pIC
000227178 917Z8 $$x164625
000227178 917Z8 $$x166927
000227178 937__ $$aEPFL-CONF-227178
000227178 973__ $$rREVIEWED$$sPUBLISHED$$aEPFL
000227178 980__ $$aCONF