research-article

Public Access

LMS-Verify: abstraction without regret for verified systems programming

Authors:

Nada Amin,

Tiark RompfAuthors Info & Claims

POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Pages 859 - 873

https://doi.org/10.1145/3009837.3009867

Published: 01 January 2017 Publication History

PDF eReader

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.

References

[1]

M. Abadi, M. Budiu, Ú. Erlingsson, and J. Ligatti. Control-flow integrity. In ACM Conference on Computer and Communications Security, pages 340–353. ACM, 2005.

Abstract

References

Cited By

Index Terms

Recommendations

LMS-Verify: abstraction without regret for verified systems programming

Compiling c programs into a strongly typed assembly language

Verified peephole optimizations for CompCert

Comments

Information

Published In

Sponsors

In-Cooperation

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Funding Sources

Conference

Acceptance Rates

Upcoming Conference

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations