WG211/M16SRomph

Tiark Romph

LMS-Verify: Abstraction Without Regret for Verified Systems Programming

Recent years have seen a surge in staging and generative programming for performance: 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 correctness of the generator, and security? Since the end result is still C code, the safety guarantees of the high-level host language are lost.

In recent work, we have shown that what makes staging attractive for performance also holds for verification. We emit ACSL specifications along with C codeto achieve ``abstraction without regret for verification: 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. Type classes can automatically attach invariants to data types, reducing the need for repetitive manual annotations.

We have implemented several case studies that varyingly exercise verification of memory safety, overflow safety, and functional correctness. The most interesting one is 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.