nx_tls13_server_session_test.nx source
↩ module page · 102 lines · 4211 B
1// nx_tls13_server_session_test.nx -- verify server session skeleton
2// allocates correctly + state machine enum is well-formed.
3//
4// Closed-form invariants:
5// (a) Null inputs return null session
6// (b) Valid inputs return non-null session at INIT state
7// (c) server_random + x25519_priv are copied into owned buffers
8// (not aliased to caller's input)
9// (d) x25519_pub is derived from priv (matches the known-answer
10// relation: pub = X25519(priv, basepoint))
11// (e) All state constants 0..N-1 are valid; out-of-range invalid
12// (f) Session-new yields all secret-buffer pointers initialised
13// to either non-null (active fields) or null (queued fields)
14// per the documented contract
15//
16// expect_exit: 0
17// license_tier: ORIGINAL
18
19import "nx_syscalls.nx"
20import "nx_x25519.nx"
21import "nx_tls13_server_session.nx"
22
23func main() -> i64 {
24 // --- (a) Null inputs ---
25 let s_null1: *Tls13ServerSession = nx_tls13_server_session_new(0 as *u8, 0 as *u8)
26 if (s_null1 as i64) != 0 { return 10 }
27 let some_buf: *u8 = sys_mmap(32)
28 let s_null2: *Tls13ServerSession = nx_tls13_server_session_new(some_buf, 0 as *u8)
29 if (s_null2 as i64) != 0 { return 11 }
30 let s_null3: *Tls13ServerSession = nx_tls13_server_session_new(0 as *u8, some_buf)
31 if (s_null3 as i64) != 0 { return 12 }
32
33 // --- (b) Valid inputs return non-null at INIT ---
34 let rnd: *u8 = sys_mmap(32)
35 let pri: *u8 = sys_mmap(32)
36 // Fill with deterministic-but-distinguishable test bytes.
37 var i: i64 = 0
38 while i < 32 {
39 rnd[i] = ((i + 100) & 0xff) as u8
40 pri[i] = ((i + 200) & 0xff) as u8
41 i = i + 1
42 }
43 let s: *Tls13ServerSession = nx_tls13_server_session_new(rnd, pri)
44 if (s as i64) == 0 { return 20 }
45 if s.state != NX_TLS13_SSTATE_INIT { return 21 }
46
47 // --- (c) server_random is COPIED, not aliased ---
48 if (s.server_random as i64) == (rnd as i64) { return 30 }
49 // ...and the bytes match the original
50 var j: i64 = 0
51 while j < 32 {
52 if s.server_random[j] != rnd[j] { return 31 }
53 j = j + 1
54 }
55 // Mutate the caller's rnd and verify the session's copy is unchanged.
56 let original_byte: i64 = (rnd[0] as i64) & 0xff
57 rnd[0] = 0
58 if (s.server_random[0] as i64) & 0xff != original_byte { return 32 }
59
60 // Same for x25519_priv:
61 if (s.x25519_priv as i64) == (pri as i64) { return 40 }
62
63 // --- (d) Derived x25519_pub != priv (sanity; full KAT in
64 // nx_x25519 smoke). At minimum: pub is non-null and
65 // differs from priv pattern. ---
66 if (s.x25519_pub as i64) == 0 { return 50 }
67 var differs: i64 = 0
68 var k: i64 = 0
69 while k < 32 {
70 if s.x25519_pub[k] != s.x25519_priv[k] { differs = 1 }
71 k = k + 1
72 }
73 if differs != 1 { return 51 }
74
75 // --- (e) State enum range checks ---
76 if nx_tls13_server_state_is_valid(-1) != 0 { return 60 }
77 if nx_tls13_server_state_is_valid(NX_TLS13_SSTATE_N) != 0 { return 61 }
78 if nx_tls13_server_state_is_valid(NX_TLS13_SSTATE_INIT) != 1 { return 62 }
79 if nx_tls13_server_state_is_valid(NX_TLS13_SSTATE_SH_SENT) != 1 { return 63 }
80 if nx_tls13_server_state_is_valid(NX_TLS13_SSTATE_CONNECTED) != 1 { return 64 }
81
82 // --- (f) Initialised pointer contract ---
83 // Active fields (filled at session-new) must be non-null:
84 if (s.server_random as i64) == 0 { return 70 }
85 if (s.x25519_priv as i64) == 0 { return 71 }
86 if (s.x25519_pub as i64) == 0 { return 72 }
87 if (s.transcript as i64) == 0 { return 73 }
88 // Queued fields (populated by later steps) must be null:
89 if (s.client_x25519_pub as i64) != 0 { return 80 }
90 if (s.handshake_secret as i64) != 0 { return 81 }
91 if (s.client_hs_traffic_secret as i64) != 0 { return 82 }
92 if (s.server_hs_traffic_secret as i64) != 0 { return 83 }
93 if (s.master_secret as i64) != 0 { return 84 }
94
95 // Sequence counters must start at 0:
96 if s.client_seq != 0 { return 90 }
97 if s.server_seq != 0 { return 91 }
98 if s.client_app_seq != 0 { return 92 }
99 if s.server_app_seq != 0 { return 93 }
100
101 return 0
102}