Verified DNS-over-QUIC Server in F*

This project aims to implement a mathematically verified DNS server using F*, Low*, and the Project Everest ecosystem (HACL*, EverCrypt, EverParse, Steel).

Documentation

• Architecture: Layered security design and Mermaid diagrams.
• Implementation Plan: High-level strategy and RFC roadmap.
• Threat Model: STRIDE analysis and Post-Quantum assessment.
• Development Roadmap: Active task tracking and progress.

Key Features

• Formal Verification: Memory safety and functional correctness proven in F*.
• DNS-over-QUIC (DoQ): Implementation based on RFC 9250.
• Modern Standards: Support for TLS 1.3 and modern DNS resource records.
• Security First: Parser-rejecting architecture and verified cryptographic primitives.

Project Structure

• src/protocol: DNS wire format and protocol definitions.
• src/security: Cryptographic integration and TLS 1.3 handshake.
• src/transport: QUIC stream mapping and framing.
• src/logic: Core DNS lookup logic (Authoritative & Recursive).
• src/concurrency: Steel-based concurrent memory management.
• spec: High-level RFC specifications.
• tests: Unit tests and fuzzing harness.

Building & Running

The project uses F* for verification and KaRaMel for extraction to C.

Toolchain Version Policy

This repository is currently pinned to F* v2026.03.24, the last project baseline before the removal of the old Low* sublanguage in F* v2026.04.17. Newer F* releases, including the weekly v2026.05.03 line, should be tracked in a separate migration lane until the Low*/Pulse/KaRaMeL strategy is settled.

Routine development should use the pinned container image. Upgrading the main toolchain past v2026.03.24 is a migration task, not a routine dependency refresh.

The repository also includes a non-blocking migration container in Containerfile.migration. That image tracks a recent F* release for compatibility testing only; failures there are migration evidence and do not replace the pinned development lane.

Using Podman/Docker (Recommended)

The development toolchain is provided by the local container image localhost/verified-dns-server:latest. Mount this repository at /workspace; the image's default command runs make verify.

# Run formal verification with the prebuilt local image
podman run --rm \
  --userns=keep-id \
  -v "$(pwd):/workspace:Z" \
  localhost/verified-dns-server:latest

If the local image is missing, build it from the checked-in Containerfile:

podman build -t localhost/verified-dns-server:latest -f Containerfile .

To test the current sources against a recent F* release without changing the stable toolchain, build and run the migration image:

podman build \
  --build-arg FSTAR_VERSION=v2026.05.10 \
  -t localhost/verified-dns-server:fstar-migration \
  -f Containerfile.migration .

podman run --rm \
  --userns=keep-id \
  -v "$(pwd):/workspace:Z" \
  localhost/verified-dns-server:fstar-migration

The migration image's default command verifies only the Pulse pilot. To also capture the current Rust-extraction assessment and legacy F*/Low* incompatibilities, run:

podman run --rm \
  --userns=keep-id \
  -v "$(pwd):/workspace:Z" \
  localhost/verified-dns-server:fstar-migration \
  bash -lc 'make verify-pulse-pilot && make pulse-rust-smoke && make verify'

To compile and run the generated Rust smoke check for the value-state Pulse pilot, run:

podman run --rm \
  --userns=keep-id \
  -v "$(pwd):/workspace:Z" \
  localhost/verified-dns-server:fstar-migration \
  bash -lc 'make pulse-rust-smoke'

To run a specific build target, override the default command:

podman run --rm \
  --userns=keep-id \
  -v "$(pwd):/workspace:Z" \
  localhost/verified-dns-server:latest \
  bash -lc 'eval $(opam env) && make extract'

To syntax-check the generated C bundle and EverParse wrapper without linking a final shell binary, run:

podman run --rm \
  --userns=keep-id \
  -v "$(pwd):/workspace:Z" \
  localhost/verified-dns-server:latest \
  bash -lc 'make c-compile-smoke'

To link and run the current generated parser and shell-boundary smoke binary, including ingress, response handoff, and the fixed-capacity C shell scaffold, run:

podman run --rm \
  --userns=keep-id \
  -v "$(pwd):/workspace:Z" \
  localhost/verified-dns-server:latest \
  bash -lc 'make c-link-smoke'

The image also includes EverParse/3D tooling. To regenerate the current EverParse parser scaffold and verify/extract the generated subset, run:

podman run --rm \
  --userns=keep-id \
  -v "$(pwd):/workspace:Z" \
  localhost/verified-dns-server:latest \
  bash -lc 'make everparse-verify'

With Docker, run the container as your host UID/GID so generated obj/, dist/, or generated/ files are writable on the bind mount. Omit the SELinux :Z suffix if your Docker setup does not support it:

docker run --rm \
  --user "$(id -u):$(id -g)" \
  -e HOME=/tmp \
  -v "$(pwd):/workspace" \
  localhost/verified-dns-server:latest \
  bash -lc 'make verify'

Manual Build

See the Makefile for details. Requires F* v2026.03.24 and KaRaMel.