code wiki / _hdl_build / nx_tls12_frag_read_gate.nx

nx_tls12_frag_read_gate.nx source

↩ module page · 167 lines · 7911 B

1// nx_tls12_frag_read_gate.nx -- DETERMINISTIC partial-read proof for the 2// TLS 1.2 record reader + ServerHello parser. 3// 4// The intermittent "cipher reads 0xC02B instead of 0xC02F" garble was 5// hypothesised to be an INCOMPLETE record read: the 5-byte header says 6// length N but fewer bytes have arrived, so tls12_parse_server_hello runs 7// on a short/shifted buffer. A live host (WSL2/CDN) often delivers the 8// whole flight in one big segment, so the partial-read code path is never 9// exercised live. This gate forces MAXIMAL fragmentation deterministically: 10// a forked child writes a known-good ServerHello record ONE BYTE AT A TIME 11// down a pipe; the parent reads it back through nx_tls13_read_record_from_fd 12// (the exact framer the 1.2 session uses) and parses the cipher. 13// 14// If the record reader truly loops to completion, the reassembled cipher 15// MUST be 0xC02F under any fragmentation. A short-buffer parse would yield 16// a garbled value -> RED. This proves (or refutes) the read mechanism. 17// 18// expect_exit: 0 19// license_tier: ORIGINAL 20 21import "nx_syscalls.nx" 22import "nx_tls12_parse.nx" 23import "nx_tls13_read_record_from_fd.nx" 24 25func fg_w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 26func fg_n(v: i64) -> i64 { 27 var m: i64=v 28 if m<0 { fg_w("-" as *u8); m=0-m } 29 let t: *u8=sys_mmap(24); var k: i64=0 30 if m==0 { t[0]=48 as u8; k=1 } 31 while m>0 { t[k]=(48+(m%10)) as u8; m=m/10; k=k+1 } 32 let o: *u8=sys_mmap(24); var i: i64=0 33 while i<k { o[i]=t[k-1-i]; i=i+1 } 34 sys_write(1,o,k); return 0 35} 36func fg_row(id: *u8, ok: i64, pass: *i64, total: *i64) -> i64 { 37 total[0]=total[0]+1 38 fg_w(" " as *u8); fg_w(id); fg_w(": " as *u8) 39 if ok==1 { fg_w("OK\n" as *u8); pass[0]=pass[0]+1 } else { fg_w("FAIL\n" as *u8) } 40 return 0 41} 42 43// Build a known-good 91-byte TLS 1.2 ServerHello record, cipher = 0xC02F. 44// [0..5) record header 16 03 03 00 56 (handshake, TLS1.2, len 86) 45// [5..9) hs header 02 00 00 52 (ServerHello, body len 82) 46// [9..] SH body: version(2)+random(32)+sid_len(1)=32+sid(32)+ 47// cipher(2)=C0 2F+compression(1)+ext(rest, zero-filled) 48func fg_build_sh(out: *u8, chi: i64, clo: i64) -> i64 { 49 out[0]=0x16 as u8; out[1]=0x03 as u8; out[2]=0x03 as u8; out[3]=0x00 as u8; out[4]=0x56 as u8 50 out[5]=0x02 as u8; out[6]=0x00 as u8; out[7]=0x00 as u8; out[8]=0x52 as u8 51 out[9]=0x03 as u8; out[10]=0x03 as u8 52 var i: i64 = 0 53 while i < 32 { out[11+i]=0xAA as u8; i=i+1 } // server_random 54 out[43]=0x20 as u8 // session_id_len = 32 55 i = 0 56 while i < 32 { out[44+i]=0xBB as u8; i=i+1 } // session_id 57 out[76]=chi as u8; out[77]=clo as u8 // cipher (caller-chosen) 58 out[78]=0x00 as u8 // compression null 59 i = 79 60 while i < 91 { out[i]=0x00 as u8; i=i+1 } // extensions (zero pad to body=82) 61 return 91 62} 63 64// Read one record from rfd, parse the ServerHello cipher. Returns the 65// negotiated cipher (or a negative error). 66func fg_read_and_parse(rfd: i64) -> i64 { 67 let rbuf: *u8 = sys_mmap(20000) 68 let rt: i64 = nx_tls13_read_record_from_fd(rfd, rbuf, 20000) 69 if rt < 9 { return 0 - 1000 } 70 if (rbuf[0] as i64) != 22 { return 0 - 1001 } // must be handshake record 71 let body: *u8 = (rbuf as i64 + 9) as *u8 // skip 5 rec hdr + 4 hs hdr 72 let mlen: i64 = ((rbuf[6] as i64) << 16) | ((rbuf[7] as i64) << 8) | (rbuf[8] as i64) 73 let sr: *u8 = sys_mmap(64) 74 let cip: *i64 = sys_mmap(16) as *i64 75 cip[0] = 0 76 if tls12_parse_server_hello(body, mlen, sr, cip) != 1 { return 0 - 1002 } 77 return cip[0] 78} 79 80// Drive one fragmentation scenario: child writes the `n`-byte record in 81// `chunk`-byte pieces (sleeping `ms` between) down a pipe; parent reads it 82// back and returns the parsed cipher. 83func fg_scenario(rec: *u8, n: i64, chunk: i64, ms: i64) -> i64 { 84 let fds_raw: *u8 = sys_mmap(32) 85 let fds: *i64 = fds_raw as *i64 86 let prc: i64 = sys_pipe2(fds, 0) 87 if prc < 0 { return 0 - 2000 } 88 // Linux pipe2 writes two int32 fds; the x86_64 build packs them into the 89 // first 8 bytes: read_fd in the low 32 bits, write_fd in the high 32. 90 let rfd: i64 = fds[0] & 0xffffffff 91 let wfd: i64 = (fds[0] >> 32) & 0xffffffff 92 let pid: i64 = sys_fork() 93 if pid < 0 { return 0 - 2001 } 94 if pid == 0 { 95 // child: writer 96 sys_close(rfd) 97 var off: i64 = 0 98 while off < n { 99 var w: i64 = chunk 100 if off + w > n { w = n - off } 101 sys_write(wfd, (rec as i64 + off) as *u8, w) 102 off = off + w 103 if ms > 0 { sys_sleep_ms(ms) } 104 } 105 sys_close(wfd) 106 sys_exit(0) 107 } 108 // parent: reader 109 sys_close(wfd) 110 let cip: i64 = fg_read_and_parse(rfd) 111 sys_close(rfd) 112 let status: *i64 = sys_mmap(16) as *i64 113 sys_wait4(pid, status, 0) 114 return cip 115} 116 117func main() -> i64 { 118 let pass: *i64 = sys_mmap(8) as *i64; pass[0]=0 119 let total: *i64 = sys_mmap(8) as *i64; total[0]=0 120 fg_w("=== NX-TLS12-FRAG-READ GATE (deterministic partial-read proof of the record framer) ===\n" as *u8) 121 122 let rec: *u8 = sys_mmap(256) 123 let n: i64 = fg_build_sh(rec, 0xC0, 0x2F) 124 fg_w(" synthetic ServerHello record built: " as *u8); fg_n(n); fg_w(" bytes, cipher=0xC02F\n" as *u8) 125 126 // Baseline: whole record at once -> cipher 0xC02F. 127 let c0: i64 = fg_scenario(rec, n, 91, 0) 128 var ok0: i64 = 0; if c0 == 49199 { ok0 = 1 } 129 fg_w(" [whole-record] parsed cipher=" as *u8); fg_n(c0); fg_w(" (want 49199)\n" as *u8) 130 fg_row("whole-record-at-once -> 0xC02F (49199)" as *u8, ok0, pass, total) 131 132 // 1-byte fragmentation with a 1ms gap -> forces the parent's reads to 133 // return exactly 1 byte each, maximally exercising the read loop. 134 let c1: i64 = fg_scenario(rec, n, 1, 1) 135 var ok1: i64 = 0; if c1 == 49199 { ok1 = 1 } 136 fg_w(" [1-byte frags] parsed cipher=" as *u8); fg_n(c1); fg_w(" (want 49199)\n" as *u8) 137 fg_row("1-byte-fragmentation -> still 0xC02F (loop reassembles)" as *u8, ok1, pass, total) 138 139 // Header-split: 3 bytes, gap, then the rest (splits the 5-byte header 140 // and the length field across reads). 141 let c2: i64 = fg_scenario(rec, n, 3, 1) 142 var ok2: i64 = 0; if c2 == 49199 { ok2 = 1 } 143 fg_w(" [3-byte frags] parsed cipher=" as *u8); fg_n(c2); fg_w(" (want 49199)\n" as *u8) 144 fg_row("3-byte-fragmentation (splits hdr+len) -> 0xC02F" as *u8, ok2, pass, total) 145 146 // Awkward split straddling the cipher offset (chunk 70: first read ends 147 // at byte 70, mid-body, before the cipher at offset 76). 148 let c3: i64 = fg_scenario(rec, n, 70, 1) 149 var ok3: i64 = 0; if c3 == 49199 { ok3 = 1 } 150 fg_w(" [70-byte frags] parsed cipher=" as *u8); fg_n(c3); fg_w(" (want 49199)\n" as *u8) 151 fg_row("70-byte split (straddles cipher offset) -> 0xC02F" as *u8, ok3, pass, total) 152 153 // NEG-CONTROL: a record whose wire cipher is 0xC02B (the garble value) 154 // MUST parse as 0xC02B (49195) -- proving the parser faithfully reports 155 // the BYTES on the wire (the 0xC02F results above are real reads, not a 156 // hardcoded constant). A clean 0xC02F wire therefore always reads 0xC02F. 157 let recb: *u8 = sys_mmap(256) 158 let nb: i64 = fg_build_sh(recb, 0xC0, 0x2B) 159 let cN: i64 = fg_scenario(recb, nb, 1, 1) 160 var okN: i64 = 0; if cN == 49195 { okN = 1 } 161 fg_w(" [neg-control] 0xC02B wire, 1-byte frags, parsed cipher=" as *u8); fg_n(cN); fg_w(" (want 49195)\n" as *u8) 162 fg_row("NEG-CONTROL: 0xC02B wire faithfully read as 49195 (parser not hardcoded)" as *u8, okN, pass, total) 163 164 fg_w("NX-TLS12-FRAG-READ rows=" as *u8); fg_n(total[0]); fg_w(" pass=" as *u8); fg_n(pass[0]) 165 if pass[0]==total[0] { fg_w(" verdict=GREEN\n" as *u8); sys_exit(0); return 0 } 166 fg_w(" verdict=RED\n" as *u8); sys_exit(1); return 1 167}