tiny.quic

Overview · API · Code relationships · Verification · Audit

Overview

QUIC version 1 carries encrypted, numbered packets over UDP. State machines in the package run on bytes the caller owns. The package holds a connection, wire codecs for headers and frames, packet protection, a TLS 1.3 handshake, and a simulated path for tests.

A program speaking this protocol must number, encrypt, and authenticate every packet it sends, recover packets that were lost, and run a key exchange whose messages travel inside its own frames. The protocol engine must execute all of these operations inside whatever event loop and memory budget the host program already has.

The state one connection keeps is large and lives as long as the connection, so an implementation that asks for memory as it runs makes its own footprint a function of what the peer chooses to send. Key exchange and packet encryption join through one key schedule and through rules about when keys are thrown away, so both parts must be settled together. Loss recovery and timeouts depend on when packets arrive, and a real network does not reproduce that timing on demand.

RFC 9000 fixes the wire format, and the codecs here read and write exactly those forms: the variable-length integers, the long and short header layouts, and the packet number truncation. RFC 9001 fixes how TLS keys protect QUIC packets, and this code derives the Initial secrets from the client connection ID, builds each nonce from the packet number, applies the masking of a packet's first byte and packet number from a sample of the encrypted payload as header protection, tags Retry packets, and updates keys under the same labels. RFC 9002 fixes loss detection and the probe timeout, and the recovery code declares losses by the same two rules and backs the probe period off the same way.

The package reaches for no allocator, so a caller derives an exact byte count from the capacities it chooses and hands over one aligned block, and every buffer a connection keeps lives inside that block. The connection opens no socket and runs no loop. The bytes of one UDP payload, which may hold more than one packet end to end, form a datagram: receiving means handing the connection those bytes, and sending means letting it write one datagram into the caller's bytes. The connection carries one bidirectional stream. The simulated path answers the timing problem by delivering datagrams on a schedule a test fixes, reproducing loss, duplication, reordering, and delay from one seed. The wire codecs, packet protection, key discard, and key update rules are written a second time as Lean definitions carrying proofs, and property tests compare the two implementations on drawn inputs.

• packet number space: one of three, Initial, Handshake, and application, each numbering its own packets from zero.
• handshake confirmation: the point at which the handshake is complete for both endpoints, after which the Handshake keys go and the retained handshake traffic secrets are erased at once.
• traffic secret: the 32 bytes from which one direction's packet keys derive.

Definitions

Namespaces

Public namespaces.

• cursor
• connection
• crypto
• frame
• packet
• sim
• tls: The TLS 1.3 handshake a QUIC connection needs runs as a state machine over bytes the caller carries.
• varint
• transport

Code relationships

Direct static dependencies extracted from parsed source by semantic graph analysis.

Uses: tiny.deflate, tiny.hypothesis, tiny.reticulum, tiny.sdfii
Used by: tiny.accy, tiny.sdfii, tiny.smg

Verification

No verification records are cataloged for this module in this build.

Audit