nx_tls13_server_session_derive_traffic_test.nx source
↩ module page · 109 lines · 3741 B
1// nx_tls13_server_session_derive_traffic_test.nx -- verify traffic
2// secrets + AEAD keys + IVs derived correctly after handshake_secret.
3//
4// Closed-form invariants:
5// (a) Wrong state (INIT) -> BAD_STATE
6// (b) After recv_ch + emit_sh + derive_hs_secrets + derive_traffic:
7// all 6 derived buffers allocated + non-zero
8// (c) c_hs_traffic_secret != s_hs_traffic_secret (distinct directions)
9// (d) c_hs_traffic_key != s_hs_traffic_key (distinct directions)
10// (e) c_hs_iv != s_hs_iv
11//
12// expect_exit: 0
13// license_tier: ORIGINAL
14
15import "nx_syscalls.nx"
16import "nx_x25519.nx"
17import "nx_x25519_ephemeral.nx"
18import "nx_tls13.nx"
19import "nx_tls13_hello.nx"
20import "nx_tls13_server_session.nx"
21import "nx_tls13_server_session_recv_ch.nx"
22import "nx_tls13_server_session_emit_sh.nx"
23import "nx_tls13_server_session_derive_hs.nx"
24import "nx_tls13_server_session_derive_traffic.nx"
25
26func buf_differs(a: *u8, b: *u8, n: i64) -> i64 {
27 var i: i64 = 0
28 while i < n {
29 if a[i] != b[i] { return 1 }
30 i = i + 1
31 }
32 return 0
33}
34
35func buf_nonzero(a: *u8, n: i64) -> i64 {
36 var i: i64 = 0
37 while i < n {
38 if a[i] != 0 { return 1 }
39 i = i + 1
40 }
41 return 0
42}
43
44func main() -> i64 {
45 let cli_priv: *u8 = sys_mmap(32)
46 let cli_pub: *u8 = sys_mmap(32)
47 let cli_rand: *u8 = sys_mmap(32)
48 var i: i64 = 0
49 while i < 32 {
50 cli_priv[i] = ((i + 17) & 0xff) as u8
51 cli_rand[i] = ((i + 50) & 0xff) as u8
52 i = i + 1
53 }
54 x25519_keypair_public(cli_priv, cli_pub)
55
56 let sni: *u8 = "nishifamily.com"
57 let ch_buf: *u8 = sys_mmap(1024)
58 let ch_n: i64 = tls13_client_hello_emit(cli_rand, sni, 15, cli_pub, ch_buf, 1024)
59 if ch_n <= 0 { return 5 }
60
61 let srv_priv: *u8 = sys_mmap(32)
62 let srv_rand: *u8 = sys_mmap(32)
63 var k: i64 = 0
64 while k < 32 {
65 srv_priv[k] = ((k + 80) & 0xff) as u8
66 srv_rand[k] = ((k + 70) & 0xff) as u8
67 k = k + 1
68 }
69 let s: *Tls13ServerSession = nx_tls13_server_session_new(srv_rand, srv_priv)
70
71 // ===== (a) Wrong state -> BAD_STATE =====
72 let r_wrong: i64 = nx_tls13_server_session_derive_traffic(s)
73 if r_wrong != NX_TLS13_SSESSION_BAD_STATE { return 10 }
74
75 // ===== Run the full chain through derive_hs_secrets =====
76 nx_tls13_server_session_recv_ch(s, ch_buf, ch_n)
77 let sh_buf: *u8 = sys_mmap(512)
78 nx_tls13_server_session_emit_sh(s, sh_buf, 512)
79 nx_tls13_server_session_derive_hs_secrets(s)
80 if s.state != NX_TLS13_SSTATE_EE_SENT { return 20 }
81
82 // ===== (b) Derive traffic + verify all 6 buffers non-zero =====
83 let r_d: i64 = nx_tls13_server_session_derive_traffic(s)
84 if r_d != NX_TLS13_SSESSION_OK { return 30 }
85 if (s.client_hs_traffic_secret as i64) == 0 { return 31 }
86 if (s.server_hs_traffic_secret as i64) == 0 { return 32 }
87 if (s.client_hs_traffic_key as i64) == 0 { return 33 }
88 if (s.client_hs_iv as i64) == 0 { return 34 }
89 if (s.server_hs_traffic_key as i64) == 0 { return 35 }
90 if (s.server_hs_iv as i64) == 0 { return 36 }
91
92 if buf_nonzero(s.client_hs_traffic_secret, 32) != 1 { return 40 }
93 if buf_nonzero(s.server_hs_traffic_secret, 32) != 1 { return 41 }
94 if buf_nonzero(s.client_hs_traffic_key, 32) != 1 { return 42 }
95 if buf_nonzero(s.server_hs_traffic_key, 32) != 1 { return 43 }
96
97 // ===== (c)(d)(e) Direction-distinct material =====
98 if buf_differs(s.client_hs_traffic_secret, s.server_hs_traffic_secret, 32) != 1 {
99 return 50
100 }
101 if buf_differs(s.client_hs_traffic_key, s.server_hs_traffic_key, 32) != 1 {
102 return 51
103 }
104 if buf_differs(s.client_hs_iv, s.server_hs_iv, 12) != 1 {
105 return 52
106 }
107
108 return 0
109}