nx_edge_serve_static_test.nx source
↩ module page · 172 lines · 6868 B
1// nx_edge_serve_static_test.nx -- prove the operator-facing
2// composition primitive turns a CONNECTED session + static HTML
3// into a sendable TLS app-data record carrying HTTP/1.1 200 OK.
4//
5// Closed-form invariants:
6// (a) Wrong state -> negative
7// (b) Full handshake driven to CONNECTED + serve_static returns
8// positive byte count
9// (c) Output starts with 0x17 (app_data record header)
10// (d) Output decrypts (via app_recv on a sibling session sharing
11// keys) back to a valid HTTP/1.1 200 OK with the HTML body
12// (e) Body present in plaintext (the actual HTML content)
13// (f) Content-Length header reflects the body length
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_hmac.nx"
22import "nx_tls13.nx"
23import "nx_tls13_hello.nx"
24import "nx_tls13_kdf.nx"
25import "nx_tls13_record.nx"
26import "nx_tls13_transcript.nx"
27import "nx_tls13_server_session.nx"
28import "nx_tls13_server_session_recv_ch.nx"
29import "nx_tls13_server_session_emit_sh.nx"
30import "nx_tls13_server_session_derive_hs.nx"
31import "nx_tls13_server_session_derive_traffic.nx"
32import "nx_tls13_server_session_emit_ee.nx"
33import "nx_tls13_server_session_emit_sf.nx"
34import "nx_tls13_server_session_recv_cf.nx"
35import "nx_tls13_server_session_app_data.nx"
36import "nx_edge_serve_static.nx"
37
38func find_needle(buf: *u8, buf_len: i64, needle: *u8) -> i64 {
39 var nlen: i64 = 0
40 while needle[nlen] != 0 { nlen = nlen + 1 }
41 if buf_len < nlen { return -1 }
42 var i: i64 = 0
43 let last: i64 = buf_len - nlen
44 while i <= last {
45 var j: i64 = 0
46 var matched: i64 = 1
47 while j < nlen {
48 if buf[i + j] != needle[j] { matched = 0; j = nlen }
49 j = j + 1
50 }
51 if matched == 1 { return i }
52 i = i + 1
53 }
54 return -1
55}
56
57func main() -> i64 {
58 let cli_priv: *u8 = sys_mmap(32)
59 let cli_pub: *u8 = sys_mmap(32)
60 let cli_rand: *u8 = sys_mmap(32)
61 var i: i64 = 0
62 while i < 32 {
63 cli_priv[i] = ((i + 17) & 0xff) as u8
64 cli_rand[i] = ((i + 50) & 0xff) as u8
65 i = i + 1
66 }
67 x25519_keypair_public(cli_priv, cli_pub)
68 let ch_buf: *u8 = sys_mmap(1024)
69 let ch_n: i64 = tls13_client_hello_emit(cli_rand, "nishifamily.com", 15, cli_pub, ch_buf, 1024)
70 if ch_n <= 0 { return 5 }
71
72 let srv_priv: *u8 = sys_mmap(32)
73 let srv_rand: *u8 = sys_mmap(32)
74 var k: i64 = 0
75 while k < 32 {
76 srv_priv[k] = ((k + 80) & 0xff) as u8
77 srv_rand[k] = ((k + 70) & 0xff) as u8
78 k = k + 1
79 }
80 let s: *Tls13ServerSession = nx_tls13_server_session_new(srv_rand, srv_priv)
81
82 // ===== (a) Wrong state =====
83 let html: *u8 = "<!doctype html><title>Nishi Family</title><h1>nishifamily.com</h1><p>Bits-up substrate live.</p>"
84 var html_len: i64 = 0
85 while html[html_len] != 0 { html_len = html_len + 1 }
86 let bad_buf: *u8 = sys_mmap(2048)
87 let r_wrong: i64 = nx_edge_serve_static_response(s, html, html_len, bad_buf, 2048)
88 let exp_bad: i64 = 0 - NX_TLS13_SSESSION_BAD_STATE
89 if r_wrong != exp_bad { return 10 }
90
91 // ===== Drive handshake to CONNECTED =====
92 nx_tls13_server_session_recv_ch(s, ch_buf, ch_n)
93 let sh_buf: *u8 = sys_mmap(512)
94 nx_tls13_server_session_emit_sh(s, sh_buf, 512)
95 nx_tls13_server_session_derive_hs_secrets(s)
96 nx_tls13_server_session_derive_traffic(s)
97 let ee_buf: *u8 = sys_mmap(256)
98 nx_tls13_server_session_emit_ee(s, ee_buf, 256)
99 let sf_buf: *u8 = sys_mmap(256)
100 nx_tls13_server_session_emit_sf(s, sf_buf, 256)
101
102 // Client Finished construction (same pattern as full-handshake smoke)
103 let finished_label: *u8 = "finished"
104 let empty: *u8 = sys_mmap(1)
105 let finished_key_c: *u8 = sys_mmap(32)
106 tls13_hkdf_expand_label(s.client_hs_traffic_secret, finished_label, 8,
107 empty, 0, 32, finished_key_c)
108 let th: *u8 = sys_mmap(32)
109 nx_tls13_transcript_snapshot(s.transcript, th)
110 let verify_data: *u8 = sys_mmap(32)
111 hmac_sha256(finished_key_c, 32, th, 32, verify_data)
112 let inner: *u8 = sys_mmap(36)
113 inner[0] = HT_FINISHED & 0xff
114 inner[1] = 0; inner[2] = 0; inner[3] = 32
115 var vi: i64 = 0
116 while vi < 32 { inner[4 + vi] = verify_data[vi]; vi = vi + 1 }
117 let cf_hdr: *u8 = sys_mmap(5)
118 let cf_ct: *u8 = sys_mmap(64)
119 let cf_tag: *u8 = sys_mmap(16)
120 nx_tls13_record_encrypt(s.client_hs_traffic_key, s.client_hs_iv, s.client_seq,
121 inner, 36, CT_HANDSHAKE, 0, cf_hdr, cf_ct, cf_tag)
122 let cf_rec: *u8 = sys_mmap(64)
123 var ci2: i64 = 0
124 while ci2 < 5 { cf_rec[ci2] = cf_hdr[ci2]; ci2 = ci2 + 1 }
125 var ci3: i64 = 0
126 while ci3 < 37 { cf_rec[5 + ci3] = cf_ct[ci3]; ci3 = ci3 + 1 }
127 var ci4: i64 = 0
128 while ci4 < 16 { cf_rec[42 + ci4] = cf_tag[ci4]; ci4 = ci4 + 1 }
129
130 nx_tls13_server_session_recv_cf(s, cf_rec, 58)
131 if s.state != NX_TLS13_SSTATE_CONNECTED { return 20 }
132
133 // ===== (b)(c) serve_static_response =====
134 let send_buf: *u8 = sys_mmap(2048)
135 let n_send: i64 = nx_edge_serve_static_response(s, html, html_len, send_buf, 2048)
136 if n_send <= 0 { return 30 }
137 if send_buf[0] != 0x17 { return 31 }
138
139 // ===== (d)(e)(f) Decrypt round-trip with SERVER's app keys =====
140 //
141 // The server's app_send encrypts under server_app_* keys + seq.
142 // session.app_recv uses CLIENT app keys (opposite direction).
143 // For the loopback test, decrypt manually using the same keys
144 // the server used to encrypt -- this is what a REAL CLIENT
145 // would have access to after the handshake.
146 let header_recv: *u8 = send_buf
147 let body_len_recv: i64 = ((header_recv[3] as i64) << 8) | (header_recv[4] as i64)
148 let ct_len_recv: i64 = body_len_recv - 16
149 let ct_recv: *u8 = (((send_buf as i64) + 5)) as *u8
150 let tag_recv: *u8 = (((send_buf as i64) + 5 + ct_len_recv)) as *u8
151
152 let decrypted: *u8 = sys_mmap(2048)
153 let real_ct_box: *i64 = sys_mmap(8) as *i64
154 let real_len_box: *i64 = sys_mmap(8) as *i64
155 // The encrypt used server_app_seq = 0 (just incremented to 1 by app_send).
156 // To decrypt, use seq = 0 (the value at-time-of-encrypt).
157 let dec_v: i64 = nx_tls13_record_decrypt(
158 s.server_app_traffic_key, s.server_app_iv, 0,
159 header_recv, ct_recv, ct_len_recv, tag_recv,
160 decrypted, real_ct_box, real_len_box)
161 if dec_v != NX_TLS13_REC_VERDICT_OK { return 40 }
162 let n_dec: i64 = *real_len_box
163 if n_dec <= 0 { return 41 }
164
165 // The decrypted plaintext should be a full HTTP/1.1 response.
166 if find_needle(decrypted, n_dec, "HTTP/1.1 200 OK") < 0 { return 50 }
167 if find_needle(decrypted, n_dec, "Content-Length: ") < 0 { return 51 }
168 if find_needle(decrypted, n_dec, "nishifamily.com") < 0 { return 52 }
169 if find_needle(decrypted, n_dec, "Bits-up substrate") < 0 { return 53 }
170
171 return 0
172}