lib/quic/src/properties/protection.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const hypothesis = @import("hypothesis");
3 const quic = @import("quic");
4
5 const crypto = quic.crypto;
6 const Aes128Gcm = std.crypto.aead.aes_gcm.Aes128Gcm;
7 const Hkdf = std.crypto.kdf.hkdf.HkdfSha256;
8 const Sha256 = std.crypto.hash.sha2.Sha256;
9 const KeyStorage = [crypto.Keys.storage_bytes_max]u8;
10 const property_seed: u64 = 0x7175_6963_6b65_7901;
11 const iv_bytes = crypto.iv_bytes;
12 const mask_bytes = crypto.header.mask_bytes;
13 const sample_bytes = crypto.header.sample_bytes;
14 const secret_bytes: usize = @sizeOf(crypto.Secret);
15 const sample_offset_bytes: usize = 4;
16 const offset_max: usize = 21;
17 const packet_bytes_max: usize = 64;
18
19 fn settings() hypothesis.Settings {
20 return hypothesis.Settings.dev()
21 .withSeed(property_seed)
22 .withDatabase("zig-out/hypothesis-failures/quic-protection");
23 }
24
25 const ModelError = error{
26 InvalidPacketNumberLength,
27 InvalidPacketNumberOffset,
28 TruncatedPacket,
29 PacketTooShort,
30 ConnectionIdTooLong,
31 PacketTooLarge,
32 InvalidLength,
33 InvalidPrefix,
34 };
35
36 const LeanError = enum {
37 invalid_packet_number_length,
38 invalid_packet_number_offset,
39 truncated_packet,
40 packet_too_short,
41 connection_id_too_long,
42 packet_too_large,
43 invalid_length,
44 invalid_prefix,
45 };
46
47 const RejectionMap = struct {
48 lean: LeanError,
49 model: ModelError,
50 production: anyerror,
51 };
52
53 /// The table pairing each error the Lean packet protection, Retry, and identity definitions can
54 /// raise with the mirror's error and the production error, for a comparison that expects both
55 /// implementations to refuse the same input. The table carries every error constructor of the Lean
56 /// `Quic.Protect.ApplyError`, `Quic.Protect.SampleError`, `Quic.Retry.TagError`, and
57 /// `Quic.Identity.DecodeError` types.
58 const rejection_map = [_]RejectionMap{
59 .{
60 .lean = .invalid_packet_number_length,
61 .model = error.InvalidPacketNumberLength,
62 .production = @as(crypto.header.ApplyError, error.InvalidPacketNumberLength),
63 },
64 .{
65 .lean = .invalid_packet_number_offset,
66 .model = error.InvalidPacketNumberOffset,
67 .production = @as(crypto.header.ApplyError, error.InvalidPacketNumberOffset),
68 },
69 .{
70 .lean = .truncated_packet,
71 .model = error.TruncatedPacket,
72 .production = @as(crypto.header.ApplyError, error.TruncatedPacket),
73 },
74 .{
75 .lean = .packet_too_short,
76 .model = error.PacketTooShort,
77 .production = @as(crypto.packet.OpenError, error.PacketTooShort),
78 },
79 .{
80 .lean = .connection_id_too_long,
81 .model = error.ConnectionIdTooLong,
82 .production = @as(crypto.retry.TagError, error.ConnectionIdTooLong),
83 },
84 .{
85 .lean = .packet_too_large,
86 .model = error.PacketTooLarge,
87 .production = @as(crypto.retry.TagError, error.PacketTooLarge),
88 },
89 .{
90 .lean = .invalid_length,
91 .model = error.InvalidLength,
92 .production = @as(SpkiError, error.InvalidLength),
93 },
94 .{
95 .lean = .invalid_prefix,
96 .model = error.InvalidPrefix,
97 .production = @as(SpkiError, error.InvalidPrefix),
98 },
99 };
100
101 const SpkiError = error{ InvalidLength, InvalidPrefix };
102
103 const RejectionCoverage = struct {
104 seen: [std.meta.fieldNames(LeanError).len]bool = @splat(false),
105
106 fn record(self: *RejectionCoverage, kind: LeanError) void {
107 self.seen[@backingInt(kind)] = true;
108 }
109
110 fn require(self: *const RejectionCoverage, kinds: []const LeanError) !void {
111 var missing: ?LeanError = null;
112 for (kinds) |kind| {
113 if (!self.seen[@backingInt(kind)]) missing = kind;
114 }
115 try std.testing.expectEqual(@as(?LeanError, null), missing);
116 }
117 };
118
119 var rejection_coverage = RejectionCoverage{};
120
121 const header_rejections = [_]LeanError{
122 .invalid_packet_number_length,
123 .invalid_packet_number_offset,
124 .truncated_packet,
125 };
126
127 const sample_rejections = [_]LeanError{.packet_too_short};
128
129 const retry_rejections = [_]LeanError{ .connection_id_too_long, .packet_too_large };
130
131 const spki_rejections = [_]LeanError{ .invalid_length, .invalid_prefix };
132
133 fn expectSameError(model_error: ModelError, production_error: anyerror) !void {
134 for (rejection_map) |mapping| {
135 if (mapping.model != model_error) continue;
136 try std.testing.expectEqual(mapping.production, production_error);
137 rejection_coverage.record(mapping.lean);
138 return;
139 }
140 return error.UnmappedLeanRejection;
141 }
142
143 test "Lean and protection mirror rejection map entries are unique and complete" {
144 var seen: [std.meta.fieldNames(LeanError).len]bool = @splat(false);
145 for (rejection_map, 0..) |entry, entry_index| {
146 const index: usize = @backingInt(entry.lean);
147 try std.testing.expect(!seen[index]);
148 seen[index] = true;
149 for (0..rejection_map.len) |prior_index| {
150 if (prior_index == entry_index) break;
151 try std.testing.expect(entry.model != rejection_map[prior_index].model);
152 }
153 }
154 for (seen) |present| try std.testing.expect(present);
155 }
156
157 test "Lean protection coverage lanes require every mapped rejection" {
158 var required: [std.meta.fieldNames(LeanError).len]bool = @splat(false);
159 const lanes = [_][]const LeanError{
160 &header_rejections,
161 &sample_rejections,
162 &retry_rejections,
163 &spki_rejections,
164 };
165 for (lanes) |lane| {
166 for (lane) |kind| required[@backingInt(kind)] = true;
167 }
168 for (required) |present| try std.testing.expect(present);
169 }
170
171 /// Returns the four big-endian bytes of a value, so the nonce construction truncates the way the
172 /// Lean definition does. A value above four bytes keeps its low four, because the Lean byte
173 /// conversion keeps the low eight bits of each byte it builds.
174 fn modelEncodeU32(value: u64) [4]u8 {
175 return .{
176 @truncate(value / 16_777_216),
177 @truncate(value / 65_536),
178 @truncate(value / 256),
179 @truncate(value),
180 };
181 }
182
183 /// Returns the packet number written big-endian into the low eight bytes of a twelve-byte zero
184 /// field, for the left half of the exclusive-or that makes a packet's nonce. The function follows
185 /// the Lean definition `Quic.Nonce.packetNumberField`.
186 fn modelPacketNumberField(packet_number: u62) [iv_bytes]u8 {
187 const value: u64 = packet_number;
188 const high = modelEncodeU32(value / (1 << 32));
189 const low = modelEncodeU32(value % (1 << 32));
190 return [_]u8{ 0, 0, 0, 0 } ++ high ++ low;
191 }
192
193 /// Returns the nonce for one packet number under one initialization vector, for a property that
194 /// compares it against the production nonce for the same inputs. The packet number field and the
195 /// vector are exclusive-ored byte by byte. The function follows the Lean definition
196 /// `Quic.Nonce.nonce`, over a twelve-byte vector.
197 fn modelNonce(iv: [iv_bytes]u8, packet_number: u62) [iv_bytes]u8 {
198 const field = modelPacketNumberField(packet_number);
199 var result: [iv_bytes]u8 = undefined;
200 for (0..iv_bytes) |index| result[index] = iv[index] ^ field[index];
201 return result;
202 }
203
204 /// Returns the bits of a packet's first byte that header protection covers, for the two header
205 /// forms that protect different bits. A long header offers its low four bits and a short header its
206 /// low five. The function follows the Lean definition `Quic.Protect.protectedBits`.
207 fn modelProtectedBits(first: u8) u8 {
208 return if (first & 0x80 != 0) 0x0f else 0x1f;
209 }
210
211 /// Returns the number of packet number bytes a first byte declares, for unmasking that starts by
212 /// reading how many packet number bytes follow. The two low bits hold that count less one. The
213 /// function follows the Lean definition `Quic.Protect.packetNumberLength`.
214 fn modelPacketNumberLength(first: u8) usize {
215 return @as(usize, first & 0x03) + 1;
216 }
217
218 /// Checks one packet length, packet number offset, and packet number length against each other, so
219 /// both masking directions can check their inputs and a property can check that the order of those
220 /// checks agrees. An empty packet gives `TruncatedPacket`, a zero offset gives
221 /// `InvalidPacketNumberOffset`, a length outside one to four gives `InvalidPacketNumberLength`, and
222 /// an offset or length past the packet end gives `TruncatedPacket`. The function follows the Lean
223 /// definition `Quic.Protect.validate`, including the order in which the checks fire.
224 fn modelValidate(packet_len: usize, offset: usize, length: usize) ModelError!void {
225 if (packet_len == 0) return error.TruncatedPacket;
226 if (offset == 0) return error.InvalidPacketNumberOffset;
227 if (length == 0 or 4 < length) return error.InvalidPacketNumberLength;
228 if (packet_len < offset) return error.TruncatedPacket;
229 if (packet_len - offset < length) return error.TruncatedPacket;
230 }
231
232 /// Returns one byte of the header protection mask, so every read past the five mask bytes has a
233 /// defined answer while the loop walks the whole packet. An index past the mask reads zero, which
234 /// leaves those bytes unchanged. The function follows the Lean definition `Quic.Protect.maskAt`.
235 fn modelMaskAt(mask: [mask_bytes]u8, index: usize) u8 {
236 return if (index < mask_bytes) mask[index] else 0;
237 }
238
239 /// Returns one byte of a packet after masking, for the per-byte rule the whole masking pass is
240 /// built from. The first byte takes the mask's first byte narrowed to the protected bits, each
241 /// packet number byte takes the mask byte that follows, and every other byte is left as it was. The
242 /// function follows the Lean definition `Quic.Protect.maskByte`.
243 fn modelMaskByte(
244 mask: [mask_bytes]u8,
245 first: u8,
246 offset: usize,
247 length: usize,
248 index: usize,
249 byte: u8,
250 ) u8 {
251 std.debug.assert(offset <= packet_bytes_max);
252 std.debug.assert(length <= 7);
253 if (index == 0) return byte ^ (modelMaskAt(mask, 0) & modelProtectedBits(first));
254 if (offset <= index and index < offset + length) {
255 return byte ^ modelMaskAt(mask, index - offset + 1);
256 }
257 return byte;
258 }
259
260 /// Writes the masked packet into a caller buffer of the same length, so both masking directions can
261 /// run it over the packet. Every byte is decided by the per-byte rule, with the packet's own first
262 /// byte deciding which bits are protected. An empty packet reads a first byte of zero, and the Lean
263 /// definition's indexed read gives the same byte there. The function follows the Lean definition
264 /// `Quic.Protect.applyMask`.
265 fn modelApplyMask(
266 mask: [mask_bytes]u8,
267 packet: []const u8,
268 offset: usize,
269 length: usize,
270 output: []u8,
271 ) void {
272 std.debug.assert(output.len == packet.len);
273 const first: u8 = if (packet.len == 0) 0 else packet[0];
274 for (packet, 0..) |byte, index| {
275 output[index] = modelMaskByte(mask, first, offset, length, index, byte);
276 }
277 }
278
279 /// Masks a packet's header into a caller buffer, after checking the offset and length, for a
280 /// property that compares it against the production masking of a header. The function follows the
281 /// Lean definition `Quic.Protect.protect`.
282 fn modelProtect(
283 mask: [mask_bytes]u8,
284 packet: []const u8,
285 offset: usize,
286 length: usize,
287 output: []u8,
288 ) ModelError!void {
289 try modelValidate(packet.len, offset, length);
290 modelApplyMask(mask, packet, offset, length, output);
291 }
292
293 const ModelInspected = struct {
294 first: u8,
295 length: usize,
296 };
297
298 /// Returns a packet's first byte with the mask taken off, so unmasking can recover the first byte
299 /// before reading how many packet number bytes to unmask. An empty packet reads a first byte of
300 /// zero. The function follows the Lean definition `Quic.Protect.unmaskedFirst`.
301 fn modelUnmaskedFirst(mask: [mask_bytes]u8, packet: []const u8) u8 {
302 const first: u8 = if (packet.len == 0) 0 else packet[0];
303 return first ^ (modelMaskAt(mask, 0) & modelProtectedBits(first));
304 }
305
306 /// Returns the unmasked first byte and the packet number length it declares, for a property that
307 /// compares it against the production header inspection that reads a header without changing it. An
308 /// empty packet gives `TruncatedPacket` and a zero offset gives `InvalidPacketNumberOffset`, both
309 /// before the first byte is unmasked. The function follows the Lean definition
310 /// `Quic.Protect.inspect`, including the order in which the checks fire.
311 fn modelInspect(
312 mask: [mask_bytes]u8,
313 packet: []const u8,
314 offset: usize,
315 ) ModelError!ModelInspected {
316 if (packet.len == 0) return error.TruncatedPacket;
317 if (offset == 0) return error.InvalidPacketNumberOffset;
318 const first = modelUnmaskedFirst(mask, packet);
319 try modelValidate(packet.len, offset, modelPacketNumberLength(first));
320 return .{ .first = first, .length = modelPacketNumberLength(first) };
321 }
322
323 /// Unmasks a packet's header into a caller buffer and returns the packet number length it found,
324 /// for a property that compares it against the production unmasking of a header. The function
325 /// follows the Lean definition `Quic.Protect.unprotect`.
326 fn modelUnprotect(
327 mask: [mask_bytes]u8,
328 packet: []const u8,
329 offset: usize,
330 output: []u8,
331 ) ModelError!usize {
332 const inspected = try modelInspect(mask, packet, offset);
333 modelApplyMask(mask, packet, offset, inspected.length, output);
334 return inspected.length;
335 }
336
337 /// Returns the offset at which the header protection sample begins, four bytes past the packet
338 /// number offset, so the mask can be derived from that sample of the encrypted payload. A packet
339 /// whose end leaves fewer than sixteen sample bytes gives `PacketTooShort`. The function follows
340 /// the Lean definition `Quic.Protect.sampleAt`.
341 fn modelSampleAt(offset: usize, packet_end: usize) ModelError!usize {
342 if (offset + sample_offset_bytes + sample_bytes <= packet_end) {
343 return offset + sample_offset_bytes;
344 }
345 return error.PacketTooShort;
346 }
347
348 test "RFC 9001 Appendix A.5 Lean nonce and header mask mirror vectors" {
349 const iv = [_]u8{
350 0xe0, 0x45, 0x9b, 0x34, 0x74, 0xbd, 0xd0, 0xe4, 0x4a, 0x41, 0xc1, 0x44,
351 };
352 const expected = [_]u8{
353 0xe0, 0x45, 0x9b, 0x34, 0x74, 0xbd, 0xd0, 0xe4, 0x6d, 0x41, 0x7e, 0xb0,
354 };
355 try std.testing.expectEqual(expected, modelNonce(iv, 654_360_564));
356 try std.testing.expectEqual(expected, crypto.packet.nonce(iv, 654_360_564));
357 const mask = [_]u8{ 0xae, 0xfe, 0xfe, 0x7d, 0x03 };
358 const packet = [_]u8{ 0x42, 0x00, 0xbf, 0xf4 };
359 var output: [packet.len]u8 = undefined;
360 try modelProtect(mask, &packet, 1, 3, &output);
361 try std.testing.expectEqual([_]u8{ 0x4c, 0xfe, 0x41, 0x89 }, output);
362 }
363
364 test "RFC 9001 section 5.4.2 Lean sample mirror minimum packet vectors" {
365 try std.testing.expectError(error.PacketTooShort, modelSampleAt(5, 24));
366 try std.testing.expectEqual(@as(usize, 9), try modelSampleAt(5, 25));
367 try std.testing.expectEqual(@as(usize, 5), try modelSampleAt(1, 21));
368 }
369
370 const NonceClass = enum(u2) {
371 zero,
372 one,
373 maximum,
374 random,
375 };
376
377 const NonceCoverage = struct {
378 classes: [std.meta.fieldNames(NonceClass).len]bool = @splat(false),
379
380 fn requireComplete(self: *const NonceCoverage) !void {
381 for (self.classes) |seen| try std.testing.expect(seen);
382 }
383 };
384
385 var nonce_coverage = NonceCoverage{};
386
387 const NonceMirror = struct {
388 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
389 const iv: [iv_bytes]u8 = (try data.drawBytes(iv_bytes, iv_bytes))[0..iv_bytes].*;
390 const class: NonceClass = @fromBackingInt(@intCast(try data.drawInteger(0, 3, 0)));
391 const packet_number: u62 = switch (class) {
392 .zero => 0,
393 .one => 1,
394 .maximum => std.math.maxInt(u62),
395 .random => @intCast(try data.drawInteger(0, std.math.maxInt(u62), 0)),
396 };
397 nonce_coverage.classes[@backingInt(class)] = true;
398 try std.testing.expectEqual(
399 modelNonce(iv, packet_number),
400 crypto.packet.nonce(iv, packet_number),
401 );
402 }
403 };
404
405 test "property: RFC 9001 section 5.3 Lean nonce mirror agrees with production" {
406 nonce_coverage = .{};
407 try hypothesis.checkNamed(NonceMirror, "quic-nonce-mirror", settings());
408 try nonce_coverage.requireComplete();
409 }
410
411 const MaskShape = enum(u3) {
412 exact,
413 sample,
414 random,
415 short,
416 zero_offset,
417 wrong_length,
418 };
419
420 const MaskCoverage = struct {
421 shapes: [std.meta.fieldNames(MaskShape).len]bool = @splat(false),
422 forms: [2]bool = @splat(false),
423 lengths: [4]bool = @splat(false),
424
425 fn requireComplete(self: *const MaskCoverage) !void {
426 for (self.shapes) |seen| try std.testing.expect(seen);
427 for (self.forms) |seen| try std.testing.expect(seen);
428 for (self.lengths) |seen| try std.testing.expect(seen);
429 }
430 };
431
432 var mask_coverage = MaskCoverage{};
433
434 const MaskDraw = struct {
435 mask: [mask_bytes]u8,
436 packet: [packet_bytes_max]u8,
437 len: usize,
438 offset: usize,
439 pn_len: u3,
440 };
441
442 fn drawMaskLength(data: *hypothesis.ConjectureData, shape: MaskShape) !u3 {
443 const wrong_lengths = [_]u3{ 0, 5, 6, 7 };
444 if (shape == .wrong_length) return wrong_lengths[@intCast(try data.drawInteger(0, 3, 0))];
445 const pn_len: u3 = @intCast(try data.drawInteger(1, 4, 1));
446 mask_coverage.lengths[pn_len - 1] = true;
447 return pn_len;
448 }
449
450 fn drawMaskShape(data: *hypothesis.ConjectureData) !MaskDraw {
451 var drawn: MaskDraw = undefined;
452 drawn.mask = (try data.drawBytes(mask_bytes, mask_bytes))[0..mask_bytes].*;
453 const shape: MaskShape = @fromBackingInt(@intCast(try data.drawInteger(0, 5, 0)));
454 mask_coverage.shapes[@backingInt(shape)] = true;
455 const long = try data.drawBoolean();
456 mask_coverage.forms[if (long) 1 else 0] = true;
457 drawn.pn_len = try drawMaskLength(data, shape);
458 drawn.offset = if (shape == .zero_offset) 0 else @intCast(try data.drawInteger(1, 8, 1));
459 const header_end = drawn.offset + drawn.pn_len;
460 drawn.len = switch (shape) {
461 .exact => header_end,
462 .sample, .wrong_length => drawn.offset + 20,
463 .random => @intCast(try data.drawInteger(0, packet_bytes_max, 0)),
464 .short => header_end - 1,
465 .zero_offset => @intCast(try data.drawInteger(1, packet_bytes_max, 1)),
466 };
467 std.debug.assert(drawn.len <= packet_bytes_max);
468 @memcpy(drawn.packet[0..drawn.len], try data.drawBytes(drawn.len, drawn.len));
469 if (drawn.len == 0) return drawn;
470 const form: u8 = if (long) 0x80 else 0x00;
471 const length_bits: u8 = @as(u8, drawn.pn_len -% 1) & 0x03;
472 drawn.packet[0] = (drawn.packet[0] & 0x7c) | form | length_bits;
473 return drawn;
474 }
475
476 fn compareInspect(mask: [mask_bytes]u8, packet: []const u8, offset: usize) !void {
477 const model_result = modelInspect(mask, packet, offset);
478 const production_result = crypto.header.inspect(mask, packet, offset);
479 const inspected = model_result catch |model_error| {
480 const production_error = if (production_result) |_|
481 return error.ProductionAcceptedLeanRejection
482 else |failure|
483 failure;
484 return expectSameError(model_error, production_error);
485 };
486 const production = production_result catch return error.ProductionRejectedLeanAcceptance;
487 try std.testing.expectEqual(inspected.first, production.first_byte);
488 try std.testing.expectEqual(inspected.length, @as(usize, production.pn_len));
489 }
490
491 fn compareProtect(
492 mask: [mask_bytes]u8,
493 packet: []const u8,
494 offset: usize,
495 pn_len: u3,
496 ) !?[packet_bytes_max]u8 {
497 var model_bytes: [packet_bytes_max]u8 = undefined;
498 const model_result = modelProtect(mask, packet, offset, pn_len, model_bytes[0..packet.len]);
499 var production_bytes: [packet_bytes_max]u8 = undefined;
500 @memcpy(production_bytes[0..packet.len], packet);
501 const production_result = crypto.header.protect(
502 mask,
503 production_bytes[0..packet.len],
504 offset,
505 pn_len,
506 );
507 model_result catch |model_error| {
508 const production_error = if (production_result) |_|
509 return error.ProductionAcceptedLeanRejection
510 else |failure|
511 failure;
512 try expectSameError(model_error, production_error);
513 try std.testing.expectEqualSlices(u8, packet, production_bytes[0..packet.len]);
514 return null;
515 };
516 production_result catch return error.ProductionRejectedLeanAcceptance;
517 try std.testing.expectEqualSlices(
518 u8,
519 model_bytes[0..packet.len],
520 production_bytes[0..packet.len],
521 );
522 return production_bytes;
523 }
524
525 const Unprotected = struct {
526 bytes: [packet_bytes_max]u8,
527 length: usize,
528 };
529
530 fn compareUnprotect(mask: [mask_bytes]u8, packet: []const u8, offset: usize) !?Unprotected {
531 try compareInspect(mask, packet, offset);
532 var model_bytes: [packet_bytes_max]u8 = undefined;
533 const model_result = modelUnprotect(mask, packet, offset, model_bytes[0..packet.len]);
534 var production_bytes: [packet_bytes_max]u8 = undefined;
535 @memcpy(production_bytes[0..packet.len], packet);
536 const production_result = crypto.header.unprotect(
537 mask,
538 production_bytes[0..packet.len],
539 offset,
540 );
541 const model_length = model_result catch |model_error| {
542 const production_error = if (production_result) |_|
543 return error.ProductionAcceptedLeanRejection
544 else |failure|
545 failure;
546 try expectSameError(model_error, production_error);
547 try std.testing.expectEqualSlices(u8, packet, production_bytes[0..packet.len]);
548 return null;
549 };
550 const production_length = production_result catch
551 return error.ProductionRejectedLeanAcceptance;
552 try std.testing.expectEqual(model_length, @as(usize, production_length));
553 try std.testing.expectEqualSlices(
554 u8,
555 model_bytes[0..packet.len],
556 production_bytes[0..packet.len],
557 );
558 return .{ .bytes = production_bytes, .length = model_length };
559 }
560
561 const MaskMirror = struct {
562 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
563 const drawn = try drawMaskShape(data);
564 const packet = drawn.packet[0..drawn.len];
565 const protected = try compareProtect(drawn.mask, packet, drawn.offset, drawn.pn_len);
566 _ = try compareUnprotect(drawn.mask, packet, drawn.offset);
567 const bytes = protected orelse return;
568 const unprotected = try compareUnprotect(drawn.mask, bytes[0..drawn.len], drawn.offset);
569 const recovered = unprotected orelse return error.ProtectedPacketRejected;
570 try std.testing.expectEqual(@as(usize, drawn.pn_len), recovered.length);
571 try std.testing.expectEqualSlices(u8, packet, recovered.bytes[0..drawn.len]);
572 }
573 };
574
575 test "property: RFC 9001 section 5.4.1 Lean header mask mirror agrees with production" {
576 mask_coverage = .{};
577 rejection_coverage = .{};
578 try hypothesis.checkNamed(MaskMirror, "quic-header-mask-mirror", settings());
579 try mask_coverage.requireComplete();
580 try rejection_coverage.require(&header_rejections);
581 }
582
583 const SampleShape = enum(u2) {
584 below,
585 exact,
586 above,
587 random,
588 };
589
590 const SampleCoverage = struct {
591 shapes: [std.meta.fieldNames(SampleShape).len]bool = @splat(false),
592 suites: [2]bool = @splat(false),
593 seal_fits: [2]bool = @splat(false),
594
595 fn requireComplete(self: *const SampleCoverage) !void {
596 for (self.shapes) |seen| try std.testing.expect(seen);
597 for (self.suites) |seen| try std.testing.expect(seen);
598 for (self.seal_fits) |seen| try std.testing.expect(seen);
599 }
600 };
601
602 var sample_coverage = SampleCoverage{};
603
604 fn checkOpenSample(
605 data: *hypothesis.ConjectureData,
606 keys: *const crypto.Keys,
607 offset: usize,
608 ) !void {
609 const shape: SampleShape = @fromBackingInt(@intCast(try data.drawInteger(0, 3, 0)));
610 sample_coverage.shapes[@backingInt(shape)] = true;
611 const boundary = offset + sample_offset_bytes + sample_bytes;
612 const len: usize = switch (shape) {
613 .below => boundary - 1,
614 .exact => boundary,
615 .above => boundary + 1,
616 .random => @intCast(try data.drawInteger(offset, packet_bytes_max, offset)),
617 };
618 var packet: [packet_bytes_max]u8 = undefined;
619 @memcpy(packet[0..len], try data.drawBytes(len, len));
620 packet[0] = 0x40 | (packet[0] & 0x3f);
621 const before = packet;
622 const model_result = modelSampleAt(offset, len);
623 const production_result = crypto.packet.unprotect(keys, packet[0..len], offset, null);
624 const sample_offset = model_result catch |model_error| {
625 const production_error = if (production_result) |_|
626 return error.ProductionAcceptedLeanRejection
627 else |failure|
628 failure;
629 return expectSameError(model_error, production_error);
630 };
631 const header = production_result catch return error.ProductionRejectedLeanAcceptance;
632 try std.testing.expectEqual(len, header.packet_end);
633 try std.testing.expectEqualSlices(
634 u8,
635 before[sample_offset..][0..sample_bytes],
636 packet[sample_offset..][0..sample_bytes],
637 );
638 }
639
640 fn checkSealSample(data: *hypothesis.ConjectureData, keys: *crypto.Keys, offset: usize) !void {
641 const pn_len: u3 = @intCast(try data.drawInteger(1, 4, 1));
642 const payload_len: u16 = @intCast(try data.drawInteger(0, 5, 0));
643 const packet_number_max = (@as(u64, 1) << (@as(u6, pn_len) * 8)) - 1;
644 const packet_number: u62 = @intCast(try data.drawInteger(0, packet_number_max, 0));
645 const packet_end = offset + pn_len + payload_len + crypto.packet.tag_bytes;
646 std.debug.assert(packet_end <= packet_bytes_max);
647 var packet: [packet_bytes_max]u8 = @splat(0);
648 packet[0] = 0x40 | @as(u8, pn_len - 1);
649 var encoded: [8]u8 = undefined;
650 std.mem.writeInt(u64, &encoded, packet_number, .big);
651 @memcpy(packet[offset..][0..pn_len], encoded[encoded.len - pn_len ..]);
652 const model_result = modelSampleAt(offset, packet_end);
653 const production_result = crypto.packet.seal(
654 keys,
655 packet_number,
656 packet[0..packet_end],
657 offset,
658 pn_len,
659 payload_len,
660 );
661 _ = model_result catch |model_error| {
662 sample_coverage.seal_fits[0] = true;
663 const production_error = if (production_result) |_|
664 return error.ProductionAcceptedLeanRejection
665 else |failure|
666 failure;
667 return expectSameError(model_error, production_error);
668 };
669 sample_coverage.seal_fits[1] = true;
670 production_result catch return error.ProductionRejectedLeanAcceptance;
671 }
672
673 const SampleMirror = struct {
674 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
675 const suite: crypto.Suite = if (try data.drawBoolean())
676 .aes_128_gcm_sha256
677 else
678 .chacha20_poly1305_sha256;
679 sample_coverage.suites[@backingInt(suite)] = true;
680 var secret: crypto.Secret = undefined;
681 @memcpy(&secret, try data.drawBytes(secret_bytes, secret_bytes));
682 const offset: usize = @intCast(try data.drawInteger(1, offset_max, 1));
683 var storage: KeyStorage = undefined;
684 var keys = try crypto.Keys.derive(&storage, suite, secret);
685 defer _ = keys.deinit();
686 try checkOpenSample(data, &keys, offset);
687 try checkSealSample(data, &keys, offset);
688 }
689 };
690
691 test "property: RFC 9001 section 5.4.2 Lean sample mirror agrees with production" {
692 sample_coverage = .{};
693 rejection_coverage = .{};
694 try hypothesis.checkNamed(SampleMirror, "quic-sample-mirror", settings());
695 try sample_coverage.requireComplete();
696 try rejection_coverage.require(&sample_rejections);
697 }
698
699 fn hexBytes(comptime text: []const u8) [text.len / 2]u8 {
700 var result: [text.len / 2]u8 = undefined;
701 _ = std.fmt.hexToBytes(&result, text) catch unreachable;
702 return result;
703 }
704
705 fn expectSameResult(model_error: ModelError, production: anyerror!void) !void {
706 if (production) |_| return error.ProductionAcceptedLeanRejection else |production_error| {
707 try expectSameError(model_error, production_error);
708 }
709 }
710
711 /// Derives a value of a given length from a secret under a label and a context, for every
712 /// derivation in the key schedule mirror. The Lean key schedule takes that derivation as a
713 /// parameter, and this function supplies HKDF over SHA-256 for it.
714 fn kdfExpandLabel(
715 secret: crypto.Secret,
716 label: []const u8,
717 context: []const u8,
718 comptime length: usize,
719 ) [length]u8 {
720 return std.crypto.tls.hkdfExpandLabel(Hkdf, secret, label, context, length);
721 }
722
723 /// The twenty-byte salt for QUIC version 1 Initial secrets, for extracting those Initial secrets.
724 /// The constant follows the Lean definition `Quic.Schedule.initialSalt`, and holds the same bytes
725 /// the shipped code uses.
726 const model_initial_salt = [_]u8{
727 0x38, 0x76, 0x2c, 0xf7, 0xf5, 0x59, 0x34, 0xb3, 0x4d, 0x17,
728 0x9a, 0xe6, 0xa4, 0xc8, 0x0c, 0xad, 0xcc, 0xbb, 0x7f, 0x0a,
729 };
730
731 /// The client and server traffic secrets a connection starts from, for a property that compares
732 /// them against the production Initial secrets. The type follows the Lean definition
733 /// `Quic.Schedule.InitialSecrets`.
734 const ModelInitialSecrets = struct {
735 client: crypto.Secret,
736 server: crypto.Secret,
737 };
738
739 /// Derives the client and server Initial traffic secrets from a client's destination connection ID,
740 /// for a property that draws a connection ID and compares both implementations' Initial secrets for
741 /// it. The connection ID is extracted under the Initial salt, and the two secrets are expanded from
742 /// the result under the "client in" and "server in" labels. The function follows the Lean
743 /// definition `Quic.Schedule.initialSecrets`, with HKDF extraction standing in for that
744 /// definition's extraction parameter.
745 fn modelInitialSecrets(dcid: []const u8) ModelInitialSecrets {
746 const initial = Hkdf.extract(&model_initial_salt, dcid);
747 return .{
748 .client = kdfExpandLabel(initial, "client in", "", secret_bytes),
749 .server = kdfExpandLabel(initial, "server in", "", secret_bytes),
750 };
751 }
752
753 /// The packet key, initialization vector, and header key derived from one traffic secret, for a
754 /// property that compares them field by field against the production keys. Both keys are held in 32
755 /// bytes and the shorter suite's keys are zero-padded, which is how the production key storage
756 /// holds them. The type follows the Lean definition `Quic.Schedule.Material`.
757 const ModelMaterial = struct {
758 key: [32]u8,
759 iv: [iv_bytes]u8,
760 hp: [32]u8,
761 };
762
763 /// Derives the packet key, initialization vector, and header key from one traffic secret for one
764 /// cipher suite, for a property that compares them against the production derivation for both
765 /// suites. The labels are "quic key", "quic iv", and "quic hp". Each suite's branch fixes its own
766 /// key length, 16 bytes or 32. The function follows the Lean definition `Quic.Schedule.material`,
767 /// whose key length it fixes per branch.
768 fn modelMaterial(suite: crypto.Suite, secret: crypto.Secret) ModelMaterial {
769 var result = ModelMaterial{
770 .key = @splat(0),
771 .iv = kdfExpandLabel(secret, "quic iv", "", iv_bytes),
772 .hp = @splat(0),
773 };
774 switch (suite) {
775 .aes_128_gcm_sha256 => {
776 result.key[0..16].* = kdfExpandLabel(secret, "quic key", "", 16);
777 result.hp[0..16].* = kdfExpandLabel(secret, "quic hp", "", 16);
778 },
779 .chacha20_poly1305_sha256 => {
780 result.key = kdfExpandLabel(secret, "quic key", "", 32);
781 result.hp = kdfExpandLabel(secret, "quic hp", "", 32);
782 },
783 }
784 return result;
785 }
786
787 /// Returns the traffic secret that follows a given one, expanded under the label `quic ku`, so key
788 /// updates in the mirror derive their next secret through it. The function follows the Lean
789 /// definition `Quic.Schedule.nextSecret`.
790 fn modelNextSecret(secret: crypto.Secret) crypto.Secret {
791 return kdfExpandLabel(secret, "quic ku", "", secret_bytes);
792 }
793
794 /// Returns the material for a new traffic secret, keeping the header key the old material had, for
795 /// a property that compares it against a production key update. The header key carries over, so the
796 /// update reaches the packet keys alone. The function follows the Lean definition
797 /// `Quic.Schedule.update`.
798 fn modelUpdate(suite: crypto.Suite, current: ModelMaterial, secret: crypto.Secret) ModelMaterial {
799 const next = modelMaterial(suite, secret);
800 return .{ .key = next.key, .iv = next.iv, .hp = current.hp };
801 }
802
803 /// The five secrets the TLS handshake schedule produces, for a property that compares them against
804 /// the production handshake schedule: the early secret, the handshake secret, the two handshake
805 /// traffic secrets, and the master secret. The type follows the Lean definition
806 /// `Quic.Schedule.Handshake`.
807 const ModelHandshake = struct {
808 early: crypto.Secret,
809 handshake: crypto.Secret,
810 client_handshake: crypto.Secret,
811 server_handshake: crypto.Secret,
812 master: crypto.Secret,
813 };
814
815 /// Derives the handshake schedule from an empty-string hash, the key exchange result, and the
816 /// transcript hash up to the hellos, for a property that draws a shared secret and two transcript
817 /// hashes and compares both implementations' schedules. Each stage extracts with the previous
818 /// secret derived under the "derived" label, and the two traffic secrets come from the "c hs
819 /// traffic" and "s hs traffic" labels. The function follows the Lean definition
820 /// `Quic.Schedule.handshake`.
821 fn modelHandshake(
822 empty_hash: crypto.Secret,
823 shared_secret: crypto.Secret,
824 hello_hash: crypto.Secret,
825 ) ModelHandshake {
826 const zero: crypto.Secret = @splat(0);
827 const early = Hkdf.extract(&zero, &zero);
828 const early_derived = kdfExpandLabel(early, "derived", &empty_hash, secret_bytes);
829 const handshake_secret = Hkdf.extract(&early_derived, &shared_secret);
830 const handshake_derived = kdfExpandLabel(
831 handshake_secret,
832 "derived",
833 &empty_hash,
834 secret_bytes,
835 );
836 return .{
837 .early = early,
838 .handshake = handshake_secret,
839 .client_handshake = kdfExpandLabel(
840 handshake_secret,
841 "c hs traffic",
842 &hello_hash,
843 secret_bytes,
844 ),
845 .server_handshake = kdfExpandLabel(
846 handshake_secret,
847 "s hs traffic",
848 &hello_hash,
849 secret_bytes,
850 ),
851 .master = Hkdf.extract(&handshake_derived, &zero),
852 };
853 }
854
855 /// The two application traffic secrets and the exporter secret, for a property that compares them
856 /// against the production application secrets. The type follows the Lean definition
857 /// `Quic.Schedule.Application`.
858 const ModelApplication = struct {
859 client: crypto.Secret,
860 server: crypto.Secret,
861 exporter: crypto.Secret,
862 };
863
864 /// Derives the two application traffic secrets and the exporter secret from the master secret and
865 /// the transcript hash, for a property that compares them against the production derivation of the
866 /// 1-RTT secrets. The labels are "c ap traffic", "s ap traffic", and "exp master". The function
867 /// follows the Lean definition `Quic.Schedule.application`.
868 fn modelApplication(master: crypto.Secret, transcript_hash: crypto.Secret) ModelApplication {
869 return .{
870 .client = kdfExpandLabel(master, "c ap traffic", &transcript_hash, secret_bytes),
871 .server = kdfExpandLabel(master, "s ap traffic", &transcript_hash, secret_bytes),
872 .exporter = kdfExpandLabel(master, "exp master", &transcript_hash, secret_bytes),
873 };
874 }
875
876 fn expectMaterial(keys: *const crypto.Keys, material: ModelMaterial) !void {
877 try std.testing.expectEqual(material.key, keys.packetKey());
878 try std.testing.expectEqual(material.iv, keys.initializationVector());
879 try std.testing.expectEqual(material.hp, keys.headerKey());
880 }
881
882 /// The length of a Retry integrity tag in bytes, 16, for the Retry mirror's length checks that are
883 /// stated against it. The constant follows the Lean definition `Quic.Retry.tagBytes`.
884 const model_retry_tag_bytes: usize = 16;
885 /// The largest connection ID the Retry tag covers, 20 bytes, so the Retry mirror can reject a
886 /// longer connection ID against it. The constant follows the Lean definition
887 /// `Quic.Retry.connectionIdBytesMax`.
888 const model_connection_id_bytes_max: usize = 20;
889 /// The largest Retry packet in bytes, 65,527, so the Retry mirror can reject a longer packet
890 /// against it. The constant follows the Lean definition `Quic.Retry.packetBytesMax`.
891 const model_retry_packet_bytes_max: usize = 65_527;
892 /// The largest body the Retry tag can cover, the largest packet less the tag, so the Retry mirror
893 /// can reject a longer authenticated body against it. The constant follows the Lean definition
894 /// `Quic.Retry.pseudoBytesMax`.
895 const model_pseudo_bytes_max: usize = model_retry_packet_bytes_max - model_retry_tag_bytes;
896 const retry_body_bytes_max: usize = 1200;
897 /// The 16-byte AES-128 key RFC 9001 section 5.8 fixes for QUIC version 1 Retry integrity tags, for
898 /// the mirror's tag computation that uses it. The mirror keeps its own copy of the value, and that
899 /// copy matches the one the shipped code holds.
900 const retry_key = [_]u8{
901 0xbe, 0x0c, 0x69, 0x0b, 0x9f, 0x66, 0x57, 0x5a,
902 0x1d, 0x76, 0x6b, 0x54, 0xe3, 0x68, 0xc8, 0x4e,
903 };
904 /// The 12-byte nonce RFC 9001 section 5.8 fixes for QUIC version 1 Retry integrity tags, for
905 /// pairing with the key in the same computation. The mirror keeps its own copy of the value, and
906 /// that copy matches the one the shipped code holds.
907 const retry_nonce = [_]u8{
908 0x46, 0x15, 0x99, 0xd3, 0x5d, 0x63,
909 0x2b, 0xf2, 0x23, 0x98, 0x25, 0xbb,
910 };
911
912 /// Returns the authentication tag over a Retry pseudo-packet, filling in the authentication step
913 /// that the Lean Retry definition leaves open. The Lean Retry definition takes the tag computation
914 /// as a parameter, and this function supplies AES-128-GCM over an empty plaintext with the
915 /// pseudo-packet as associated data.
916 fn retryMac(pseudo: []const u8) [model_retry_tag_bytes]u8 {
917 var tag: [model_retry_tag_bytes]u8 = undefined;
918 var empty: [0]u8 = .{};
919 Aes128Gcm.encrypt(&empty, &tag, &empty, pseudo, retry_nonce, retry_key);
920 return tag;
921 }
922
923 /// Writes the bytes a Retry tag covers into caller storage, so the mirror lays them out the same
924 /// way the tag computation requires: the original destination connection ID's length, those bytes,
925 /// then the Retry packet's body. The function follows the Lean definition `Quic.Retry.pseudo`, into
926 /// a caller buffer. The caller's buffer holds the whole result, which debug builds check.
927 fn modelPseudo(odcid: []const u8, body: []const u8, output: []u8) []const u8 {
928 const length = 1 + odcid.len + body.len;
929 std.debug.assert(length <= output.len);
930 output[0] = @truncate(odcid.len);
931 @memcpy(output[1..][0..odcid.len], odcid);
932 @memcpy(output[1 + odcid.len ..][0..body.len], body);
933 return output[0..length];
934 }
935
936 /// Returns the Retry integrity tag for one original destination connection ID and one packet body,
937 /// for a property that compares it against the production tag for drawn inputs. A connection ID
938 /// past 20 bytes gives `ConnectionIdTooLong` and a body past the pseudo-packet bound gives
939 /// `PacketTooLarge`, both before any byte is read. The function follows the Lean definition
940 /// `Quic.Retry.tag`.
941 fn modelRetryTag(
942 odcid: []const u8,
943 body: []const u8,
944 scratch: []u8,
945 ) ModelError![model_retry_tag_bytes]u8 {
946 if (model_connection_id_bytes_max < odcid.len) return error.ConnectionIdTooLong;
947 if (model_pseudo_bytes_max < body.len) return error.PacketTooLarge;
948 return retryMac(modelPseudo(odcid, body, scratch));
949 }
950
951 /// Returns the trailing tag bytes of a Retry packet, so verification can compare against the tag
952 /// that the packet carries. A packet shorter than a tag gives the whole packet, because the
953 /// subtraction saturates. The function follows the Lean definition `Quic.Retry.tagOf`.
954 fn modelTagOf(packet: []const u8) []const u8 {
955 return packet[packet.len -| model_retry_tag_bytes..];
956 }
957
958 /// Reports whether a Retry packet's trailing tag is the one its body and a given original
959 /// destination connection ID produce, for a property that compares it against the production
960 /// verification for drawn packets. A connection ID past 20 bytes, a packet no longer than a tag, or
961 /// a packet past the largest Retry packet all give false. The function follows the Lean definition
962 /// `Quic.Retry.verify`.
963 fn modelRetryVerify(odcid: []const u8, packet: []const u8, scratch: []u8) bool {
964 if (model_connection_id_bytes_max < odcid.len) return false;
965 if (packet.len <= model_retry_tag_bytes) return false;
966 if (model_retry_packet_bytes_max < packet.len) return false;
967 const body = packet[0 .. packet.len - model_retry_tag_bytes];
968 const expected = modelRetryTag(odcid, body, scratch) catch return false;
969 return std.mem.eql(u8, &expected, modelTagOf(packet));
970 }
971
972 /// The twelve bytes that open an Ed25519 public key in its RFC 8410 SubjectPublicKeyInfo encoding,
973 /// so every encoded identity starts with it and decoding can check for it. The constant follows the
974 /// Lean definition `Quic.Identity.spkiPrefix`.
975 const model_spki_prefix = [_]u8{
976 0x30, 0x2a, 0x30, 0x05, 0x06, 0x03, 0x2b, 0x65, 0x70, 0x03, 0x21, 0x00,
977 };
978 /// The length of an Ed25519 public key in bytes, 32, so the encoding's length can be stated against
979 /// it. The constant follows the Lean definition `Quic.Identity.publicKeyBytes`.
980 const model_public_key_bytes: usize = 32;
981 /// The length of the whole encoded identity in bytes, 44, so decoding can reject any other length
982 /// against it. The constant follows the Lean definition `Quic.Identity.spkiLength`.
983 const model_spki_length: usize = 44;
984
985 /// Returns an Ed25519 public key in its RFC 8410 SubjectPublicKeyInfo encoding, for a property that
986 /// compares it against the production encoding for drawn keys. The fixed prefix is followed by the
987 /// key's own bytes. The function follows the Lean definition `Quic.Identity.encodeSpki`.
988 fn modelEncodeSpki(public_key: [model_public_key_bytes]u8) [model_spki_length]u8 {
989 var result: [model_spki_length]u8 = undefined;
990 result[0..model_spki_prefix.len].* = model_spki_prefix;
991 result[model_spki_prefix.len..].* = public_key;
992 return result;
993 }
994
995 /// Returns the Ed25519 public key an encoded identity carries, for a property that compares it
996 /// against the production decoding for drawn bytes. A length other than 44 bytes gives
997 /// `InvalidLength`, and a different opening gives `InvalidPrefix`. The function follows the Lean
998 /// definition `Quic.Identity.decodeSpki`.
999 fn modelDecodeSpki(encoded: []const u8) ModelError![model_public_key_bytes]u8 {
1000 if (encoded.len != model_spki_length) return error.InvalidLength;
1001 if (!std.mem.eql(u8, encoded[0..model_spki_prefix.len], &model_spki_prefix)) {
1002 return error.InvalidPrefix;
1003 }
1004 return encoded[model_spki_prefix.len..][0..model_public_key_bytes].*;
1005 }
1006
1007 test "RFC 9001 Appendix A.1 and A.4 Lean key schedule and Retry mirror vectors" {
1008 const dcid = hexBytes("8394c8f03e515708");
1009 const secrets = modelInitialSecrets(&dcid);
1010 try std.testing.expectEqual(
1011 hexBytes("c00cf151ca5be075ed0ebfb5c80323c42d6b7db67881289af4008f1f6c357aea"),
1012 secrets.client,
1013 );
1014 const material = modelMaterial(.aes_128_gcm_sha256, secrets.client);
1015 try std.testing.expectEqual(
1016 hexBytes("1f369613dd76d5467730efcbe3b1a22d"),
1017 material.key[0..16].*,
1018 );
1019 try std.testing.expectEqual(hexBytes("fa044b2f42a3fd3b46fb255c"), material.iv);
1020 try std.testing.expectEqual(hexBytes("9f50449e04a0e810283a1e9933adedd2"), material.hp[0..16].*);
1021 const retry_packet = hexBytes(
1022 "ff000000010008f067a5502a4262b5746f6b656e04a265ba2eff4d829058fb3f0f2496ba",
1023 );
1024 var scratch: [1 + model_connection_id_bytes_max + retry_packet.len]u8 = undefined;
1025 try std.testing.expect(modelRetryVerify(&dcid, &retry_packet, &scratch));
1026 }
1027
1028 const DcidClass = enum(u2) {
1029 empty,
1030 eight,
1031 maximum,
1032 random,
1033 };
1034
1035 const ScheduleCoverage = struct {
1036 dcids: [std.meta.fieldNames(DcidClass).len]bool = @splat(false),
1037 suites: [2]bool = @splat(false),
1038
1039 fn requireComplete(self: *const ScheduleCoverage) !void {
1040 for (self.dcids) |seen| try std.testing.expect(seen);
1041 for (self.suites) |seen| try std.testing.expect(seen);
1042 }
1043 };
1044
1045 var schedule_coverage = ScheduleCoverage{};
1046
1047 fn drawSecret(data: *hypothesis.ConjectureData) !crypto.Secret {
1048 var secret: crypto.Secret = undefined;
1049 @memcpy(&secret, try data.drawBytes(secret_bytes, secret_bytes));
1050 return secret;
1051 }
1052
1053 const InitialSecretsMirror = struct {
1054 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
1055 const class: DcidClass = @fromBackingInt(@intCast(try data.drawInteger(0, 3, 0)));
1056 const dcid_length: usize = switch (class) {
1057 .empty => 0,
1058 .eight => 8,
1059 .maximum => model_connection_id_bytes_max,
1060 .random => @intCast(try data.drawInteger(0, model_connection_id_bytes_max, 0)),
1061 };
1062 schedule_coverage.dcids[@backingInt(class)] = true;
1063 const dcid = try data.drawBytes(dcid_length, dcid_length);
1064 const model_secrets = modelInitialSecrets(dcid);
1065 const production_secrets = crypto.initial.secrets(dcid);
1066 try std.testing.expectEqual(model_secrets.client, production_secrets.client);
1067 try std.testing.expectEqual(model_secrets.server, production_secrets.server);
1068
1069 const suite: crypto.Suite = if (try data.drawBoolean())
1070 .aes_128_gcm_sha256
1071 else
1072 .chacha20_poly1305_sha256;
1073 schedule_coverage.suites[@backingInt(suite)] = true;
1074 const secret = try drawSecret(data);
1075 var storage: KeyStorage = undefined;
1076 var keys = try crypto.Keys.derive(&storage, suite, secret);
1077 defer _ = keys.deinit();
1078 const material = modelMaterial(suite, secret);
1079 try expectMaterial(&keys, material);
1080 const next = modelNextSecret(secret);
1081 try std.testing.expectEqual(next, crypto.Keys.next(suite, secret));
1082 keys.update(next);
1083 try expectMaterial(&keys, modelUpdate(suite, material, next));
1084
1085 const shared_secret = try drawSecret(data);
1086 const hello_hash = try drawSecret(data);
1087 const transcript_hash = try drawSecret(data);
1088 const empty_hash = std.crypto.tls.emptyHash(Sha256);
1089 const model_handshake = modelHandshake(empty_hash, shared_secret, hello_hash);
1090 const schedule = quic.tls.schedule.Schedule.init(shared_secret, hello_hash);
1091 try std.testing.expectEqual(model_handshake.early, schedule.early);
1092 try std.testing.expectEqual(model_handshake.handshake, schedule.handshake);
1093 try std.testing.expectEqual(model_handshake.client_handshake, schedule.client_handshake);
1094 try std.testing.expectEqual(model_handshake.server_handshake, schedule.server_handshake);
1095 try std.testing.expectEqual(model_handshake.master, schedule.master);
1096 const model_application = modelApplication(model_handshake.master, transcript_hash);
1097 const application = schedule.application(transcript_hash);
1098 try std.testing.expectEqual(model_application.client, application.client);
1099 try std.testing.expectEqual(model_application.server, application.server);
1100 try std.testing.expectEqual(model_application.exporter, application.exporter);
1101 }
1102 };
1103
1104 test "property: RFC 9001 sections 5.1 and 5.2 Lean key schedule mirror agrees with production" {
1105 schedule_coverage = .{};
1106 try hypothesis.checkNamed(InitialSecretsMirror, "quic-initial-secrets-mirror", settings());
1107 try schedule_coverage.requireComplete();
1108 }
1109
1110 const OdcidClass = enum(u2) {
1111 empty,
1112 maximum,
1113 too_long,
1114 };
1115
1116 const RetryBodyClass = enum(u2) {
1117 empty,
1118 one,
1119 large,
1120 oversized,
1121 };
1122
1123 const RetryCoverage = struct {
1124 odcids: [std.meta.fieldNames(OdcidClass).len]bool = @splat(false),
1125 bodies: [std.meta.fieldNames(RetryBodyClass).len]bool = @splat(false),
1126 verified: [2]bool = @splat(false),
1127
1128 fn requireComplete(self: *const RetryCoverage) !void {
1129 for (self.odcids) |seen| try std.testing.expect(seen);
1130 for (self.bodies) |seen| try std.testing.expect(seen);
1131 for (self.verified) |seen| try std.testing.expect(seen);
1132 }
1133 };
1134
1135 var retry_coverage = RetryCoverage{};
1136
1137 fn compareRetryTag(odcid: []const u8, body: []const u8, scratch: []u8) !void {
1138 const production = crypto.retry.tag(odcid, body);
1139 const model_tag = modelRetryTag(odcid, body, scratch) catch |model_error| {
1140 return expectSameResult(model_error, if (production) |_| {} else |failure| failure);
1141 };
1142 try std.testing.expectEqual(model_tag, try production);
1143 }
1144
1145 fn compareRetryVerify(odcid: []const u8, packet: []const u8, scratch: []u8) !bool {
1146 const verified = modelRetryVerify(odcid, packet, scratch);
1147 try std.testing.expectEqual(verified, crypto.retry.verify(odcid, packet));
1148 return verified;
1149 }
1150
1151 /// Compares both implementations on a Retry body and a Retry packet whose stated lengths run past
1152 /// the bounds, over a one-byte buffer, so a property can reach the two length rejections without
1153 /// building a buffer of that size. A one-byte buffer suffices because both implementations reject
1154 /// those lengths before they read a byte. The call returns what the oversized verification
1155 /// reported.
1156 fn compareOversizedRetry(odcid: []const u8, scratch: []u8) !bool {
1157 const anchor = [_]u8{0};
1158 const many: [*]const u8 = &anchor;
1159 try compareRetryTag(odcid, many[0 .. model_pseudo_bytes_max + 1], scratch);
1160 return compareRetryVerify(odcid, many[0 .. model_retry_packet_bytes_max + 1], scratch);
1161 }
1162
1163 const RetryMirror = struct {
1164 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
1165 const odcid_class: OdcidClass = @fromBackingInt(@intCast(try data.drawInteger(0, 2, 0)));
1166 const odcid_length: usize = switch (odcid_class) {
1167 .empty => 0,
1168 .maximum => model_connection_id_bytes_max,
1169 .too_long => model_connection_id_bytes_max + 1,
1170 };
1171 const odcid = try data.drawBytes(odcid_length, odcid_length);
1172 const body_class: RetryBodyClass = @fromBackingInt(@intCast(try data.drawInteger(0, 3, 0)));
1173 retry_coverage.odcids[@backingInt(odcid_class)] = true;
1174 retry_coverage.bodies[@backingInt(body_class)] = true;
1175 var scratch: [1 + model_connection_id_bytes_max + retry_body_bytes_max]u8 = undefined;
1176 if (body_class == .oversized) {
1177 const oversized_verified = try compareOversizedRetry(odcid, &scratch);
1178 retry_coverage.verified[@intFromBool(oversized_verified)] = true;
1179 return;
1180 }
1181 const body_length: usize = switch (body_class) {
1182 .empty => 0,
1183 .one => 1,
1184 .large, .oversized => retry_body_bytes_max,
1185 };
1186 const body = try data.drawBytes(body_length, body_length);
1187 try compareRetryTag(odcid, body, &scratch);
1188 var packet: [retry_body_bytes_max + model_retry_tag_bytes]u8 = undefined;
1189 @memcpy(packet[0..body.len], body);
1190 const drawn_tag: [model_retry_tag_bytes]u8 = (try data.drawBytes(16, 16))[0..16].*;
1191 const tag = modelRetryTag(odcid, body, &scratch) catch drawn_tag;
1192 packet[body.len..][0..model_retry_tag_bytes].* = tag;
1193 const tagged = packet[0 .. body.len + model_retry_tag_bytes];
1194 const verified = try compareRetryVerify(odcid, tagged, &scratch);
1195 retry_coverage.verified[@intFromBool(verified)] = true;
1196 _ = try compareRetryVerify(odcid, tagged[0 .. tagged.len - 1], &scratch);
1197 packet[body.len] ^= 0x01;
1198 try std.testing.expect(!try compareRetryVerify(odcid, tagged, &scratch));
1199 }
1200 };
1201
1202 test "property: RFC 9001 section 5.8 Lean Retry mirror agrees with production" {
1203 retry_coverage = .{};
1204 rejection_coverage = .{};
1205 try hypothesis.checkNamed(RetryMirror, "quic-retry-mirror", settings());
1206 try retry_coverage.requireComplete();
1207 try rejection_coverage.require(&retry_rejections);
1208 }
1209
1210 const SpkiClass = enum(u3) {
1211 valid,
1212 short,
1213 long,
1214 wrong_prefix,
1215 random,
1216 };
1217
1218 const SpkiCoverage = struct {
1219 classes: [std.meta.fieldNames(SpkiClass).len]bool = @splat(false),
1220
1221 fn requireComplete(self: *const SpkiCoverage) !void {
1222 for (self.classes) |seen| try std.testing.expect(seen);
1223 }
1224 };
1225
1226 var spki_coverage = SpkiCoverage{};
1227
1228 fn compareSpkiDecode(input: []const u8) !void {
1229 const production = quic.tls.decodeSubjectPublicKeyInfo(input);
1230 const public_key = modelDecodeSpki(input) catch |model_error| {
1231 return expectSameResult(model_error, if (production) |_| {} else |failure| failure);
1232 };
1233 try std.testing.expectEqual(public_key, try production);
1234 }
1235
1236 const SpkiMirror = struct {
1237 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
1238 const class: SpkiClass = @fromBackingInt(@intCast(try data.drawInteger(0, 4, 0)));
1239 spki_coverage.classes[@backingInt(class)] = true;
1240 const public_key: [model_public_key_bytes]u8 = (try data.drawBytes(32, 32))[0..32].*;
1241 const encoded = modelEncodeSpki(public_key);
1242 try std.testing.expectEqual(encoded, quic.tls.encodeSubjectPublicKeyInfo(public_key));
1243 var buffer: [model_spki_length + 20]u8 = undefined;
1244 buffer[0..model_spki_length].* = encoded;
1245 const input: []const u8 = switch (class) {
1246 .valid => buffer[0..model_spki_length],
1247 .short => buffer[0 .. model_spki_length - 1],
1248 .long => long: {
1249 buffer[model_spki_length] = @intCast(try data.drawInteger(0, 255, 0));
1250 break :long buffer[0 .. model_spki_length + 1];
1251 },
1252 .wrong_prefix => wrong: {
1253 const index_max = model_spki_prefix.len - 1;
1254 const index: usize = @intCast(try data.drawInteger(0, index_max, 0));
1255 buffer[index] ^= @intCast(try data.drawInteger(1, 255, 1));
1256 break :wrong buffer[0..model_spki_length];
1257 },
1258 .random => try data.drawBytes(0, buffer.len),
1259 };
1260 try compareSpkiDecode(input);
1261 if (modelDecodeSpki(input)) |_| {
1262 try compareSpkiDecode(input[0 .. input.len - 1]);
1263 } else |_| {}
1264 }
1265 };
1266
1267 test "property: RFC 8410 section 4 Lean SPKI mirror agrees with production" {
1268 spki_coverage = .{};
1269 rejection_coverage = .{};
1270 try hypothesis.checkNamed(SpkiMirror, "quic-spki-mirror", settings());
1271 try spki_coverage.requireComplete();
1272 try rejection_coverage.require(&spki_rejections);
1273 }