nx_tls13_server_session_emit_sf_test.nx source
↩ module page · 93 lines · 3197 B
1// nx_tls13_server_session_emit_sf_test.nx -- verify server Finished
2// emission.
3//
4// Closed-form invariants:
5// (a) Wrong state -> negative verdict
6// (b) After full chain through emit_ee + emit_sf: positive byte count
7// (c) Output starts with 0x17 (app_data record)
8// (d) Output >= 5 header + 36 inner + 1 type + 16 tag = 58 bytes
9// (e) State advances to SF_SENT
10// (f) server_seq increments from 1 (after emit_ee) to 2
11// (g) Re-calling -> BAD_STATE
12//
13// expect_exit: 0
14// license_tier: ORIGINAL
15
16import "nx_syscalls.nx"
17import "nx_x25519.nx"
18import "nx_x25519_ephemeral.nx"
19import "nx_tls13.nx"
20import "nx_tls13_hello.nx"
21import "nx_tls13_server_session.nx"
22import "nx_tls13_server_session_recv_ch.nx"
23import "nx_tls13_server_session_emit_sh.nx"
24import "nx_tls13_server_session_derive_hs.nx"
25import "nx_tls13_server_session_derive_traffic.nx"
26import "nx_tls13_server_session_emit_ee.nx"
27import "nx_tls13_server_session_emit_sf.nx"
28
29func main() -> i64 {
30 let cli_priv: *u8 = sys_mmap(32)
31 let cli_pub: *u8 = sys_mmap(32)
32 let cli_rand: *u8 = sys_mmap(32)
33 var i: i64 = 0
34 while i < 32 {
35 cli_priv[i] = ((i + 17) & 0xff) as u8
36 cli_rand[i] = ((i + 50) & 0xff) as u8
37 i = i + 1
38 }
39 x25519_keypair_public(cli_priv, cli_pub)
40 let ch_buf: *u8 = sys_mmap(1024)
41 let ch_n: i64 = tls13_client_hello_emit(cli_rand, "nishifamily.com", 15, cli_pub, ch_buf, 1024)
42 if ch_n <= 0 { return 5 }
43
44 let srv_priv: *u8 = sys_mmap(32)
45 let srv_rand: *u8 = sys_mmap(32)
46 var k: i64 = 0
47 while k < 32 {
48 srv_priv[k] = ((k + 80) & 0xff) as u8
49 srv_rand[k] = ((k + 70) & 0xff) as u8
50 k = k + 1
51 }
52 let s: *Tls13ServerSession = nx_tls13_server_session_new(srv_rand, srv_priv)
53
54 // ===== (a) Wrong state -> BAD_STATE =====
55 let bad_buf: *u8 = sys_mmap(256)
56 let r_wrong: i64 = nx_tls13_server_session_emit_sf(s, bad_buf, 256)
57 let exp_bad: i64 = 0 - NX_TLS13_SSESSION_BAD_STATE
58 if r_wrong != exp_bad { return 10 }
59
60 // ===== Run chain through emit_ee =====
61 nx_tls13_server_session_recv_ch(s, ch_buf, ch_n)
62 let sh_buf: *u8 = sys_mmap(512)
63 nx_tls13_server_session_emit_sh(s, sh_buf, 512)
64 nx_tls13_server_session_derive_hs_secrets(s)
65 nx_tls13_server_session_derive_traffic(s)
66 let ee_buf: *u8 = sys_mmap(256)
67 nx_tls13_server_session_emit_ee(s, ee_buf, 256)
68 if s.state != NX_TLS13_SSTATE_CERT_SENT { return 20 }
69 if s.server_seq != 1 { return 21 }
70
71 // ===== (b) emit_sf succeeds =====
72 let sf_buf: *u8 = sys_mmap(256)
73 let n: i64 = nx_tls13_server_session_emit_sf(s, sf_buf, 256)
74 if n <= 0 { return 30 }
75
76 // ===== (c) Output starts with 0x17 (app_data record) =====
77 if sf_buf[0] != 0x17 { return 40 }
78
79 // ===== (d) Output >= 58 bytes =====
80 if n < 58 { return 50 }
81
82 // ===== (e) State advances to SF_SENT =====
83 if s.state != NX_TLS13_SSTATE_SF_SENT { return 60 }
84
85 // ===== (f) server_seq incremented =====
86 if s.server_seq != 2 { return 70 }
87
88 // ===== (g) Re-calling -> BAD_STATE =====
89 let r_again: i64 = nx_tls13_server_session_emit_sf(s, sf_buf, 256)
90 if r_again != exp_bad { return 80 }
91
92 return 0
93}