nx_tls13_server_session_emit_ee_test.nx source
↩ module page · 92 lines · 3185 B
1// nx_tls13_server_session_emit_ee_test.nx -- verify emit_ee
2// produces a well-formed AEAD-encrypted record.
3//
4// Closed-form invariants:
5// (a) Wrong state (INIT) -> negative verdict
6// (b) After recv_ch + emit_sh + derive_hs + derive_traffic:
7// emit_ee returns positive byte count
8// (c) Output buffer starts with type=0x17 (app_data record)
9// (d) Output is at least header(5) + inner(7) + tag(16) = 28 bytes
10// (e) State advances to CERT_SENT
11// (f) server_seq increments from 0 to 1
12// (g) Calling emit_ee again -> BAD_STATE
13//
14// expect_exit: 0
15// license_tier: ORIGINAL
16
17import "nx_syscalls.nx"
18import "nx_x25519.nx"
19import "nx_x25519_ephemeral.nx"
20import "nx_tls13.nx"
21import "nx_tls13_hello.nx"
22import "nx_tls13_server_session.nx"
23import "nx_tls13_server_session_recv_ch.nx"
24import "nx_tls13_server_session_emit_sh.nx"
25import "nx_tls13_server_session_derive_hs.nx"
26import "nx_tls13_server_session_derive_traffic.nx"
27import "nx_tls13_server_session_emit_ee.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
41 let ch_buf: *u8 = sys_mmap(1024)
42 let ch_n: i64 = tls13_client_hello_emit(cli_rand, "nishifamily.com", 15, cli_pub, ch_buf, 1024)
43 if ch_n <= 0 { return 5 }
44
45 let srv_priv: *u8 = sys_mmap(32)
46 let srv_rand: *u8 = sys_mmap(32)
47 var k: i64 = 0
48 while k < 32 {
49 srv_priv[k] = ((k + 80) & 0xff) as u8
50 srv_rand[k] = ((k + 70) & 0xff) as u8
51 k = k + 1
52 }
53 let s: *Tls13ServerSession = nx_tls13_server_session_new(srv_rand, srv_priv)
54
55 // ===== (a) Wrong state -> BAD_STATE =====
56 let bad_buf: *u8 = sys_mmap(256)
57 let r_wrong: i64 = nx_tls13_server_session_emit_ee(s, bad_buf, 256)
58 let exp_bad: i64 = 0 - NX_TLS13_SSESSION_BAD_STATE
59 if r_wrong != exp_bad { return 10 }
60
61 // ===== Run full chain to EE_SENT =====
62 nx_tls13_server_session_recv_ch(s, ch_buf, ch_n)
63 let sh_buf: *u8 = sys_mmap(512)
64 nx_tls13_server_session_emit_sh(s, sh_buf, 512)
65 nx_tls13_server_session_derive_hs_secrets(s)
66 nx_tls13_server_session_derive_traffic(s)
67 if s.state != NX_TLS13_SSTATE_EE_SENT { return 20 }
68 if s.server_seq != 0 { return 21 }
69
70 // ===== (b) emit_ee succeeds =====
71 let ee_buf: *u8 = sys_mmap(256)
72 let n: i64 = nx_tls13_server_session_emit_ee(s, ee_buf, 256)
73 if n <= 0 { return 30 }
74
75 // ===== (c) Output starts with type=0x17 (app_data) =====
76 if ee_buf[0] != 0x17 { return 40 }
77
78 // ===== (d) Output size >= 28 bytes (5 header + 7 inner + 16 tag) =====
79 if n < 28 { return 50 }
80
81 // ===== (e) State advances to CERT_SENT =====
82 if s.state != NX_TLS13_SSTATE_CERT_SENT { return 60 }
83
84 // ===== (f) server_seq incremented =====
85 if s.server_seq != 1 { return 70 }
86
87 // ===== (g) Calling again -> BAD_STATE =====
88 let r_again: i64 = nx_tls13_server_session_emit_ee(s, ee_buf, 256)
89 if r_again != exp_bad { return 80 }
90
91 return 0
92}