  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 \`a 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.
