# Projects

## Noise*

My research journey towards program verification at scale started with Noise*, a verified compiler for the Noise family of protocols. Noise defines a simple, succinct domain-specific language (DSL) to describe key-exchanged (or handshake) protocols. Handshake protocols are typically used to setup secure connexions between peers willing to communicate, similarly to TLS. The description of a protocol in the Noise DSL is called a “pattern”.

IKpsk2: <- s ... -> e, es, s, ss <- e, ee, se, psk

Protocol code can be quite low-level, leading to bugs which can compromise their security (e.g., see Heartbleed) and making such code a prime target for program verification. Verifying one protocol is however expensive: for instance, miTLS, a verified implementation of TLS, took 3.5 person-years to verify. At the same time, we need various protocols for various use cases, leading to obvious scalability issues. This is the reason why we decided to target a whole family of protocols like Noise, which covers a wide range of use cases at one.

The result of our work is a compiler which generates fast, specialized C code for every choice of cipher suite and Noise protocol pattern, and complements this low-level protocol code with a high-level, specialized, defensive API which handles state-machines, key lookup and storage, peers, etc. We used the Low* toolchain inside the F* theorem prover to prove that the code is memory safe, functionally correct, and satisfies formal authentication and confidentiality properties.

We implemented this compiler by using a technique called the Futamura
projection. We wrote and formally verified *one* generic interpreter for the
Noise DSL, that we could later instantiate with a specific pattern. By partially
evaluating this instantiation (i.e., by evaluating subexpressions at compile
time, for instance by unfolding functions, inlining let-bindings, evaluating
matches, etc.) we could turn this instantiation into specialized code. This is a
simple technique which becomes extremely powerful when combined with F*’s
expressive type system, and more specifically its dependent types. As a
consequence, we were able to generate efficient, idiomatic C code with precise
control-flow, types and function signatures for each of the 59 Noise protocols
(remember, miTLS took 3.5 person-years for a *single* protocol!). If you want to know
more about the application of partial reduction to the verification of
cryptographic code in general, you can read Jonathan’s excellent blog
post.

Given that every API instantiation generates between 4k and 6k lines of C code and that we currently support 8 choices of cipher suites per pattern, not even mentionning the fact that we can pick various optimized implementations for the cryptographic primitives, we can generate hundreds of thousands of lines of verified code for the 59 Noise patterns! For now, we generated 472 instantiatiations which are readily available in the github repository of the project. Those are of course a limited subset of what we cover: feel free to reach us if you want a specific instantiation of Noise*. And if you want to know more about the specific details, you can have a look at our S&P’22 paper.

The project hit several difficulties, however, which revealed the limitations of our toolchain.

First of all, F* targets *intrinsic* proofs, by which we write code with
annotations such as pre and post-conditions, assertions or lemma calls. At
type-checking time, F* generates big weakest preconditions (sets of proof
obligations) which it sends to the Z3 SMT solver to discharge (or fail to
discharge, in which case we need to update the code to fix bugs, or better
explain to Z3 why the code is indeed correct). The issue is that intrinsic
proofs work fine and are very pleasant at first… until they suddenly become
intractable. More specifically, as the context grows bigger, the proof
obligations become more complex and Z3’s response time becomes higher, making
F* gradually less interactive. This can lead to nightmarish situations when
combined with the fact that the user is blind when carrying their
proofs. Carefully controling the context, for instance by hiding definitions
behind interface files, requires great care and expertise and is not always
possible. Finally, intrinsic proofs are fundamentally non-modular, while
projects require modularity as they grow bigger: for instance, one may want
to verify a single function in several steps.

A second problem we faced was reasoning about memory and aliasing. This was especially frustrating because memory management is quite simple in Noise*, making one expect the memory reasoning to be straightforward. More specifically, reasoning about the disjointness of various elements in memory makes the context quickly saturate, especially in the last layers of the API, and acted as a formidable catalyzer of all the problems we faced with intrinsic proofs. Overall, the Low* toolchain is very well suited at verifying cryptographic primitives and protocols as demonstrated by the Hacl* project: memory management is quite simple and in particular memory allocation is almost non-existent, the control-flow contains few branchings, the SMT solver is of great help when reasoning about non-linear arithmetic, etc. As a consequence, we had a very smooth experience when working on the protocol code of Noise*. In contrast, we quickly faced an accumulation of problems while moving up the stack through the various layers of the API, and as a consequence decided to completely rethink our toolchain, leading us to the second part of my journey.

## Aeneas, and his little brother Charon

An appalling issue we faced when reasoning about aliasing in Noise* is that,
when one looks closer, there is actually barely any aliasing at all in this
code. This made us ask ourselves: isn’t there a way of drastically simplifying
the proofs when the memory usage is *disciplined*? And actually, what does a
*disciplined* memory usage mean? Fortunately, Rust and its borrow mechanism
answer this last question in a very interesting manner, by constraining the
programmer in their use of memory to get memory safety while allowing for a very
expressive language. We consequently decided to switch to Rust as our
implementation language, and leverage its type system to simplify the proof
obligations.

This idea of leveraging the Rust type system to simplify memory reasoning is not
new, and has been exploited for several years by other projects like
Prusti or
Creusot. However, many of those projects
target frontends *à la* Dafny, with intrinsic proofs and weakest preconditions
sent to SMT solvers. As stated above, such proofs work fine in many situations,
but on our side we needed a toolchain targeting extrinsic proofs. We also wanted
to use tactic-based theorem provers, by which one does the proofs incrementally
by interacting with a proof context, while leveraging the possibility of
implementing custom automation with their tactic language. For this reason, we
decided to create a new toolchain.

Our toolchain, Aeneas, leverages the
Rust type system to compile Rust programs to pure, executable models (i.e.,
pure, functional versions of the original Rust programs). The key idea behind
Aeneas’ compilation is that, under the proper restrictions, a Rust function is
fully characterized by a *forward* function, which computes its return value at
call site, and a set of *backward* functions (one per lifetime), which propagate
changes back into the environment upon ending lifetimes, thus accounting for
side effects. Such forward and backward functions behave similarly to
lenses.
Relying on theorem provers to state and prove lemmas about those models, it is
then possible to enforce guarantees about the original programs. For instance,
one can prove panic freedom and functional correctness (see our ICFP
paper, or its long
version), but also security guarantees like
authentication and confidentiality as was done with Noise*, and potentially
more. For now, Aeneas generates pure models for
F* and Coq, and we are
working on additional backends for Lean and
HOL4. This project is actually very similar
to an older project called Electrolysis
and which targeted LEAN: Aeneas is our attempt at designing a more principled
translation which targets a bigger subset of Rust and generates code for several
backends.

Aeneas relies on Charon to retrieve code from the Rust compiler. Charon is a driver which retrieves Rustc’s output (more precisely, the generated MIR) and translates it to an intermediate language we called LLBC (Low Level Borrow Calculus - an “easy-to-use” version of MIR in practice). Charon is independent of Aeneas and should be reusable for other projects: feel free to use it, submit PRs, and contact us if you have any questions.

## Side Projects

### F* Extended Mode

The F* extended mode is a side project I did at some point to improve the interaction with F*, and in particular make the user less blind when writing proofs by inserting information about the context directly into their code. The principle is very simple: by calling dedicated commands, one could introduce the pre and post-conditions of an (effectful) function call, unfold definitions or split conjunctions in assertions. I merged the F* meta code necessary to compute this information to the F* main branch, but for some reason I never took the time to merge the elisp code into the F*-mode repo. I may find the motivation to do so in the future provided I get enoug traction.