nx_tls13_server_session_emit_cv_test.nx source
↩ module page · 113 lines · 4146 B
1// nx_tls13_server_session_emit_cv_test.nx -- verify CertificateVerify
2// emission + ECDSA-P256 signing pipeline.
3//
4// Closed-form invariants:
5// (a) Wrong state -> negative
6// (b) Null priv key -> negative
7// (c) After chain through emit_ee: emit_cv succeeds
8// (d) Output starts with 0x17 (app_data record)
9// (e) Output size sensible (header + CV message + tag)
10// (f) State advances CV_SENT
11// (g) server_seq increments (1 from emit_ee -> 2 after emit_cv)
12// (h) emit_sf still works AFTER emit_cv (state CV_SENT accepted)
13// (i) emit_cv called twice -> BAD_STATE
14//
15// expect_exit: 0
16// license_tier: ORIGINAL
17
18import "nx_syscalls.nx"
19import "nx_x25519.nx"
20import "nx_x25519_ephemeral.nx"
21import "nx_tls13.nx"
22import "nx_tls13_hello.nx"
23import "nx_tls13_server_session.nx"
24import "nx_tls13_server_session_recv_ch.nx"
25import "nx_tls13_server_session_emit_sh.nx"
26import "nx_tls13_server_session_derive_hs.nx"
27import "nx_tls13_server_session_derive_traffic.nx"
28import "nx_tls13_server_session_emit_ee.nx"
29import "nx_tls13_server_session_emit_cv.nx"
30import "nx_tls13_server_session_emit_sf.nx"
31
32func main() -> i64 {
33 let cli_priv: *u8 = sys_mmap(32)
34 let cli_pub: *u8 = sys_mmap(32)
35 let cli_rand: *u8 = sys_mmap(32)
36 var i: i64 = 0
37 while i < 32 {
38 cli_priv[i] = ((i + 17) & 0xff) as u8
39 cli_rand[i] = ((i + 50) & 0xff) as u8
40 i = i + 1
41 }
42 x25519_keypair_public(cli_priv, cli_pub)
43 let ch_buf: *u8 = sys_mmap(1024)
44 let ch_n: i64 = tls13_client_hello_emit(cli_rand, "nishifamily.com", 15, cli_pub, ch_buf, 1024)
45 if ch_n <= 0 { return 5 }
46
47 let srv_priv: *u8 = sys_mmap(32)
48 let srv_rand: *u8 = sys_mmap(32)
49 let srv_ecdsa: *u8 = sys_mmap(32)
50 var k: i64 = 0
51 while k < 32 {
52 srv_priv[k] = ((k + 80) & 0xff) as u8
53 srv_rand[k] = ((k + 70) & 0xff) as u8
54 srv_ecdsa[k] = ((k + 100) & 0xff) as u8 // deterministic test priv
55 k = k + 1
56 }
57 let s: *Tls13ServerSession = nx_tls13_server_session_new(srv_rand, srv_priv)
58
59 // ===== (a) Wrong state =====
60 let bad_buf: *u8 = sys_mmap(512)
61 let r_wrong: i64 = nx_tls13_server_session_emit_cv(s, srv_ecdsa, bad_buf, 512)
62 let exp_bad: i64 = 0 - NX_TLS13_SSESSION_BAD_STATE
63 if r_wrong != exp_bad { return 10 }
64
65 // ===== Drive through emit_ee =====
66 nx_tls13_server_session_recv_ch(s, ch_buf, ch_n)
67 let sh_buf: *u8 = sys_mmap(512)
68 nx_tls13_server_session_emit_sh(s, sh_buf, 512)
69 nx_tls13_server_session_derive_hs_secrets(s)
70 nx_tls13_server_session_derive_traffic(s)
71 let ee_buf: *u8 = sys_mmap(256)
72 nx_tls13_server_session_emit_ee(s, ee_buf, 256)
73 if s.state != NX_TLS13_SSTATE_CERT_SENT { return 20 }
74 if s.server_seq != 1 { return 21 }
75
76 // ===== (b) Null priv key =====
77 let r_null: i64 = nx_tls13_server_session_emit_cv(s, 0 as *u8, bad_buf, 512)
78 if r_null != 0 - NX_TLS13_SSESSION_INTERNAL { return 25 }
79 // State must not have advanced
80 if s.state != NX_TLS13_SSTATE_CERT_SENT { return 26 }
81
82 // ===== (c) emit_cv succeeds =====
83 let cv_buf: *u8 = sys_mmap(512)
84 let n_cv: i64 = nx_tls13_server_session_emit_cv(s, srv_ecdsa, cv_buf, 512)
85 if n_cv <= 0 { return 30 }
86
87 // ===== (d) Output starts with 0x17 =====
88 if cv_buf[0] != 0x17 { return 40 }
89
90 // ===== (e) Size sensible: header(5) + inner(~80) + tag(16) >= 100 =====
91 if n_cv < 90 { return 50 }
92 if n_cv > 200 { return 51 }
93
94 // ===== (f) State advances =====
95 if s.state != NX_TLS13_SSTATE_CV_SENT { return 60 }
96
97 // ===== (g) server_seq increments =====
98 if s.server_seq != 2 { return 70 }
99
100 // ===== (h) emit_sf accepts CV_SENT =====
101 let sf_buf: *u8 = sys_mmap(256)
102 let n_sf: i64 = nx_tls13_server_session_emit_sf(s, sf_buf, 256)
103 if n_sf <= 0 { return 80 }
104 if s.state != NX_TLS13_SSTATE_SF_SENT { return 81 }
105 if s.server_seq != 3 { return 82 }
106
107 // ===== (i) emit_cv re-called -> BAD_STATE =====
108 // (s.state is now SF_SENT, not CERT_SENT)
109 let r_again: i64 = nx_tls13_server_session_emit_cv(s, srv_ecdsa, cv_buf, 512)
110 if r_again != exp_bad { return 90 }
111
112 return 0
113}