Noise: A Library of Verified High-Performance Secure Channel Protocol Implementations

## Overview Nostar is a verified implementation framework for the Noise protocol family, a collection of approximately 59 protocols (expandable with new features) used for key exchange and contract establishment. Noise protocols are already deployed in real-world applications like WhatsApp and WireGuard VPN. The core problem Nostar addresses is that while many Noise implementations exist across programming languages, none are formally verified, leaving them vulnerable to bugs commonly discovered in protocol implementations (such as TLS and Signal).

## Technical Architecture Nostar comprises three integrated components:

1. **Protocol Compiler**: Transforms Noise protocol patterns into specialized, verified C implementations 2. **Verified Library Stack**: Provides a high-level defensive API exposing memory-safe, type-safe, and functionally correct code 3. **Formal Security Analysis**: Uses symbolic methods to prove authentication and confidentiality guarantees

The verification toolchain builds on F* (a theorem prover with dependent types and program verification) and Low* (an effectful subset for writing verified C-like code), with compilation to C via the Karamel framework. This approach has been successfully applied in the Everest project for providing verified HTTPS components.

## Key Innovation: Partial Evaluation The central technical contribution is using partial evaluation to transform a generic interpreter-based specification into specialized compiled code. Rather than writing separate implementations for each protocol, the speaker describes a technique where: - A single High* interpreter processes protocol token lists - Low* rewrites this interpreter with preconditions, postconditions, and functional correctness properties linked to the high-level spec - At compile-time, F* specializes the code by inlining the interpreter, evaluating matches, and eliminating recursive calls

F*'s dependent type system enables extremely precise control flow with no runtime token processing or list manipulation. The speaker compares this to C++ template metaprogramming applied at the protocol definition level, using partial reduction techniques previously employed in cryptographic primitives like Hacl* and vectorization code.

## API Design and Security Properties The high-level API (accounting for over 75% of generated code) implements: - Verified state machines abstracting handshake and transport phases - Misuse-resistant patterns that prevent sending data before security guarantees are established - Dynamic checks and verified key management utilities for validation, loading, and secure storage

Security analysis is formalized in Dollar* (a photosymbolic analysis framework), with one generic symbolic proof operating at the interpreter specification level. This enables analysis of all 59 protocols simultaneously, in contrast to tools like ProVerif that typically require per-protocol proofs.

## Implementation Results The framework generated code for all 59 Noise patterns with 8 cipher suite variants each, totaling 472 instantiations. Benchmarks show competitive performance against existing implementations, with execution speed superior to all tested alternatives except WireGuard (which is hand-optimized for a single pattern).

## Limitations and Q&A Clarifications Formal proofs cover functional correctness and some constant-time properties (by avoiding operations like division), but do not extend to C compiler behavior or memory-zeroing guarantees (which are implemented manually). Adding new protocols at the pattern layer is straightforward, but extending the API or updating security proofs requires more substantial work due to subtle symbolic analysis constraints.