PaperlayerView exact revision on arXiv

Source-linked AI summary

Verified Low-Level Programming Embedded in F*

Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy

arXiv:1703.00053v6cs.PLcs.CR

TL;DR

Low* addresses the challenge of combining high-level verification with efficient low-level cryptographic code. It embeds a C-like language and memory model in F*, compiles verified programs to C, and evaluates the approach on cryptographic libraries and constructions. The resulting code achieves performance on par with existing C code while supporting memory-safety, functional-correctness, and security proofs.

  • Problem

    High-performance cryptographic software remains vulnerable to attacks, while high-level safe-by-construction code may lack low-level control and can lose guarantees when linked with vulnerable C.

  • Method

    Low* embeds a C-like low-level language and structured memory model in F*, using F* verification to prove memory safety, functional correctness, and security properties before compiling to C.

  • Results

    The authors apply Low* to verified cryptographic algorithms, libraries, and TLS 1.3 AEAD constructions, with compiled code performing on par with existing C code.

  • Takeaways & Limitations

    Low* supports modular high-level proofs for low-level code while retaining performance comparable to hand-written C and enabling integration with existing software.

Abstract

from arXiv · show

We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, well-behaved subset of C in F*, a dependently-typed variant of ML aimed at program verification. Departing from ML, Low* does not involve any garbage collection or implicit heap allocation; instead, it has a structured memory model à la CompCert, and it provides the control required for writing efficient low-level security-critical code. By virtue of typing, any Low* program is memory safe. In addition, the programmer can make full use of the verification power of F* to write high-level specifications and verify the functional correctness of Low* code using a combination of SMT automation and sophisticated manual proofs. At extraction time, specifications and proofs are erased, and the remaining code enjoys a predictable translation to C. We prove that this translation preserves semantics and side-channel resistance. We provide a new compiler back-end from Low* to C and, to evaluate our approach, we implement and verify various cryptographic algorithms, constructions, and tools for a total of about 28,000 lines of code, specification and proof. We show that our Low* code delivers performance competitive with existing (unverified) C cryptographic libraries, suggesting our approach may be applicable to larger-scale low-level software.

1 INTRODUCTION

Low* embeds efficient low-level programming in F*, combining C-like control and memory modeling with F* verification. The paper presents formal translation and compiler support, then evaluates the approach on verified cryptographic software and applications.

  • Low* bridges high-level, safe-by-construction code and low-level code with fine control over data representation and memory layout.
  • Low* programs use a structured, CompCert-like memory model and interoperate with F* specifications and code.
  • The formal translation to CompCert Clight preserves trace equivalence, functional behavior, and source-level side-channel resistance.
  • KreMLin compiles Low* to well-formatted C, which can be compiled with CompCert or mainstream C compilers and integrated through standard means.
  • The evaluation covers efficient verified cryptographic libraries, including HACL* and TLS 1.3 AEAD implementations, with about 20,000+ lines of Low* code extracted to C.
  • The trusted computing base includes the F* typechecker, Z3, manual metatheory proofs, unverified KreMLin, and the C compiler.

2 A LOW∗TUTORIAL

Low∗ combines a structured low-level memory model with F∗ specifications and typing to verify safe, functionally correct, and side-channel-resistant code. The tutorial illustrates these mechanisms through buffers, structs, cryptographic implementations, and proofs for Poly1305 and AEAD.

  • Memory model: Low∗’s core library models manually allocated arrays and structs while supporting reasoning about object extents, liveness, and contents.KreMLin compiles verified client code using these abstractions to C.
  • Verification: Type refinements and specifications enforce safe buffer use by constraining lengths, liveness, allocation effects, and postconditions.The ChaCha20 example uses stack-only allocation, fixed-size buffers, and preconditions that rule out buffer overruns.
  • Buffers: Refinement types translate bounded Low∗ buffers into native C arrays while preserving length information for verification.A buffer refinement such as length b = n is translated into uint32_t b[n] and then used through C pointer decay.
  • Structs: The memory model supports C-style structs with field-indexed pointers, enabling navigation through nested fields without unrestricted pointer arithmetic.Structs are represented as contiguous memory blocks, while the library exposes paths through fields.
  • Security: Low∗ uses type abstraction and secret-independent control flow and memory access patterns to support side-channel-resistant cryptographic code.The approach formalizes source-level secret independence and carries it through compilation to Clight.
  • Cryptographic proofs: The Poly1305 implementation proves that its output tag equals a mathematical specification, while the AEAD development verifies ideal-cipher behavior and nonce non-reuse.These proofs connect low-level implementations to functional and cryptographic specifications.

3 A FORMAL TRANSLATION FROM LOW∗TO CLIGHT

The formal pipeline translates Low* through λow*, C*, and CompCert Clight while preserving safety, functional behavior, and traces relevant to side-channel resistance. The core language models structured memory and secret-independent traces, with stated limitations around heap formalization and nested arrays.

  • 3 A FORMAL TRANSLATION FROM LOW∗TO CLIGHT: The translation pipeline proceeds from emf⋆ through λow∗ and C∗ to CompCert Clight after erasing ghost code and specifications.The formal development establishes semantics-preserving stages and connects verified F* properties to generated Clight code.
  • 3 A FORMAL TRANSLATION FROM LOW∗TO CLIGHT: The transcription to λow∗ uses first-order terms with stack memory only, leaving heap behavior outside the formal core proof.The authors identify this transcription as straightforward but not backed by a specific proof and leave mechanization for future work.
  • 3.1 λow∗: A Formal Core of Low∗Post-Erasure: λow∗ is a first-order stateful language whose stack of memory regions produces traces recording branches and accessed memory addresses.These traces model potential leaks through program-counter and cache-related memory-access behavior.
  • 3.1 λow∗: A Formal Core of Low∗Post-Erasure: Its syntax supports stack buffers, mutable structures, and field paths, but arbitrary nesting of arrays within mutable structures requires explicit indirection.The generalization to direct arbitrary nesting is left as future work.
  • 3.1 λow∗: A Formal Core of Low∗Post-Erasure: Secret independence requires implementations of abstract secret interfaces to preserve related values and memories, yielding identical progress behavior and traces.The theorem compares well-typed substitutions and states that either both executions stop or both proceed with the same trace.
  • 3.2 C∗: An Intermediate Language: The λow∗-to-C∗ transformation exactly preserves execution traces, and safe λow∗ programs produce safe C∗ programs.The proof uses bisimulation, with quasi-refinement allowing temporary step mismatches caused by C∗'s big-step expression semantics.
  • 3.3 From C∗to CompCert Clight and Beyond: Structure erasure improves the benchmark by 20% relative to its absence under CompCert 2.7.Without structure erasure, CompCert-generated code is reported as 60% slower than gcc -O1 and may suffer stack overflow.

4 KREMLIN: A COMPILER FROM LOW∗TO C

KreMLin compiles erased Low* programs through intermediate representations into readable, portable C while preserving predictable interfaces and integration paths.

  • Compilation pipeline: KreMLin transforms extracted Low* terms into λow*, then C* and C, producing C11 files compilable by GCC, Clang, Microsoft’s compiler, or CompCert.The pipeline includes pretty-printing to a set of C files.
  • Data representation: KreMLin translates F* tuples and inductive types into specialized C structs, enums, tagged unions, and corresponding control flow.Pattern matches become switches, let-bindings, or cascading conditionals.
  • Whole-program transformations: Whole-program transformations substitute parameterized type abbreviations, bundle modules into translation units, and mark internal functions static to enable C-compiler optimizations.Only functions reachable through the distinguished API module remain externally visible.
  • Statement translation: KreMLin stratifies allocations, assignments, and conditionals and hoists buffers to reconcile Low* lifetimes with C99 block scope.Hoisting prevents a buffer allocated under a branch from outliving its enclosing frame incorrectly.
  • Readability and integration: KreMLin preserves names and uses idiomatic C constructs to generate readable code that security experts can review.Its output depends only on one header and C11 standard headers, enabling integration into existing source trees.
  • Readability and integration: Generated libraries expose predictable C headers and comply with the C ABI, supporting drop-in replacement and foreign-function interfaces.Hand-written bindings can improve performance and control but require potentially error-prone C code and recompilation.

5 BUILDING VERIFIED LOW∗LIBRARIES AND APPLICATIONS

The evaluation applies Low* to verified cryptographic libraries and applications, showing interoperability, strong assurance properties, and performance close to optimized C and assembly.

  • HACL*: HACL* implements the NaCl API with mechanically verified memory safety, functional correctness, and side-channel resistance, while remaining ABI-compatible as a drop-in replacement.Its generated C can replace Sodium or TweetNaCl without recompiling dependent applications.
  • HACL*: HACL* matches optimized C performance for ChaCha20, Salsa20, and Poly1305, while assembly implementations are about 3–4 times faster.The comparison uses 16KB inputs and averages 1000 iterations in cycles per byte.
  • HACL*: HACL*’s Curve25519 implementation is about as fast as Sodium’s 64-bit C, an order of magnitude faster than TweetNaCl’s 32-bit code, and significantly faster than OpenSSL.The implementations in Sodium and HACL* exploit the 64×64-bit multiplier on Intel 64-bit platforms.
  • Trust and performance: The evaluation’s performance guarantees remain dependent on trusting GCC and Clang, while CompCert imposes substantial slowdowns for some cryptographic code.CompCert causes a 3x slowdown for Salsa20 and ChaCha20 and a 30–60x slowdown for Poly1305 and Curve25519.
  • Applications: PneuTube uses HACL* to provide asynchronous encrypted file transfer with verified memory safety, side-channel resistance, and correct file and socket usage.It protects metadata and hides file size through padding before encryption.
  • Applications: A 1GB same-machine transfer takes 6s in PneuTube versus 8 seconds for SCP using SSH with ChaCha20-Poly1305.The timing combines cryptographic, disk, and network I/O.
  • AEAD for miTLS: The AEAD implementation replaces an idealized OpenSSL binding in miTLS, addressing the risk that the real implementation diverges from the ideal behavior.The motivating concern includes vulnerabilities such as CVE-2016-7054.

6 RELATED WORK

Related work spans verification directly on C, memory-safe low-level languages, and generative systems, while Low* emphasizes sophisticated reasoning, portability, and cryptographic security proofs.

  • Verification approaches: Verification-condition approaches can verify existing C but must handle C’s complexity and arbitrary optimization techniques.This motivates alternatives that constrain the programming model or move verification closer to the source.
  • Verified cryptography: Low* applications are an order of magnitude larger than most previous verified cryptographic work, and AEAD verification targets cryptographic security as well as functional correctness.The AEAD result extends beyond functional correctness.
  • Memory safety: Memory-safe C dialects and low-level languages prevent important attacks, but their type systems may limit expressiveness for complex invariants.Low* supports arbitrarily sophisticated memory-safety reasoning, but currently cannot handle concurrency and lacks efficient decision procedures.
  • Generative verification: LMS-Verify verifies generated C, keeping code generation outside its trusted computing base but separating verification from the original source.Its approach is contrasted with Low*’s source-level verification setting.
  • Generative verification: Bedrock builds verified low-level programs from assembly-like generators without sacrificing performance, but its verified code is not portable.This contrasts with Low*’s focus on portable C compilation.
  • AEAD verification: Earlier miTLS work described AEAD security with an experimental C backend but made no further backend claims, whereas the present work develops and evaluates Low* compilation.The distinction concerns the compiler backend rather than the cryptographic security model itself.

7 CONCLUSION

The paper presents a methodology for verifying low-level code in F* while retaining a modular programming style and performance comparable to hand-written C. Its formal development defines Low* and its semantics, compilation to C*, and the associated operational machinery.

  • Conclusion: Low* embeds low-level programming and memory models within F*, enabling high-level proofs while retaining modular features such as recursion and type abstraction.The methodology targets code written for verification without giving up low-level control.
  • Conclusion: The toolchain uses partial evaluation and C compilers to produce code suitable for verification with performance comparable to hand-written C.
  • Conclusion: The conclusion identifies three ongoing directions: porting miTLS to Low*, verifying more of KreMLin, and embedding assembly instructions for further optimization.The authors specifically mention the λow* to C* transformation as a target for formal verification.
  • Formal definitions: The formal development defines C* and λow* syntax, values, memory, evaluation contexts, labels, and operational semantics.C* expressions use evaluation functions while statements use small-step semantics; λow* makes effectful operations explicit.
  • Compilation: The λow* to C* compilation is a partial function whose rules enforce syntactic constraints, including wrapping compilable top-level functions in withframe constructs.The compilation rules translate expressions, statements, functions, and values into C* constructs.

D BISIMULATION PROOF

The bisimulation proof establishes that compiled C* faithfully represents λow* execution and preserves safety. Because expression evaluation can temporarily desynchronize the systems, the proof uses quasi-refinement and determinism to recover refinement and bisimulation.

  • Proof strategy: Quasi-refinement permits temporary stuttering when λow* and C* steps go out of sync, while still supporting the bisimulation proof.The mismatch arises because C* expressions use big-step semantics.
  • Configuration relation: The proof uses a C*-to-λow* back-translation to relate configurations because C* exposes a call stack while λow* uses one large expression.
  • Main results: Theorem D.6 states that safety of a λow* program implies safety of its C* counterpart.
  • Main results: Theorem D.7 states that the C* transition system bisimulates the corresponding λow* transition system.This result applies to compiled programs, closed expressions, and closing substitutions.
  • Proof strategy: Determinism converts quasi-refinement into refinement, and the refinement results then yield bisimulation and safety.The argument relies on Lemma D.10, Lemma D.12, and Corollary D.13.

E.1 Reminder: CompCert Clight

This section recalls CompCert Clight’s syntax, transition semantics, and memory model as the target foundation for the Low* compilation pipeline. Clight separates side-effect-free expressions from statements and models memory through typed block operations.

  • Clight overview: CompCert Clight is a C subset with side-effect-free expressions and byte-level value representation.Its syntax, semantic definitions, expression evaluation, and small-step semantics are presented separately.
  • Program semantics: Clight program execution is defined by calling main with no arguments, with final configurations determined by main’s return value.
  • Syntax: Clight expressions support variables, pointer addition, field projection, address formation, and pointer dereference.
  • Trace semantics: Generated Clight statements use annotation calls to record memory accesses in execution traces.Each statement performs at most one memory access, which is preceded by an annotation producing the corresponding event.
  • Memory model: The Clight memory model provides Get, Set, and Alloc operations for reading, writing, and allocating memory blocks.Get decodes bytes, Set encodes values into bytes, and Alloc returns a fresh block initialized with unknown locations.

E.2 Issues

The translation from C* to Clight must address differences in local structures, stack allocation, and memory-event identities. In particular, Clight hoists local variables, which can change allocated blocks and therefore threaten exact trace preservation.

  • Local structures: C* local structures create memory-access management issues when translating to Clight, despite compatible structure memory representations.
  • Stack-allocated local variables: Clight requires all local variables to be hoisted and allocated when entering a function, unlike C*’s on-the-fly stack allocation.The verified part of CompCert does not support this hoisting transformation directly.
  • Stack-allocated local variables: Hoisting variables across branches can allocate blocks that the original C* execution would not allocate, changing memory-event traces.The example contrasts one conditionally allocated variable with two variables allocated before the branch.
  • Trace preservation: The adopted solution replaces concrete pointers in read and write events with function, recursion-depth, variable, offset, and field identifiers.The authors use this representation to prove the correctness of hoisting.

E.3 Summary: from C∗to Clight

The compilation pipeline transforms C∗ into CompCert Clight while preserving functional behavior and noninterference. It uses intermediate language changes and abstract traces to accommodate differing memory representations.

  • The pipeline transforms a C∗ program into CompCert Clight while targeting preservation of functional correctness and noninterference.
  • C∗ is first enriched with unambiguous variable information, then reinterpreted with an abstract trace model.
  • Local arrays are hoisted, structure-returning functions are transformed, and structure accesses are expanded into field-level events.
  • The transformed program is reinterpreted to restore concrete memory-location traces before compilation into Clight.

E.4.1 Disambiguation of variable names.

Variable-name disambiguation enriches C∗ configurations so memory blocks can be mapped back to local variables. Under the stated safety and naming conditions, the transformation preserves traces, functional correctness, and noninterference.

  • Unambiguous local variables forbid conflicting array and non-array declarations within a function.
  • C∗2 records the current function and active local-array names in each configuration to track variable-to-block correspondence.
  • Under unambiguous local variables, C∗ and C∗2 have the same execution traces and preserve functional correctness and noninterference.
  • C∗3 replaces concrete pointers in read and write events with abstract pointers obtained through VarOfBlock.
  • C∗2-to-C∗3 reinterpretation preserves behavior after removing read and write events, and preserves noninterference under the stated safety conditions.

E.6 Local structures

The local-structure treatment addresses both CompCert performance overhead and noninterference reasoning. The approach erases most local structures into individual fields, while retaining explicit memory accesses for returned structures.

  • Naively compiling local structures as C structures caused more than 60% slowdown with CompCert compared with GCC -O1.
  • CompCert treats C structure field accesses as memory reads, limiting optimization of local structures whose addresses are not taken.
  • Treating local structures as memory accesses complicates noninterference proofs when fields are read as expressions.
  • Local structures may be expressions, by-value arguments, or return values; returned structures require caller-provided stack storage and a pointer to the callee.
  • At the Clight level, only structures returned by value introduce additional memory accesses from local structures.

E.6.1 Structure return.

Structure-return handling introduces explicit events and then transforms structure returns into pointer-based writes and ordinary returns. The transformation preserves behavior and traces, yielding functional correctness and noninterference together.

  • Structure returns are modeled with additional fake read and write events before introducing corresponding stack-allocated variables.
  • C∗4 adds return-related events only when the caller uses the returned value, while preserving the prior functional behavior after auxiliary events are removed.
  • The C∗3 invariants continue to hold in C∗4, including the invariants used for reasoning about executions with equal traces.
  • StructRet replaces a structure return with a write through a fresh pointer and an ordinary unit return, or leaves non-structure returns unchanged.
  • The structure-return transformation therefore establishes functional correctness and noninterference together.
  • If the source program is safe and has unambiguous local variables, StructRet preserves behavior and traces.

E.6.2 Events for accessing structure buffers.

Structure-buffer accesses are expanded into field-level events, preserving traces and therefore both functional correctness and noninterference while restricting accesses to atomic types.

  • Read and write events on structure values are translated into sequences of events for each non-structure field.
  • The C∗3-to-C∗5 trace transformation is correct: every translated trace corresponds to an original trace and vice versa.
  • The transformation preserves functional correctness and noninterference despite not being injective.
  • After transformation, all read and write events target atomic, non-structure types.
  • Local structures are then replaced by field-specific variable names for every reachable non-structure field.

E.6.3 Local structures.

Local-structure erasure reduces structured expressions and statements to field-level forms, preserving execution traces while exposing a limitation around structure-valued parameters and ABI compliance.

  • 20% time savings are reported for structure erasure with CompCert 2.7 on the stated 4-core Intel Core i7 laptop.
  • Expression erasure: Expression reduction produces structure-free expressions of the same type, and evaluation then depends only on non-structure variable values.
  • Statement erasure: Structure-valued parameters passed by value are replaced with recursive lists of their non-structure fields.
  • Statement erasure: Structure erasure removes local structure variables, structure expressions, and field projections from the transformed program.
  • Correctness: For safe C∗5 programs satisfying the stated syntactic restrictions, structure erasure preserves execution traces.
  • Limitation: The field-based parameter transformation can cause ABI compliance issues because System V x86 requires byte sequences, including padding, for structures passed by value.

E.7 Generation of CompCert Clight code

The compiler translates the structure-erased C∗ language into CompCert Clight through explicit memory and entrypoint representations, preserving execution traces and noninterference.

  • Entrypoint translation: Clight built-in functions provide a secret-independent representation for values supplied to the C∗ entrypoint.
  • Expression translation: C∗2 expressions without structures or field projections are translated directly into corresponding CompCert Clight expressions.
  • Expression translation: The expression translation preserves evaluation results under the stated correspondence between C∗2 variable maps and Clight variables.
  • Correctness: For safe C∗2 systems under the stated restrictions, the generated Clight program has the same execution trace.
  • Security: Because both semantics record memory accesses in traces, the translation preserves functional correctness and noninterference.

F PROOF OF THE SECRET INDEPENDENCE THEOREM

The secret-independence proof formalizes Low∗ typing, value and heap relations, and assumptions on secret-manipulating functions to establish secret-independent traces, while noting that typing alone does not ensure progress.

  • Type system: Low∗ types include integers, units, records, buffers, mutable structures, and abstract types, with judgments tracking signatures, store typing, and variables.
  • Equivalence relations: The proof defines equivalence relations for values and heaps that relate secret-independent components while allowing abstract components to vary.
  • Proof infrastructure: The generation functions construct substitutions and typing contexts from related values and heaps for the proof of secret equivalence.
  • Function assumptions: The assumptions require related inputs, well-typed closed heaps, matching traces, equivalent output heaps, and related output values for secret-manipulating functions.
  • Type system: The type system guarantees preservation but not progress because it does not track buffer bounds or buffer and mutable-structure lifetimes.
Loading 1703.00053v6…