nx_tls13_transcript_test.nx source
↩ module page · 152 lines · 5093 B
1// nx_tls13_transcript_test.nx -- KAT + internal consistency for the
2// TLS 1.3 transcript hash.
3//
4// Verification:
5//
6// A. Empty transcript snapshot == SHA-256("") well-known constant
7// (e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855).
8//
9// B. 3-message transcript snapshot == sha256_digest of the
10// concatenated bytes (round-trip vs the underlying primitive).
11//
12// C. Snapshot is non-destructive: snapshot, update with more data,
13// snapshot again -- the two snapshots differ.
14//
15// D. HRR replace produces a transcript whose snapshot equals
16// SHA-256(synthetic_record), where synthetic_record =
17// 0xfe || 0x00 0x00 0x20 || SHA-256(CH1).
18//
19// expect_exit: 0
20// license_tier: ORIGINAL
21
22import "nx_syscalls.nx"
23import "nx_sha256.nx"
24import "nx_tls13_transcript.nx"
25
26func main() -> i64 {
27 // ---- Test A: empty transcript ----
28 let state_a: *u8 = nx_tls13_transcript_new()
29 let h_a: *u8 = sys_mmap(64)
30 nx_tls13_transcript_snapshot(state_a, h_a)
31 // Expected: e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855
32 if (h_a[0] & 0xff) != 0xe3 { return 1 }
33 if (h_a[1] & 0xff) != 0xb0 { return 2 }
34 if (h_a[7] & 0xff) != 0x14 { return 3 }
35 if (h_a[15] & 0xff) != 0x24 { return 4 }
36 if (h_a[23] & 0xff) != 0x4c { return 5 }
37 if (h_a[31] & 0xff) != 0x55 { return 6 }
38
39 // ---- Test B: 3-message transcript vs sha256_digest of concatenation ----
40 let m1: *u8 = sys_mmap(32)
41 m1[0]=0x16; m1[1]=0x03; m1[2]=0x03; m1[3]=0x00; m1[4]=0x04 // 5-byte fake msg 1
42 let m2: *u8 = sys_mmap(32)
43 var i: i64 = 0
44 while i < 17 {
45 m2[i] = 0x40 + i // 17-byte fake msg 2
46 i = i + 1
47 }
48 let m3: *u8 = sys_mmap(64)
49 i = 0
50 while i < 41 {
51 m3[i] = (i * 7 + 3) & 0xff // 41-byte fake msg 3
52 i = i + 1
53 }
54
55 let state_b: *u8 = nx_tls13_transcript_new()
56 nx_tls13_transcript_update(state_b, m1, 5)
57 nx_tls13_transcript_update(state_b, m2, 17)
58 nx_tls13_transcript_update(state_b, m3, 41)
59 let h_b: *u8 = sys_mmap(64)
60 nx_tls13_transcript_snapshot(state_b, h_b)
61
62 // Compute reference: SHA-256(m1 || m2 || m3) directly via one-shot
63 let concat: *u8 = sys_mmap(128)
64 var c: i64 = 0
65 var k: i64 = 0
66 while k < 5 { concat[c + k] = m1[k]; k = k + 1 }
67 c = c + 5
68 k = 0
69 while k < 17 { concat[c + k] = m2[k]; k = k + 1 }
70 c = c + 17
71 k = 0
72 while k < 41 { concat[c + k] = m3[k]; k = k + 1 }
73 c = c + 41
74 let h_ref: *u8 = sys_mmap(64)
75 sha256_digest(concat, c, h_ref)
76
77 var bi: i64 = 0
78 while bi < 32 {
79 if (h_b[bi] & 0xff) != (h_ref[bi] & 0xff) { return 10 + bi }
80 bi = bi + 1
81 }
82
83 // ---- Test C: snapshot non-destructive ----
84 let state_c: *u8 = nx_tls13_transcript_new()
85 nx_tls13_transcript_update(state_c, m1, 5)
86 let h_c1: *u8 = sys_mmap(64)
87 nx_tls13_transcript_snapshot(state_c, h_c1)
88 // State should be unmodified; feed m2 and re-snapshot.
89 nx_tls13_transcript_update(state_c, m2, 17)
90 let h_c2: *u8 = sys_mmap(64)
91 nx_tls13_transcript_snapshot(state_c, h_c2)
92 // The two snapshots MUST differ (different inputs hashed).
93 var diff_c: i64 = 0
94 bi = 0
95 while bi < 32 {
96 if (h_c1[bi] & 0xff) != (h_c2[bi] & 0xff) { diff_c = diff_c + 1 }
97 bi = bi + 1
98 }
99 if diff_c < 20 { return 50 } // expect most bytes to differ
100
101 // Also verify state_c's final snapshot matches sha256(m1 || m2)
102 let cc: *u8 = sys_mmap(64)
103 k = 0
104 while k < 5 { cc[k] = m1[k]; k = k + 1 }
105 k = 0
106 while k < 17 { cc[5 + k] = m2[k]; k = k + 1 }
107 let h_cref: *u8 = sys_mmap(64)
108 sha256_digest(cc, 22, h_cref)
109 bi = 0
110 while bi < 32 {
111 if (h_c2[bi] & 0xff) != (h_cref[bi] & 0xff) { return 60 + bi }
112 bi = bi + 1
113 }
114
115 // ---- Test D: HRR replace ----
116 // Feed CH1 (use m1 as a stand-in), HRR-replace, snapshot.
117 // Expected snapshot = SHA-256(0xfe || 0x00 0x00 0x20 || SHA-256(m1))
118 let state_d: *u8 = nx_tls13_transcript_new()
119 nx_tls13_transcript_update(state_d, m1, 5)
120 nx_tls13_transcript_replace_with_hrr(state_d)
121 let h_d: *u8 = sys_mmap(64)
122 nx_tls13_transcript_snapshot(state_d, h_d)
123
124 // Reference: compute Hash(m1) then synthetic record then its hash.
125 let h_m1: *u8 = sys_mmap(64)
126 sha256_digest(m1, 5, h_m1)
127 let synth: *u8 = sys_mmap(64)
128 synth[0] = 0xfe
129 synth[1] = 0
130 synth[2] = 0
131 synth[3] = 32
132 bi = 0
133 while bi < 32 {
134 synth[4 + bi] = h_m1[bi]
135 bi = bi + 1
136 }
137 let h_d_ref: *u8 = sys_mmap(64)
138 sha256_digest(synth, 36, h_d_ref)
139
140 bi = 0
141 while bi < 32 {
142 if (h_d[bi] & 0xff) != (h_d_ref[bi] & 0xff) { return 100 + bi }
143 bi = bi + 1
144 }
145
146 // ---- Verdict gate ----
147 if nx_tls13_tx_verdict_is_valid(NX_TLS13_TX_VERDICT_OK) != 1 { return 200 }
148 if nx_tls13_tx_verdict_is_valid(NX_TLS13_TX_VERDICT_N) != 0 { return 201 }
149 if nx_tls13_tx_verdict_is_valid(0 - 1) != 0 { return 202 }
150
151 return 0
152}