Generate OCaml/C cryptographic libraries from F*

Mixing OCaml and C is the standard way to develop cryptographic libraries at No-
madic Labs.
This approach however suffers from several downsides: – memory unsafe C can hin-
ders the safety properties offered by OCaml – writing C is not fun – bindings between
languages are dangerous boilerplate code – OCaml’s type-system is often not enough
to express some security properties
F* is a proof-oriented programming language which by default generates OCaml code
and embeds a C-like language, Low*, which can be extracted to memory-safe C. Con-
veniently OCaml bindings can be automatically generated for Low* functions. Fur-
thermore F* can be used to prove interesting properties.
The goal of the internship is to explore advantages and limitations of developing
cryptographic libraries in F*/Low* and integrating them into an OCaml project.

Internships goals

The case study of the internship consists in reimplementing in F*/Low* an existing
OCaml/C library that handles polynomials over finite-fields.
One objective is to understand how to effectively structure an F*/Low* project so that
the build-system, tool-chain and CI are easy to integrate into an OCaml project.
The second objective is to prove properties about correctness and performance of
data structures. For example avoiding unnecessary bound checks or copies.
The third objective is prove properties about the algebra underpinning the crypto-
graphic primitives. For example that polynomial addition behaves correctly.

Requirements

The intern must be familiar with one functional programming language and have
some experience with C. Some understanding of manual memory management and
garbage collection is important. Experience with a formal verification tool or proof
assistant is a plus.

Internship Context

You will work at the Nomadic Labs’ offices in Paris.
Participating in a large scale open-source project you will have to rapidly learn to
use collaborative tools (Git, merge request, issues, gitlab, continuous integration,
documentation) and to communicate about your work. The final results might be
presented at an international conference or workshop.
You will have a designated advisor at Nomadic Labs and will have to work indepen-
dently and to propose thoroughly-considered solutions to the different problems you
will have to solve. You will be encouraged to seek advice from members of the team.

Intellectual Property

All material produced (essays, documentation, code, etc.) will be released under an
open source license (e.g. MIT or CC).