nx_tls13_record_test.nx source

1// nx_tls13_record_test.nx -- internal-consistency KAT for the 2// TLS 1.3 record-layer protection wrapper. 3// 4// We don't pin to RFC 8448 §3 wire bytes here because those depend 5// on the full key schedule + traffic-secret derivation tied to 6// specific handshake messages. Instead we verify: 7// 8// A. Round-trip: encrypt then decrypt restores plaintext + type 9// B. Nonce-with-seq: encrypt(seq=0) != encrypt(seq=1) given 10// same (key, iv, content) -- confirms IV XOR seq actually 11// varies the keystream 12// C. Tampered tag rejected (TAG_MISMATCH) 13// D. Tampered header (wrong length in AAD) rejected 14// E. Padding: encrypt with padding_len > 0, decrypt strips it 15// F. All-zeros inner (no type byte) rejected (EMPTY_INNER) 16// G. Nonce construction byte-exact for known (iv, seq) pair 17// 18// expect_exit: 0 19// license_tier: ORIGINAL 20 21import "nx_syscalls.nx" 22import "nx_chacha20_poly1305.nx" 23import "nx_tls13_record.nx" 24 25func main() -> i64 { 26 // ---- Test G: nonce construction byte-exact ---- 27 // iv = 01 02 03 04 05 06 07 08 09 0a 0b 0c 28 // seq = 0x0000000000000001 29 // nonce = iv XOR (4 zero bytes || 8-byte BE seq) 30 // = 01 02 03 04 05 06 07 08 09 0a 0b 0d (last byte = 0c ^ 01) 31 let iv: *u8 = sys_mmap(16) 32 var ii: i64 = 0 33 while ii < 12 { 34 iv[ii] = ii + 1 35 ii = ii + 1 36 } 37 let nonce: *u8 = sys_mmap(16) 38 tls13_record_build_nonce(iv, 1, nonce) 39 if (nonce[0] & 0xff) != 0x01 { return 1 } 40 if (nonce[3] & 0xff) != 0x04 { return 2 } 41 if (nonce[4] & 0xff) != 0x05 { return 3 } // iv[4] XOR 0 42 if (nonce[10] & 0xff) != 0x0b { return 4 } // iv[10] XOR 0 43 if (nonce[11] & 0xff) != 0x0d { return 5 } // iv[11] (0x0c) XOR 0x01 44 45 // Seq = 0x0102030405060708 -> last 8 bytes of nonce should XOR 46 // those big-endian bytes into iv[4..12]. 47 tls13_record_build_nonce(iv, 0x0102030405060708, nonce) 48 if (nonce[4] & 0xff) != (0x05 ^ 0x01) { return 10 } 49 if (nonce[5] & 0xff) != (0x06 ^ 0x02) { return 11 } 50 if (nonce[6] & 0xff) != (0x07 ^ 0x03) { return 12 } 51 if (nonce[11] & 0xff) != (0x0c ^ 0x08) { return 13 } 52 53 // ---- Test A: round-trip encrypt+decrypt ---- 54 let key: *u8 = sys_mmap(64) 55 var k: i64 = 0 56 while k < 32 { 57 key[k] = 0xa0 + k 58 k = k + 1 59 } 60 let content: *u8 = sys_mmap(64) 61 let msg_bytes: i64 = 23 // arbitrary length 62 var c: i64 = 0 63 while c < msg_bytes { 64 content[c] = 0x40 + c 65 c = c + 1 66 } 67 let header: *u8 = sys_mmap(16) 68 let ct: *u8 = sys_mmap(128) 69 let tag: *u8 = sys_mmap(32) 70 let v1: i64 = nx_tls13_record_encrypt( 71 key, iv, 7, 72 content, msg_bytes, 73 NX_TLS13_CT_HANDSHAKE, 74 0, 75 header, ct, tag 76 ) 77 if v1 != NX_TLS13_REC_VERDICT_OK { return 20 } 78 // Header length field should equal msg_bytes + 1 (content_type) + 16 (tag). 79 let expected_len: i64 = msg_bytes + 1 + 16 80 let actual_len: i64 = ((header[3] & 0xff) << 8) | (header[4] & 0xff) 81 if actual_len != expected_len { return 21 } 82 83 let pt_out: *u8 = sys_mmap(128) 84 let ct_type_out: *i64 = sys_mmap(16) as *i64 85 let ct_len_out: *i64 = sys_mmap(16) as *i64 86 let v2: i64 = nx_tls13_record_decrypt( 87 key, iv, 7, 88 header, 89 ct, msg_bytes + 1, // inner length = content + type byte 90 tag, 91 pt_out, ct_type_out, ct_len_out 92 ) 93 if v2 != NX_TLS13_REC_VERDICT_OK { return 30 } 94 if *ct_type_out != NX_TLS13_CT_HANDSHAKE { return 31 } 95 if *ct_len_out != msg_bytes { return 32 } 96 var r: i64 = 0 97 while r < msg_bytes { 98 if (pt_out[r] & 0xff) != (content[r] & 0xff) { return 40 + r } 99 r = r + 1 100 } 101 102 // ---- Test B: nonce-with-seq varies output ---- 103 let ct_seq0: *u8 = sys_mmap(128) 104 let tag_seq0: *u8 = sys_mmap(32) 105 let header0: *u8 = sys_mmap(16) 106 nx_tls13_record_encrypt( 107 key, iv, 0, 108 content, msg_bytes, 109 NX_TLS13_CT_HANDSHAKE, 110 0, 111 header0, ct_seq0, tag_seq0 112 ) 113 let ct_seq1: *u8 = sys_mmap(128) 114 let tag_seq1: *u8 = sys_mmap(32) 115 let header1: *u8 = sys_mmap(16) 116 nx_tls13_record_encrypt( 117 key, iv, 1, 118 content, msg_bytes, 119 NX_TLS13_CT_HANDSHAKE, 120 0, 121 header1, ct_seq1, tag_seq1 122 ) 123 // Ciphertexts MUST differ (different keystream). 124 var diff_count: i64 = 0 125 var d: i64 = 0 126 while d < msg_bytes + 1 { 127 if (ct_seq0[d] & 0xff) != (ct_seq1[d] & 0xff) { diff_count = diff_count + 1 } 128 d = d + 1 129 } 130 if diff_count < (msg_bytes + 1) - 2 { return 80 } // expect almost all bytes to differ 131 132 // Tags MUST differ. 133 if (tag_seq0[0] & 0xff) == (tag_seq1[0] & 0xff) { 134 if (tag_seq0[8] & 0xff) == (tag_seq1[8] & 0xff) { return 81 } 135 } 136 137 // ---- Test C: tampered tag rejected ---- 138 let bad_tag: *u8 = sys_mmap(32) 139 var bi: i64 = 0 140 while bi < 16 { 141 bad_tag[bi] = tag[bi] 142 bi = bi + 1 143 } 144 bad_tag[7] = bad_tag[7] ^ 0x40 145 let v_bad_tag: i64 = nx_tls13_record_decrypt( 146 key, iv, 7, header, ct, msg_bytes + 1, bad_tag, 147 pt_out, ct_type_out, ct_len_out 148 ) 149 if v_bad_tag != NX_TLS13_REC_VERDICT_TAG_MISMATCH { return 90 } 150 151 // ---- Test D: tampered header (wrong length in AAD) rejected ---- 152 let bad_header: *u8 = sys_mmap(16) 153 bad_header[0] = header[0] 154 bad_header[1] = header[1] 155 bad_header[2] = header[2] 156 bad_header[3] = header[3] 157 bad_header[4] = header[4] ^ 1 // wrong length lo byte 158 let v_bad_h: i64 = nx_tls13_record_decrypt( 159 key, iv, 7, bad_header, ct, msg_bytes + 1, tag, 160 pt_out, ct_type_out, ct_len_out 161 ) 162 if v_bad_h != NX_TLS13_REC_VERDICT_TAG_MISMATCH { return 91 } 163 164 // ---- Test E: padding round-trip ---- 165 let header_pad: *u8 = sys_mmap(16) 166 let ct_pad: *u8 = sys_mmap(128) 167 let tag_pad: *u8 = sys_mmap(32) 168 let pad_len: i64 = 7 169 nx_tls13_record_encrypt( 170 key, iv, 42, 171 content, msg_bytes, 172 NX_TLS13_CT_APPLICATION_DATA, 173 pad_len, 174 header_pad, ct_pad, tag_pad 175 ) 176 let pt_pad: *u8 = sys_mmap(128) 177 let v_pad: i64 = nx_tls13_record_decrypt( 178 key, iv, 42, header_pad, 179 ct_pad, msg_bytes + 1 + pad_len, tag_pad, 180 pt_pad, ct_type_out, ct_len_out 181 ) 182 if v_pad != NX_TLS13_REC_VERDICT_OK { return 100 } 183 if *ct_type_out != NX_TLS13_CT_APPLICATION_DATA { return 101 } 184 if *ct_len_out != msg_bytes { return 102 } // padding stripped 185 186 // ---- Test F: verdict gate ---- 187 if nx_tls13_rec_verdict_is_valid(NX_TLS13_REC_VERDICT_OK) != 1 { return 110 } 188 if nx_tls13_rec_verdict_is_valid(NX_TLS13_REC_VERDICT_N) != 0 { return 111 } 189 if nx_tls13_rec_verdict_is_valid(0 - 1) != 0 { return 112 } 190 191 return 0 192}