Verify curve25519-dalek

Appearance

Project ​

Curve25519-dalek ​

Curve25519-dalek is a pure-Rust implementation of group operations on Curve25519. It provides fast, safe cryptographic primitives used by thousands of projects for key agreement, signatures and zero-knowledge proofs.

Project aims ​

This project aims to prove the functional correctness of the curve25519-dalek implementation. Using Aeneas, we obtain a faithful representation of the Rust code in Lean 4, a powerful proof assistant. This allows us to harness Lean's mathematical capabilities to write precise specifications and formally prove that the implementation satisfies them.

The aims are two fold:

  • Formally verify the chosen subset of functions from this crate
  • Figure out how formal verification can be done on large scale, quicker, cheaper and commonplace

Extraction Overview ​

Our Progress ​

Check out the Stats page to track our progress, or the Status page to see which functions have been verified.

The Scalability Challenge ​

Formal verification has traditionally been resource-intensive and time-consuming. Can we find ways to solve the scalability problem of formal verification?

If you're interested in the verification methodology or formal methods at scale, we'd love your insights and contributions.

Trust Model ​

See below for information on what we need to trust to rely on these proofs.

Source Information ​

This repository contains the curve25519-dalek Rust crate from:

Here we work exclusively with the 64 bit serial backend. I.e., we compile the Rust code with the flags:

bash
RUSTFLAGS='--cfg curve25519_dalek_backend="serial" --cfg curve25519_dalek_bits="64"' cargo build

From this we have chosen a subset of functions which isn't all of those in this crate with this particular choice of backend but it is a useful complete set for typical cryptographic applications.

Status tracking ​

  • The file status.csv is the source of truth for tracking progress of the project, updates to this file should be made when functions are extracted, have specs added or if verification is complete
  • The column extracted can be empty of have the value extracted
  • The column verified can be empty or have the values draft spec, specified or verified
    • ✏️ draft spec - Draft spec (in natural language) has been added
    • 📋 specified - Formal specification in Lean added
    • ✅ verified - Function has been formally verified (spec theorem has been proven)

Issue and PR Linking ​

Open GitHub issues and pull requests are automatically linked to functions in the status table when they mention the full function name (including crate prefix) in any of these formats:

  • Rust path: curve25519_dalek::backend::serial::u64::field::FieldElement51::from_bytes
  • Lean notation: curve25519_dalek.backend.serial.u64.field.FieldElement51.from_bytes

CI ​

  • CI will automatically update the project site when the file status.csv is updated
  • Whilst fixes to Aeneas are in progress we sometimes make modifications to the Rust source code in order to enable extraction, the changes are recorded in src-modifications.diff and CI checks that this file is updated
  • The CI runs Aeneas on the source code and checks that the generated files, Types.lean and Funs.lean haven't been modified since extraction (not active, to be activated soon)
  • CI checks that the Lean project builds without errors. It permits the presence of sorry since this often represents work in progress

Repository Structure ​

  • curve25519-dalek/ - Original Rust implementation from dalek-cryptography
    • src/ - Rust source code of curve25519-dalek
  • Curve25519Dalek/ - Lean formalization and proofs
    • Types.lean - Type definitions extracted from Rust (generated by Aeneas and not manually edited)
    • Funs.lean - Function definitions extracted from Rust (generated by Aeneas and not manually edited)
    • TypesExternal.lean - Definition of types external to the crate
    • FunsExternal.lean - Definition of functions external to the crate
    • Specs/ - Spec theorems (together with proofs), folder structure coincides with Rust modules
    • Aux.lean - Auxiliary lemmas and utilities
    • Defs.lean - Spec-specific definitions
    • Tactics.lean - Custom tactics
  • site/ - Verification project website
  • scripts/ - Convenience scripts
  • status.csv - Verification progress tracking
  • src-modifications.diff - Modifications to the upstream Rust code

Trust model and Verification Method ​

Verification Approach ​

Lean is an open-source programming language and proof assistant, allowing us to write mathematical specifications and prove that the implementation meets these specifications.

In this approach to formal verification, the Rust code is extracted (translated) to a representation in Lean. The idea is that the Lean code is then a faithful functional representation of the Rust code. This is done in a way that panics, failure to terminate, etc., are represented in the extracted code, in addition to being an accurate function representation. In this project we use Aeneas for this extraction.

What You Need to Trust ​

To trust that the curve25519-dalek implementation satisfies the proven specifications, you need to trust:

1. The Lean Proof Checker ​

  • Lean’s minimal trusted kernel guarantees absolute correctness in the proofs

2. The Aeneas Translation ​

  • One needs to know that the Lean code extracted by Aeneas faithfully represents the Rust code, this is a limited set of translations and subject to ongoing soundness proofs

3. The Specifications ​

  • The specifications are written in Lean which allows a phrasing which is convenient for humans to parse and allows easy drilling down into details using the interactive feature of Lean

4. External specifications ​

  • External dependencies of the crate have specs written in FunsExternal.lean and TypesExternal.lean so these files need to be inspected to ensure that these specs are correct

What You Don't Need to Check ​

  • Trust of spec proofs doesn't require inspecting the proofs themselves since this is checked by Lean
  • That no additional axioms have been introduced in the proofs can be checked by #print axioms spec_theorem_name