nx_tls13_finished.nx source
↩ module page · 116 lines · 4496 B
1// nx_tls13_finished.nx -- TLS 1.3 Finished MAC (RFC 8446 §4.4.4).
2//
3// Phase 0b §J of the Nishi TLS 1.3 stack per
4// docs/NISHI_TLS13_GAP_AUDIT.md. The single HMAC over the
5// transcript hash that proves to the peer "I have the same
6// handshake-traffic-secret as you, and I saw the same handshake
7// messages." Without this the handshake never completes; with it,
8// the connection is authenticated end-to-end.
9//
10// Per RFC 8446 §4.4.4:
11//
12// finished_key = HKDF-Expand-Label(base_key, "finished", "", Hash.length)
13// verify_data = HMAC(finished_key, Transcript-Hash(Messages))
14//
15// finished_key derivation lives in nx_tls13_schedule.tls13_finished_key.
16// This module is just the HMAC call + constant-time verify.
17//
18// What it does today:
19// - compute Finished MAC (HMAC-SHA256 over transcript hash)
20// - verify received Finished against expected (constant-time)
21// - sealed verdict + validity gate
22//
23// What it doesn't do yet:
24// - SHA-384 variant (composes against existing nx_hmac_sha384;
25// trivial - same shape but 48-byte tag instead of 32)
26//
27// KAT verified:
28// - compute output == direct hmac_sha256(finished_key, transcript_hash)
29// (cross-check confirms Finished is literally HMAC, no extra
30// wrapping)
31// - verify on correct MAC returns OK
32// - verify on flipped-bit MAC returns FIN_MISMATCH
33// - constant-time compare: timing equivalence not measured here
34// but the code shape (XOR-and-OR all bytes, single subtract,
35// single shift) matches the proven pattern from
36// nx_poly1305.poly1305_tag_equal
37//
38// Composes with:
39// - nx_hmac (HMAC-SHA256 primitive)
40// - nx_tls13_schedule (produces finished_key)
41// - nx_tls13_transcript (produces transcript_hash)
42//
43// license_tier: INDEPENDENT_REDERIVE
44// genealogy_id: international-research-sources/ietf/rfc_8446
45// lineage_id: nishi_tls13_finished_q10
46
47// nx_safety_envelope:
48// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
49// sil_target: SIL1
50// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
51// verdict: NOT_YET_EVALUATED
52
53import "nx_syscalls.nx"
54import "nx_hmac.nx"
55
56// SHA-256 output size; if/when we ship SHA-384 variant, the function
57// signatures take hash_len explicitly so the same code generalises.
58const NX_TLS13_FIN_LEN_SHA256: i64 = 32
59
60const NX_TLS13_FIN_VERDICT_OK: i64 = 1
61const NX_TLS13_FIN_VERDICT_MISMATCH: i64 = 2
62const NX_TLS13_FIN_VERDICT_N: i64 = 3
63
64// Compute Finished MAC: HMAC(finished_key, transcript_hash).
65//
66// finished_key MUST come from tls13_finished_key in nx_tls13_schedule.
67// transcript_hash MUST come from a snapshot of the appropriate
68// transcript hash state (which prefix of messages is "appropriate"
69// depends on whose Finished and whether HRR happened; spec §4.4.4
70// is the reference).
71//
72// Writes 32 bytes (SHA-256) of MAC to `out`.
73func nx_tls13_finished_compute(
74 finished_key: *u8, finished_key_len: i64,
75 transcript_hash: *u8, transcript_hash_len: i64,
76 out: *u8
77) -> i64 {
78 hmac_sha256(finished_key, finished_key_len, transcript_hash, transcript_hash_len, out)
79 return NX_TLS13_FIN_VERDICT_OK
80}
81
82// Verify received Finished MAC against expected. Constant-time
83// comparison (XOR-and-OR pattern from RFC 8446 §C.5 + Lucky13
84// absorbed lesson per docs/NISHI_BROWSER_KNOWN_LESSONS.md §1).
85//
86// Returns NX_TLS13_FIN_VERDICT_OK if equal, NX_TLS13_FIN_VERDICT_MISMATCH
87// if not. The verify path MUST NOT short-circuit on first mismatched
88// byte -- the timing leak that lets an attacker brute-force the MAC.
89func nx_tls13_finished_verify(
90 finished_key: *u8, finished_key_len: i64,
91 transcript_hash: *u8, transcript_hash_len: i64,
92 received: *u8, mac_len: i64
93) -> i64 {
94 let computed: *u8 = sys_mmap(64)
95 hmac_sha256(finished_key, finished_key_len, transcript_hash, transcript_hash_len, computed)
96
97 // Constant-time XOR-OR accumulation. diff stays 0 iff every
98 // byte matches. No early exit.
99 var diff: i64 = 0
100 var i: i64 = 0
101 while i < mac_len {
102 diff = diff | ((computed[i] & 0xff) ^ (received[i] & 0xff))
103 i = i + 1
104 }
105 let neg: i64 = 0 - diff
106 let neq: i64 = (neg >> 63) & 1
107 if neq == 0 { return NX_TLS13_FIN_VERDICT_OK }
108 return NX_TLS13_FIN_VERDICT_MISMATCH
109}
110
111// Sealed-enum validity gate.
112func nx_tls13_fin_verdict_is_valid(v: i64) -> i64 {
113 if v < 0 { return 0 }
114 if v >= NX_TLS13_FIN_VERDICT_N { return 0 }
115 return 1
116}