nx_chacha20_poly1305.nx source
↩ module page · 259 lines · 9329 B
1// nx_chacha20_poly1305.nx -- AEAD per RFC 8439 §2.8.
2//
3// Phase 0b §A.2 of the Nishi TLS 1.3 stack per
4// docs/NISHI_TLS13_GAP_AUDIT.md. Composes the already-shipped
5// ChaCha20 stream cipher and Poly1305 universal hash into the
6// Authenticated Encryption with Associated Data primitive that
7// TLS 1.3, QUIC, WireGuard, Signal, and Noise all use.
8//
9// Construction:
10// 1. otk = ChaCha20(key, counter=0, nonce)[0..32]
11// -- the per-message Poly1305 key, fresh because nonce is fresh
12// 2. ciphertext = ChaCha20(key, counter=1, nonce, plaintext)
13// -- counter starts at 1 because counter 0 was burnt on the OTK
14// 3. mac_data = aad || pad16(aad) || ct || pad16(ct) || u64_le(|aad|) || u64_le(|ct|)
15// 4. tag = Poly1305(otk, mac_data)
16//
17// Decrypt is symmetric: recompute tag, constant-time compare, then
18// XOR ciphertext with the same keystream. Tag check FIRST, decrypt
19// AFTER -- this matters because returning plaintext when the tag
20// failed would let an attacker probe for valid ciphertexts byte-by-byte
21// (the classic CBC-padding-oracle attack pattern, ported to AEAD by
22// careless implementations).
23//
24// What it does today:
25// - encrypt + tag in one call
26// - decrypt + verify in one call; constant-time tag compare
27// - sealed AEAD verdict (OK / TAG_MISMATCH)
28//
29// What it doesn't do yet:
30// - chunked / streaming encryption (one-shot only; matches
31// TLS 1.3 record-layer usage which is bounded by 2^14 + 256)
32// - extended XChaCha20-Poly1305 (24-byte nonce variant; Signal
33// + libsodium use this; not yet in TLS 1.3)
34//
35// KAT verified:
36// - RFC 8439 §2.8.2 worked example (114-byte Sunscreen vector +
37// 12-byte AAD; both ciphertext and tag match spec)
38// - internal round-trip on random-ish data
39// - tampered-tag rejection
40// - tampered-ciphertext rejection
41//
42// Composes with:
43// - nx_chacha20 (stream cipher)
44// - nx_poly1305 (universal hash + constant-time tag compare)
45// - Above the AEAD: nx_tls13_record (RFC 8446 §5.2 record protection)
46//
47// license_tier: INDEPENDENT_REDERIVE
48// genealogy_id: international-research-sources/ietf/rfc_8439
49// lineage_id: nishi_tls13_aead_chacha20_poly1305_q10
50//
51// nx_safety_envelope:
52// intended_use: "ChaCha20-Poly1305 AEAD (RFC 8439 §2.8) --
53// TLS 1.3 mandatory cipher suite; preferred
54// on shared-cache CPUs where AES-GCM has
55// timing side-channels"
56// sil_target: SIL3 (combined cipher; one nonce reuse =
57// full break per Joux 2006)
58// asil_target: QM
59// dal_target: DAL B
60// iec_62304_class: B
61// evidence: [RFC_8439_canonical_basis,
62// inherits_nx_chacha20_constant_time,
63// inherits_nx_poly1305_evidence,
64// AAD_handled_per_section_2_8]
65// hazard_register: [bug-tape-nonce-reuse-CATASTROPHIC,
66// bug-tape-AAD-length-not-encoded-in-MAC,
67// bug-tape-tag-truncation-attack]
68// residual_risk: "Nonce uniqueness CATASTROPHIC failure mode
69// (Joux 2006). Caller MUST guarantee 96-bit
70// nonce uniqueness per key. Substrate cannot
71// enforce; documented prominently."
72// verdict: NOT_YET_EVALUATED
73
74import "nx_syscalls.nx"
75import "nx_chacha20.nx"
76import "nx_poly1305.nx"
77
78const NX_AEAD_TAG_BYTES: i64 = 16
79const NX_AEAD_NONCE_BYTES: i64 = 12
80const NX_AEAD_KEY_BYTES: i64 = 32
81
82// Sealed AEAD verdict.
83const NX_AEAD_VERDICT_UNKNOWN: i64 = 0
84const NX_AEAD_VERDICT_OK: i64 = 1
85const NX_AEAD_VERDICT_TAG_MISMATCH: i64 = 2
86const NX_AEAD_VERDICT_N: i64 = 3
87
88// Derive the one-time Poly1305 key per RFC 8439 §2.6:
89// otk = first 32 bytes of ChaCha20(key, counter=0, nonce).
90func aead_derive_otk(key: *u8, nonce: *u8, otk_out: *u8) -> i64 {
91 let block: *u8 = sys_mmap(128)
92 chacha20_block(key, 0, nonce, block)
93 var i: i64 = 0
94 while i < 32 {
95 otk_out[i] = block[i]
96 i = i + 1
97 }
98 return 0
99}
100
101// Write a u64 as 8 little-endian bytes to buf[off..off+8].
102func aead_put_u64_le(buf: *u8, off: i64, v: i64) -> i64 {
103 buf[off + 0] = v & 0xff
104 buf[off + 1] = (v >> 8) & 0xff
105 buf[off + 2] = (v >> 16) & 0xff
106 buf[off + 3] = (v >> 24) & 0xff
107 buf[off + 4] = (v >> 32) & 0xff
108 buf[off + 5] = (v >> 40) & 0xff
109 buf[off + 6] = (v >> 48) & 0xff
110 buf[off + 7] = (v >> 56) & 0xff
111 return 8
112}
113
114// Build mac_data = aad || pad16(aad) || ct || pad16(ct) || u64_le(aad_len) || u64_le(ct_len)
115// into mac_buf. Returns total bytes written.
116//
117// pad16(x) = number of zero bytes needed so |x| rounds up to a 16-byte
118// boundary; pad16(0-length) = 0.
119func aead_build_mac_data(
120 aad: *u8, aad_len: i64,
121 ct: *u8, ct_len: i64,
122 mac_buf: *u8
123) -> i64 {
124 var o: i64 = 0
125 var i: i64 = 0
126 while i < aad_len {
127 mac_buf[o + i] = aad[i]
128 i = i + 1
129 }
130 o = o + aad_len
131 let aad_rem: i64 = aad_len % 16
132 let aad_pad: i64 = (16 - aad_rem) % 16
133 var p: i64 = 0
134 while p < aad_pad {
135 mac_buf[o + p] = 0
136 p = p + 1
137 }
138 o = o + aad_pad
139 var j: i64 = 0
140 while j < ct_len {
141 mac_buf[o + j] = ct[j]
142 j = j + 1
143 }
144 o = o + ct_len
145 let ct_rem: i64 = ct_len % 16
146 let ct_pad: i64 = (16 - ct_rem) % 16
147 var q: i64 = 0
148 while q < ct_pad {
149 mac_buf[o + q] = 0
150 q = q + 1
151 }
152 o = o + ct_pad
153 aead_put_u64_le(mac_buf, o, aad_len)
154 o = o + 8
155 aead_put_u64_le(mac_buf, o, ct_len)
156 o = o + 8
157 return o
158}
159
160// Encrypt + authenticate. Writes pt_len bytes of ciphertext to ct_out
161// and 16 bytes of authentication tag to tag_out. Returns
162// NX_AEAD_VERDICT_OK.
163//
164// Nonce MUST be unique per (key, message) pair -- a nonce-reuse
165// catastrophically breaks Poly1305's one-time-key assumption and
166// leaks the authentication key. TLS 1.3 enforces this via per-record
167// sequence number XOR'd into the static IV.
168func nx_chacha20_poly1305_encrypt(
169 key: *u8, nonce: *u8,
170 aad: *u8, aad_len: i64,
171 pt: *u8, pt_len: i64,
172 ct_out: *u8,
173 tag_out: *u8
174) -> i64 {
175 let otk: *u8 = sys_mmap(64)
176 aead_derive_otk(key, nonce, otk)
177
178 chacha20_encrypt(key, 1, nonce, pt, pt_len, ct_out)
179
180 // Worst-case mac_data size: aad + 15 (max pad) + ct + 15 (max pad) + 16 (lens).
181 let mac_cap: i64 = aad_len + pt_len + 64
182 let mac_buf: *u8 = sys_mmap(mac_cap)
183 let mac_len: i64 = aead_build_mac_data(aad, aad_len, ct_out, pt_len, mac_buf)
184
185 poly1305_mac(otk, mac_buf, mac_len, tag_out)
186 return NX_AEAD_VERDICT_OK
187}
188
189// Decrypt + verify. Tag check FIRST (constant-time), then decrypt.
190// On tag mismatch, pt_out is NOT written and verdict TAG_MISMATCH is
191// returned -- caller must NOT use pt_out's contents in that case.
192//
193// Constant-time-first is the absorbed lesson from
194// docs/NISHI_BROWSER_KNOWN_LESSONS.md §AEAD: returning partial
195// plaintext on tag failure enables padding-oracle-style probing.
196// native perf split accumulators (stderr-read via getters) -- which AEAD half is slow.
197static G_CP_MAC_MS: i64
198static G_CP_POLY_MS: i64
199static G_CP_CHA_MS: i64
200func nx_cp_mac_ms() -> i64 { return G_CP_MAC_MS }
201func nx_cp_poly_ms() -> i64 { return G_CP_POLY_MS }
202func nx_cp_cha_ms() -> i64 { return G_CP_CHA_MS }
203
204// reusable decrypt scratch (allocate once; TLS records <= 16640, so 17000 covers mac_buf).
205const NX_CP_MACBUF_CAP: i64 = 17000
206static G_CP_SCRATCH: i64
207static G_CP_OTK: i64
208static G_CP_MACBUF: i64
209static G_CP_ETAG: i64
210static G_CP_CALLS: i64
211func nx_cp_calls() -> i64 { return G_CP_CALLS }
212func nx_cp_scratch() -> i64 { return G_CP_SCRATCH }
213
214func nx_chacha20_poly1305_decrypt(
215 key: *u8, nonce: *u8,
216 aad: *u8, aad_len: i64,
217 ct: *u8, ct_len: i64,
218 tag: *u8,
219 pt_out: *u8
220) -> i64 {
221 G_CP_CALLS = G_CP_CALLS + 1
222 if G_CP_SCRATCH == 0 {
223 G_CP_OTK = sys_mmap(64) as i64
224 G_CP_MACBUF = sys_mmap(NX_CP_MACBUF_CAP) as i64
225 G_CP_ETAG = sys_mmap(32) as i64
226 G_CP_SCRATCH = 1
227 sys_write(2, "A" as *u8, 1) // DIAG: one mark per scratch allocation (1=cached, many=re-alloc)
228 }
229 let otk: *u8 = G_CP_OTK as *u8
230 aead_derive_otk(key, nonce, otk)
231
232 let _m0: i64 = sys_now_ms()
233 let mac_cap: i64 = aad_len + ct_len + 64
234 var mac_buf: *u8 = G_CP_MACBUF as *u8
235 if mac_cap > NX_CP_MACBUF_CAP { mac_buf = sys_mmap(mac_cap) } // oversized record (rare) -> one-off
236 let mac_len: i64 = aead_build_mac_data(aad, aad_len, ct, ct_len, mac_buf)
237 G_CP_MAC_MS = G_CP_MAC_MS + (sys_now_ms() - _m0)
238
239 let expected_tag: *u8 = G_CP_ETAG as *u8
240 let _p0: i64 = sys_now_ms()
241 poly1305_mac(otk, mac_buf, mac_len, expected_tag)
242 G_CP_POLY_MS = G_CP_POLY_MS + (sys_now_ms() - _p0)
243
244 if poly1305_tag_equal(expected_tag, tag) != 1 {
245 return NX_AEAD_VERDICT_TAG_MISMATCH
246 }
247
248 let _c0: i64 = sys_now_ms()
249 chacha20_encrypt(key, 1, nonce, ct, ct_len, pt_out)
250 G_CP_CHA_MS = G_CP_CHA_MS + (sys_now_ms() - _c0)
251 return NX_AEAD_VERDICT_OK
252}
253
254// Sealed-enum validity gate.
255func nx_aead_verdict_is_valid(v: i64) -> i64 {
256 if v < 0 { return 0 }
257 if v >= NX_AEAD_VERDICT_N { return 0 }
258 return 1
259}