code wiki / (root) / nx_tls13_server_session_derive_hs_test.nx

nx_tls13_server_session_derive_hs_test.nx source

↩ module page · 88 lines · 3085 B

1// nx_tls13_server_session_derive_hs_test.nx -- verify the server's 2// handshake-secret derivation after ServerHello. 3// 4// Closed-form invariants: 5// (a) Wrong state (INIT) -> BAD_STATE 6// (b) After recv_ch + emit_sh + derive_hs_secrets: 7// state advances to EE_SENT 8// (c) handshake_secret is allocated (non-null) + 32 bytes non-zero 9// (d) Calling derive again -> BAD_STATE (already past SH_SENT) 10// 11// expect_exit: 0 12// license_tier: ORIGINAL 13 14import "nx_syscalls.nx" 15import "nx_x25519.nx" 16import "nx_x25519_ephemeral.nx" 17import "nx_tls13.nx" 18import "nx_tls13_hello.nx" 19import "nx_tls13_server_session.nx" 20import "nx_tls13_server_session_recv_ch.nx" 21import "nx_tls13_server_session_emit_sh.nx" 22import "nx_tls13_server_session_derive_hs.nx" 23 24func main() -> i64 { 25 // ===== Build client side + ClientHello ===== 26 let cli_priv: *u8 = sys_mmap(32) 27 let cli_pub: *u8 = sys_mmap(32) 28 let cli_rand: *u8 = sys_mmap(32) 29 var i: i64 = 0 30 while i < 32 { 31 cli_priv[i] = ((i + 17) & 0xff) as u8 32 cli_rand[i] = ((i + 50) & 0xff) as u8 33 i = i + 1 34 } 35 x25519_keypair_public(cli_priv, cli_pub) 36 37 let sni: *u8 = "nishifamily.com" 38 let sni_len: i64 = 15 39 let ch_buf: *u8 = sys_mmap(1024) 40 let ch_n: i64 = tls13_client_hello_emit(cli_rand, sni, sni_len, cli_pub, ch_buf, 1024) 41 if ch_n <= 0 { return 5 } 42 43 // ===== Build server session ===== 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 if (s as i64) == 0 { return 6 } 54 55 // ===== (a) Wrong state (INIT) -> BAD_STATE ===== 56 let r_wrong: i64 = nx_tls13_server_session_derive_hs_secrets(s) 57 if r_wrong != NX_TLS13_SSESSION_BAD_STATE { return 10 } 58 59 // ===== Run recv_ch + emit_sh to get to SH_SENT ===== 60 let r_rc: i64 = nx_tls13_server_session_recv_ch(s, ch_buf, ch_n) 61 if r_rc != NX_TLS13_SSESSION_OK { return 20 } 62 let sh_buf: *u8 = sys_mmap(512) 63 let sh_n: i64 = nx_tls13_server_session_emit_sh(s, sh_buf, 512) 64 if sh_n <= 0 { return 21 } 65 if s.state != NX_TLS13_SSTATE_SH_SENT { return 22 } 66 67 // ===== (b)(c) derive_hs_secrets succeeds ===== 68 let r_d: i64 = nx_tls13_server_session_derive_hs_secrets(s) 69 if r_d != NX_TLS13_SSESSION_OK { return 30 } 70 if s.state != NX_TLS13_SSTATE_EE_SENT { return 31 } 71 if (s.handshake_secret as i64) == 0 { return 32 } 72 73 // 32 bytes of handshake_secret -- at least one byte non-zero 74 // (HKDF output is uniformly random for non-zero ECDHE). 75 var nonzero: i64 = 0 76 var m: i64 = 0 77 while m < 32 { 78 if s.handshake_secret[m] != 0 { nonzero = 1 } 79 m = m + 1 80 } 81 if nonzero != 1 { return 33 } 82 83 // ===== (d) Calling derive again -> BAD_STATE ===== 84 let r_again: i64 = nx_tls13_server_session_derive_hs_secrets(s) 85 if r_again != NX_TLS13_SSESSION_BAD_STATE { return 40 } 86 87 return 0 88}