code wiki / _hdl_build / nx_tls13_app_send_fd_gate.nx

nx_tls13_app_send_fd_gate.nx source

↩ module page · 218 lines · 13067 B

1// nx_tls13_app_send_fd_gate.nx -- ENGINEER gate for the chunked TLS app-data 2// sender. Evidence-driven, re-runnable, no network: fabricates a CONNECTED 3// Tls13ServerSession with fixed ChaCha20-Poly1305 keys, sends a 40000-byte 4// payload to a real file fd, then plays the CLIENT side -- walks the wire 5// bytes record by record, asserts every record plaintext <= 16384 (the RFC 6// 8446 ยง5.1 cap the old single-record path violated), decrypts each record 7// with the KAT'd nx_tls13_record_decrypt_v2 under the same keys, reassembles, 8// and byte-compares against the original payload. Also gates the empty- 9// payload path (one empty record) and the partner invariant: exactly 10// ceil(40000/16000) = 3 records, seq increments 0,1,2. 11// license_tier: ORIGINAL 12 13import "nx_tls13_app_send_fd.nx" 14import "nx_gate_verdict.nx" 15static tfg_plan: *i64 16static tfg_count: *i64 17func g_equal(a: *u8,b: *u8) -> i64 { var i: i64=0;while a[i]==b[i] { if a[i]==(0 as u8) { return 1 };i=i+1 };return 0 } 18 19func g_slen(s: *u8) -> i64 { var n: i64=0;while s[n]!=(0 as u8) { n=n+1 };return n } 20func g_puts(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 21func g_pn(v: i64) -> i64 { 22 let b: *u8 = sys_mmap(28) 23 if v == 0 { b[0]=48; sys_write(1,b,1); return 0 } 24 var d: i64=0; var x: i64=v 25 while x>0 { d=d+1; x=x/10 } 26 var i: i64=d-1; x=v 27 while i>=0 { b[i]=(48+(x%10)) as u8; x=x/10; i=i-1 } 28 sys_write(1,b,d); return 0 29} 30const TFG_CASES: *u8="send returns payload_len (40000)\nsession seq advanced to 3 (3 records)\nwire length = 40000 + 3*22\nrecord count = 3 (chunked, not one giant record)\nevery record plaintext <= 16384 (RFC 8446 5.1)\nevery record decrypts OK under app keys\nreassembled length = 40000\nreassembled plaintext byte-identical\nempty payload -> rc 0, one record\nempty payload advanced seq by 1\nfile range completes with closed reader\nfile range decrypts to exact header and selected bytes\nfailed header closes reader without reading body\npremature EOF retains read cause and closes reader\nempty region sends header and closes\ninvalid scratch closes owned reader\nclosed socket peer retains EPIPE and closes reader\n" 31func g_check(name: *u8, cond: i64) -> i64 { 32 gv_plan_check(tfg_plan,name,cond,tfg_count) 33 if cond==1 { g_puts(" PASS " as *u8) } else { g_puts(" FAIL " as *u8) } 34 g_puts(name); g_puts("\n" as *u8); return cond 35} 36 37func main(argc: i64, argv: *i64) -> i64 { 38 if argc!=2 { return 2 } 39 if sys_mkdir(argv[1] as *u8,0x1c0)!=0 { return 2 } 40 if sys_chdir(argv[1] as *u8)!=0 { return 2 } 41 tfg_count=gv_ctr();tfg_plan=gv_plan_new(TFG_CASES) 42 g_puts("nx_tls13_app_send_fd gate\n" as *u8) 43 var pass: i64 = 0 44 var total: i64 = 0 45 46 // ---- fabricate a CONNECTED session with fixed app keys ---- 47 let srand: *u8 = sys_mmap(32) 48 let spriv: *u8 = sys_mmap(32) 49 var i: i64 = 0 50 while i < 32 { srand[i] = (i) as u8; spriv[i] = (64 + i) as u8; i = i + 1 } 51 let s: *Tls13ServerSession = nx_tls13_server_session_new(srand, spriv) 52 if (s as i64) == 0 { g_puts("FAIL session_new\n" as *u8); return 1 } 53 54 let key: *u8 = sys_mmap(32) 55 let iv: *u8 = sys_mmap(12) 56 i = 0 57 while i < 32 { key[i] = (i * 3 + 1) as u8; i = i + 1 } 58 i = 0 59 while i < 12 { iv[i] = (i * 5 + 2) as u8; i = i + 1 } 60 s.state = NX_TLS13_SSTATE_CONNECTED 61 s.server_app_traffic_key = key 62 s.server_app_iv = iv 63 s.server_app_seq = 0 64 65 // ---- 40000-byte deterministic payload ---- 66 let plen: i64 = 40000 67 let payload: *u8 = sys_mmap(plen) 68 i = 0 69 while i < plen { payload[i] = ((i * 7 + 13) & 0xff) as u8; i = i + 1 } 70 71 // ---- send to a real file fd via the chunked path ---- 72 let rec_buf: *u8 = sys_mmap(NX_TLS13_SENDFD_REC_MIN + 512) 73 let path: *u8 = "nx_sendfd_gate.bin" as *u8 74 let fd: i64 = sys_openat_wr(path, 0x1a4) 75 if fd < 0 { g_puts("FAIL open\n" as *u8); return 1 } 76 let sent: i64 = nx_tls13_app_send_fd(s, payload, plen, fd, rec_buf, NX_TLS13_SENDFD_REC_MIN + 512) 77 sys_close(fd) 78 pass = pass + g_check("send returns payload_len (40000)" as *u8, sent == plen); total = total + 1 79 pass = pass + g_check("session seq advanced to 3 (3 records)" as *u8, s.server_app_seq == 3); total = total + 1 80 81 // ---- client side: read wire bytes, walk + decrypt every record ---- 82 let wire_len_box: *i64 = (sys_mmap(8)) as *i64 83 wire_len_box[0] = 0 84 let wire: *u8 = sys_read_file(path, wire_len_box) 85 let wn: i64 = wire_len_box[0] 86 // 3 records, each = plaintext + 5 header + 1 inner-type + 16 tag 87 pass = pass + g_check("wire length = 40000 + 3*22" as *u8, wn == plen + 66); total = total + 1 88 89 let plain_out: *u8 = sys_mmap(17000) 90 let rebuilt: *u8 = sys_mmap(plen + 64) 91 let ct_box: *i64 = (sys_mmap(8)) as *i64 92 let len_box: *i64 = (sys_mmap(8)) as *i64 93 var off: i64 = 0 94 var nrec: i64 = 0 95 var rb: i64 = 0 96 var all_caps_ok: i64 = 1 97 var all_dec_ok: i64 = 1 98 var seq: i64 = 0 99 while off + 5 <= wn { 100 let hdr: *u8 = (wire as i64 + off) as *u8 101 if (hdr[0] as i64) != 0x17 { all_dec_ok = 0; off = wn } 102 else { 103 let body_len: i64 = ((hdr[3] as i64) << 8) | (hdr[4] as i64) 104 if body_len > 16384 + 256 { all_caps_ok = 0 } 105 let ct_len: i64 = body_len - 16 106 // plaintext = ct_len - 1 (inner type byte); RFC cap check 107 if ct_len - 1 > 16384 { all_caps_ok = 0 } 108 let ct: *u8 = (wire as i64 + off + 5) as *u8 109 let tag: *u8 = (wire as i64 + off + 5 + ct_len) as *u8 110 let rv: i64 = nx_tls13_record_decrypt_v2( 111 0x1303, key, iv, seq, hdr, ct, ct_len, tag, 112 plain_out, ct_box, len_box) 113 if rv != NX_TLS13_REC_VERDICT_OK { all_dec_ok = 0 } 114 if ct_box[0] != CT_APPLICATION_DATA { all_dec_ok = 0 } 115 var k: i64 = 0 116 while k < len_box[0] { rebuilt[rb + k] = plain_out[k]; k = k + 1 } 117 rb = rb + len_box[0] 118 seq = seq + 1 119 nrec = nrec + 1 120 off = off + 5 + body_len 121 } 122 } 123 pass = pass + g_check("record count = 3 (chunked, not one giant record)" as *u8, nrec == 3); total = total + 1 124 pass = pass + g_check("every record plaintext <= 16384 (RFC 8446 5.1)" as *u8, all_caps_ok == 1); total = total + 1 125 pass = pass + g_check("every record decrypts OK under app keys" as *u8, all_dec_ok == 1); total = total + 1 126 pass = pass + g_check("reassembled length = 40000" as *u8, rb == plen); total = total + 1 127 128 var same: i64 = 1 129 i = 0 130 while i < plen { if rebuilt[i] != payload[i] { same = 0; i = plen } else { i = i + 1 } } 131 pass = pass + g_check("reassembled plaintext byte-identical" as *u8, same == 1); total = total + 1 132 133 // ---- empty payload still emits exactly one record ---- 134 let fd2: i64 = sys_openat_wr("nx_sendfd_gate0.bin" as *u8, 0x1a4) 135 let seq_before: i64 = s.server_app_seq 136 let sent0: i64 = nx_tls13_app_send_fd(s, payload, 0, fd2, rec_buf, NX_TLS13_SENDFD_REC_MIN + 512) 137 sys_close(fd2) 138 pass = pass + g_check("empty payload -> rc 0, one record" as *u8, sent0 == 0); total = total + 1 139 pass = pass + g_check("empty payload advanced seq by 1" as *u8, s.server_app_seq == seq_before + 1); total = total + 1 140 141 142 // Real file -> bounded reader -> TLS records -> authenticated decrypt. 143 let source_fd: i64=sys_openat_wr("source.bin",0x180) 144 let source_write: *NxFileWriteResult=sys_mmap(__size_of(NxFileWriteResult)) as *NxFileWriteResult 145 if fio_write_sync_fd(source_fd,payload,plen,source_write)!=0 { return 3 } 146 let reader: *NxFileReadRegion=sys_mmap(__size_of(NxFileReadRegion)) as *NxFileReadRegion 147 let receipt: *NxTlsFileSendResult=sys_mmap(__size_of(NxTlsFileSendResult)) as *NxTlsFileSendResult 148 fio_region_init(reader) 149 if fio_region_open("source.bin",reader)!=0 { return 3 } 150 let range_start: i64=NX_TLS13_SENDFD_CHUNK-1 151 let range_length: i64=plen-range_start 152 if fio_region_select(reader,range_start,range_length)!=0 { return 3 } 153 let header: *u8="header\r\n\r\n" 154 let header_n: i64=g_slen(header) 155 let scratch_cap: i64=NX_TLS13_SENDFD_CHUNK 156 let scratch: *u8=sys_mmap(scratch_cap) 157 i=0;while i<header_n { scratch[i]=header[i];i=i+1 } 158 let range_fd: i64=sys_openat_wr("range.tls",0x180) 159 s.server_app_seq=0 160 let streamed: i64=nx_tls13_file_send_fd(s,reader,scratch,header_n,scratch,scratch_cap,range_fd,rec_buf,NX_TLS13_SENDFD_REC_MIN,receipt) 161 sys_close(range_fd) 162 pass=pass+g_check("file range completes with closed reader",((streamed==0)&&(reader.fd<0)&&(receipt.body_bytes==range_length)&&(receipt.header_bytes==header_n)&&(receipt.read_bytes==range_length)) as i64);total=total+1 163 let range_wire: *u8=sys_read_file("range.tls",wire_len_box) 164 var at: i64=0;var rebuilt_n: i64=0;var range_seq: i64=0;var decoded: i64=1 165 while at+5<=wire_len_box[0] { 166 let rh: *u8=range_wire+at 167 let rbody: i64=((rh[3] as i64)<<8)|(rh[4] as i64) 168 if rbody<17 || rbody>wire_len_box[0]-at-5 { decoded=0;break } 169 let rct: i64=rbody-16 170 let rc: i64=nx_tls13_record_decrypt_v2(0x1303,key,iv,range_seq,rh,rh+5,rct,rh+5+rct,plain_out,ct_box,len_box) 171 if rc!=NX_TLS13_REC_VERDICT_OK || ct_box[0]!=CT_APPLICATION_DATA { decoded=0;break } 172 if len_box[0]>plen+64-rebuilt_n { decoded=0;break } 173 i=0;while i<len_box[0] { rebuilt[rebuilt_n+i]=plain_out[i];i=i+1 } 174 rebuilt_n=rebuilt_n+len_box[0];at=at+5+rbody;range_seq=range_seq+1 175 } 176 var exact_range: i64=decoded 177 if receipt.wire_bytes!=wire_len_box[0] || receipt.write_code!=0 { exact_range=0 } 178 if rebuilt_n!=header_n+range_length || at!=wire_len_box[0] { exact_range=0 } 179 i=0;while i<header_n { if rebuilt[i]!=header[i] { exact_range=0 };i=i+1 } 180 i=0;while i<range_length { if rebuilt[header_n+i]!=payload[range_start+i] { exact_range=0 };i=i+1 } 181 pass=pass+g_check("file range decrypts to exact header and selected bytes",exact_range);total=total+1 182 fio_region_open("source.bin",reader) 183 let failed_header: i64=nx_tls13_file_send_fd(s,reader,header,header_n,scratch,scratch_cap,0-1,rec_buf,NX_TLS13_SENDFD_REC_MIN,receipt) 184 pass=pass+g_check("failed header closes reader without reading body",((failed_header<0)&&(reader.fd<0)&&(receipt.read_bytes==0)&&(receipt.body_bytes==0)&&(g_equal(receipt.stage,"header-send")==1)&&(receipt.write_code==(0-9))&&(receipt.wire_bytes==0)) as i64);total=total+1 185 // A connected local socket with its peer closed exercises a real write error. 186 sys_ignore_sigpipe() 187 let listener: i64=sys_unix_listen("closed-peer.sock",1) 188 if listener<0 { return 4 } 189 let peer: i64=sys_unix_connect_fd("closed-peer.sock") 190 if peer<0 { sys_close(listener);return 4 } 191 let accepted: i64=sys_accept(listener) 192 sys_close(peer);sys_close(listener) 193 fio_unlink("closed-peer.sock") 194 if accepted<0 { return 4 } 195 fio_region_open("source.bin",reader) 196 let peer_failure: i64=nx_tls13_file_send_fd(s,reader,header,header_n,scratch,scratch_cap,accepted,rec_buf,NX_TLS13_SENDFD_REC_MIN,receipt) 197 sys_close(accepted) 198 pass=pass+g_check("closed socket peer retains EPIPE and closes reader",((peer_failure<0)&&(receipt.write_code==(0-32))&&(receipt.wire_bytes==0)&&(reader.fd<0)&&(receipt.read_bytes==0)) as i64);total=total+1 199 fio_region_open("source.bin",reader) 200 // Truncate the same inode after measuring it to exercise premature EOF. 201 let truncate_fd: i64=sys_openat_wr("source.bin",0x180);sys_close(truncate_fd) 202 let failure_fd: i64=sys_openat_wr("failed-read.tls",0x180) 203 let failed_read: i64=nx_tls13_file_send_fd(s,reader,header,header_n,scratch,scratch_cap,failure_fd,rec_buf,NX_TLS13_SENDFD_REC_MIN,receipt) 204 sys_close(failure_fd) 205 pass=pass+g_check("premature EOF retains read cause and closes reader",((failed_read==FIO_EIO)&&(reader.fd<0)&&(receipt.header_bytes==header_n)&&(receipt.body_bytes==0)&&(g_equal(receipt.stage,"read-premature-eof")==1)) as i64);total=total+1 206 fio_region_open("source.bin",reader) 207 let empty_fd: i64=sys_openat_wr("empty-range.tls",0x180) 208 let empty_range: i64=nx_tls13_file_send_fd(s,reader,header,header_n,scratch,scratch_cap,empty_fd,rec_buf,NX_TLS13_SENDFD_REC_MIN,receipt) 209 sys_close(empty_fd) 210 pass=pass+g_check("empty region sends header and closes",((empty_range==0)&&(reader.fd<0)&&(receipt.header_bytes==header_n)&&(receipt.body_bytes==0)) as i64);total=total+1 211 fio_region_open("source.bin",reader) 212 let invalid: i64=nx_tls13_file_send_fd(s,reader,header,header_n,scratch,0,0-1,rec_buf,NX_TLS13_SENDFD_REC_MIN,receipt) 213 pass=pass+g_check("invalid scratch closes owned reader",((invalid==FIO_EINVAL)&&(reader.fd<0)&&(receipt.header_bytes==0)) as i64);total=total+1 214 215 g_puts("gate: " as *u8); g_pn(pass); g_puts("/" as *u8); g_pn(total); g_puts("\n" as *u8) 216 gv_plan_finish(tfg_plan,tfg_count) 217 return gv_verdict("TLS-FILE-SEND-GATE",tfg_count,"real files and authenticated record decryption; live network qualification separate") 218}