nx_tls13_server_session_recv_cf_test.nx source
↩ module page · 188 lines · 6983 B
1// nx_tls13_server_session_recv_cf_test.nx -- close the loopback-class
2// TLS 1.3 server handshake.
3//
4// Smoke construction:
5// 1. Drive server through emit_sf (state == SF_SENT)
6// 2. Snapshot the transcript hash AT THAT POINT (this is what
7// the client would have computed for its Finished)
8// 3. Construct the client Finished record:
9// finished_key_c = HKDF-Expand-Label(c_hs_traffic_secret,
10// "finished", "", 32)
11// verify_data = HMAC-SHA256(finished_key_c, th)
12// plaintext = HT_FINISHED + u24_len + verify_data
13// record = AEAD-encrypt(c_hs_traffic_key, c_hs_iv,
14// client_seq=0, plaintext, CT_HANDSHAKE)
15// 4. Feed the record to recv_cf
16// 5. Assert state == CONNECTED + app keys derived
17//
18// Closed-form invariants:
19// (a) Wrong state -> BAD_STATE
20// (b) Tampered Finished bytes -> PROTOCOL_ERR (HMAC mismatch caught)
21// (c) Honest client Finished -> OK
22// (d) State advances to CONNECTED
23// (e) App traffic secrets + keys + IVs derived (6 non-zero buffers)
24//
25// expect_exit: 0
26// license_tier: ORIGINAL
27
28import "nx_syscalls.nx"
29import "nx_x25519.nx"
30import "nx_x25519_ephemeral.nx"
31import "nx_hmac.nx"
32import "nx_tls13.nx"
33import "nx_tls13_hello.nx"
34import "nx_tls13_kdf.nx"
35import "nx_tls13_record.nx"
36import "nx_tls13_transcript.nx"
37import "nx_tls13_server_session.nx"
38import "nx_tls13_server_session_recv_ch.nx"
39import "nx_tls13_server_session_emit_sh.nx"
40import "nx_tls13_server_session_derive_hs.nx"
41import "nx_tls13_server_session_derive_traffic.nx"
42import "nx_tls13_server_session_emit_ee.nx"
43import "nx_tls13_server_session_emit_sf.nx"
44import "nx_tls13_server_session_recv_cf.nx"
45
46// Construct a TLS 1.3 application_data record that contains an
47// HT_FINISHED handshake message with the given verify_data, encrypted
48// under the supplied key + iv + sequence. Returns total bytes written.
49
50func build_client_finished_record(
51 cli_hs_key: *u8, cli_hs_iv: *u8, cli_seq: i64,
52 verify_data: *u8,
53 out: *u8, out_cap: i64
54) -> i64 {
55 let inner_len: i64 = 36 // HT + u24 + 32 verify
56 let inner: *u8 = sys_mmap(inner_len)
57 inner[0] = HT_FINISHED & 0xff
58 inner[1] = 0
59 inner[2] = 0
60 inner[3] = 32
61 var i: i64 = 0
62 while i < 32 {
63 inner[4 + i] = verify_data[i]
64 i = i + 1
65 }
66 let header: *u8 = sys_mmap(5)
67 let ct: *u8 = sys_mmap(inner_len + 16 + 1)
68 let tag: *u8 = sys_mmap(16)
69 let rv: i64 = nx_tls13_record_encrypt(
70 cli_hs_key, cli_hs_iv, cli_seq,
71 inner, inner_len,
72 CT_HANDSHAKE, 0,
73 header, ct, tag)
74 if rv != NX_TLS13_REC_VERDICT_OK { return -1 }
75
76 let total: i64 = 5 + inner_len + 1 + 16
77 if total > out_cap { return -1 }
78 var w: i64 = 0
79 var hi: i64 = 0
80 while hi < 5 { out[w + hi] = header[hi]; hi = hi + 1 }
81 w = w + 5
82 var ci: i64 = 0
83 while ci < inner_len + 1 { out[w + ci] = ct[ci]; ci = ci + 1 }
84 w = w + inner_len + 1
85 var ti: i64 = 0
86 while ti < 16 { out[w + ti] = tag[ti]; ti = ti + 1 }
87 w = w + 16
88 return w
89}
90
91func main() -> i64 {
92 let cli_priv: *u8 = sys_mmap(32)
93 let cli_pub: *u8 = sys_mmap(32)
94 let cli_rand: *u8 = sys_mmap(32)
95 var i: i64 = 0
96 while i < 32 {
97 cli_priv[i] = ((i + 17) & 0xff) as u8
98 cli_rand[i] = ((i + 50) & 0xff) as u8
99 i = i + 1
100 }
101 x25519_keypair_public(cli_priv, cli_pub)
102 let ch_buf: *u8 = sys_mmap(1024)
103 let ch_n: i64 = tls13_client_hello_emit(cli_rand, "nishifamily.com", 15, cli_pub, ch_buf, 1024)
104 if ch_n <= 0 { return 5 }
105
106 let srv_priv: *u8 = sys_mmap(32)
107 let srv_rand: *u8 = sys_mmap(32)
108 var k: i64 = 0
109 while k < 32 {
110 srv_priv[k] = ((k + 80) & 0xff) as u8
111 srv_rand[k] = ((k + 70) & 0xff) as u8
112 k = k + 1
113 }
114 let s: *Tls13ServerSession = nx_tls13_server_session_new(srv_rand, srv_priv)
115
116 // ===== (a) Wrong state -> BAD_STATE =====
117 let dummy_rec: *u8 = sys_mmap(64)
118 let r_wrong: i64 = nx_tls13_server_session_recv_cf(s, dummy_rec, 64)
119 if r_wrong != NX_TLS13_SSESSION_BAD_STATE { return 10 }
120
121 // ===== Drive server through emit_sf =====
122 nx_tls13_server_session_recv_ch(s, ch_buf, ch_n)
123 let sh_buf: *u8 = sys_mmap(512)
124 nx_tls13_server_session_emit_sh(s, sh_buf, 512)
125 nx_tls13_server_session_derive_hs_secrets(s)
126 nx_tls13_server_session_derive_traffic(s)
127 let ee_buf: *u8 = sys_mmap(256)
128 nx_tls13_server_session_emit_ee(s, ee_buf, 256)
129 let sf_buf: *u8 = sys_mmap(256)
130 nx_tls13_server_session_emit_sf(s, sf_buf, 256)
131 if s.state != NX_TLS13_SSTATE_SF_SENT { return 20 }
132
133 // ===== Compute the verify_data the client would send =====
134 let finished_label: *u8 = "finished"
135 let empty: *u8 = sys_mmap(1)
136 let finished_key_c: *u8 = sys_mmap(32)
137 tls13_hkdf_expand_label(s.client_hs_traffic_secret,
138 finished_label, 8, empty, 0, 32, finished_key_c)
139
140 let th: *u8 = sys_mmap(32)
141 nx_tls13_transcript_snapshot(s.transcript, th)
142
143 let verify_data: *u8 = sys_mmap(32)
144 hmac_sha256(finished_key_c, 32, th, 32, verify_data)
145
146 // ===== (b) Tampered Finished -> PROTOCOL_ERR =====
147 let bad_verify: *u8 = sys_mmap(32)
148 var bi: i64 = 0
149 while bi < 32 { bad_verify[bi] = verify_data[bi]; bi = bi + 1 }
150 bad_verify[0] = (bad_verify[0] as i64 ^ 0xff) as u8 // flip a byte
151
152 let bad_rec_buf: *u8 = sys_mmap(256)
153 let bad_n: i64 = build_client_finished_record(
154 s.client_hs_traffic_key, s.client_hs_iv, s.client_seq,
155 bad_verify, bad_rec_buf, 256)
156 if bad_n <= 0 { return 25 }
157
158 let s_save_state: i64 = s.state
159 let s_save_seq: i64 = s.client_seq
160 let r_bad: i64 = nx_tls13_server_session_recv_cf(s, bad_rec_buf, bad_n)
161 if r_bad != NX_TLS13_SSESSION_PROTOCOL_ERR { return 26 }
162 // State + seq must NOT have advanced on tampered input
163 if s.state != s_save_state { return 27 }
164
165 // ===== (c) Honest Finished -> OK =====
166 let good_rec_buf: *u8 = sys_mmap(256)
167 let good_n: i64 = build_client_finished_record(
168 s.client_hs_traffic_key, s.client_hs_iv, s.client_seq,
169 verify_data, good_rec_buf, 256)
170 if good_n <= 0 { return 30 }
171
172 let r_good: i64 = nx_tls13_server_session_recv_cf(s, good_rec_buf, good_n)
173 if r_good != NX_TLS13_SSESSION_OK { return 31 }
174
175 // ===== (d) State advances to CONNECTED =====
176 if s.state != NX_TLS13_SSTATE_CONNECTED { return 40 }
177
178 // ===== (e) App traffic secrets + keys + IVs all derived =====
179 if (s.master_secret as i64) == 0 { return 50 }
180 if (s.client_app_traffic_secret as i64) == 0 { return 51 }
181 if (s.server_app_traffic_secret as i64) == 0 { return 52 }
182 if (s.client_app_traffic_key as i64) == 0 { return 53 }
183 if (s.server_app_traffic_key as i64) == 0 { return 54 }
184 if (s.client_app_iv as i64) == 0 { return 55 }
185 if (s.server_app_iv as i64) == 0 { return 56 }
186
187 return 0
188}