Project Everest: Building a Provably Secure HTTPS Ecosystem with F*

As part of “The Key Exchange” — a weekly gathering for the CMPS297AD/396AI Applied Cryptography course at AUB — I gave an optional presentation on a topic I’m passionate about: formal verification in cryptographic software.

The goal of this weekly gathering was to provide advanced training in communicating complex technical ideas. My professor, Dr. Nadim Kobeissi, later summarized the student presentations and was kind enough to say this about my talk:

[…] Daniel Dia’s deep dive into Project Everest and F* formal verification showed appreciation for the intersection of programming languages and cryptographic correctness.

My presentation, “Project Everest: Building a Provably Secure HTTPS Ecosystem with F*,” served as an introduction to how we can use advanced programming language theory to build software that is provably correct, moving beyond the limitations of traditional testing.

The core of the talk focused on several key ideas:

• A New Way of Thinking About Types: I contrasted the classical “systems view” of types (e.g., in C++, where a type is just a description of a memory layout) with the “formal methods view” used in languages like F* and Lean4. In this paradigm, a type is a tool for reasoning, classifying values, and expressing provable constraints before the program ever runs.

• Motivation (Why Testing Isn’t Enough): Using real-world examples like the Heartbleed bug, I argued that many critical vulnerabilities are not flaws in the cryptographic algorithms themselves, but simple programming errors in their implementation (like missing bounds checks). Testing is insufficient to catch all of these subtle but catastrophic bugs.

• Core Concepts (Dependent Types): I introduced dependent types—types that depend on values, not just other types. This allows us to encode program logic directly into the type system (e.g., type key_buffer = b:array u8{Array.length b = 32}). This moves runtime checks into compile-time guarantees, making entire classes of errors (like buffer overflows or timing attacks) impossible to represent.

• Case Study (Project Everest): The talk culminated in a deep dive into Project Everest, a collaborative effort to build a fully verified HTTPS stack using the F* language. I covered its main components:

  • HACL*: A library of cryptographic primitives (like ChaCha20, Curve25519) formally proven to be memory-safe, functionally correct, and side-channel resistant.

  • KreMLin: A verified compiler that translates the proven F* code into efficient, readable, and dependency-free C code.

  • MiTLS: A verified reference implementation of the TLS 1.2 and 1.3 protocol state machines, eliminating logical flaws.

• Finally, I highlighted the real-world impact of this work, showing that the C code generated by Project Everest is already used in production by major projects, including the Linux Kernel, Mozilla Firefox, and the Windows Kernel.

Here are the talk’s detailed slides (in LaTeX, of course)!