nx_poly1305.nx source

1// poly1305.nx -- Bernstein's Poly1305 MAC (RFC 8439 variant). 2// 3// license_tier: INDEPENDENT_REDERIVE 4// genealogy_id: international-research-sources/ietf/rfc_8439 5// 6// One-time authenticator over prime p = 2^130 - 5. Takes a 256-bit 7// one-time key (128-bit r clamped + 128-bit s), a message of any 8// length, and produces a 16-byte tag that is unforgeable under a 9// unique-per-message key assumption. 10// 11// Why Poly1305: 12// - Proven secure in the one-time-key model (Bernstein 2005). 13// - Pairs with ChaCha20 to form the RFC 8439 AEAD construction 14// (ChaCha20-Poly1305), the primary TLS 1.3 cipher suite that 15// avoids AES cache-side-channel concerns. 16// - Naturally constant-time on this design: only modular 17// multiplication and addition, no branches on key/message 18// bits. (Some implementations use table lookups for 19// performance -- we avoid those for side-channel reasons.) 20// - Under Grover's algorithm a 128-bit MAC has 64-bit effective 21// security against quantum second-preimage -- that's marginal, 22// but second-preimage on a MAC isn't a practical attack; the 23// one-time-key property is what matters. 24// 25// Arithmetic representation: 26// r and acc live as 5 x 26-bit limbs (total ~130 bits). Each 27// limb fits in i64 with headroom; partial products during 28// multiplication sum to at most ~5 * 2^52 = 2^54.3, still in 29// i64 range. After multiplication we carry-propagate and 30// reduce modulo p = 2^130 - 5 via the standard Bernstein trick 31// (multiply high bits by 5, add back to low). 32// 33// Invariants: 34// P1 No branch depends on secret data (key or message bytes). 35// P2 The message is processed exactly once per block; padding 36// of the final short block is explicit (append 0x01, zero- 37// extend), no early exit. 38// P3 The r-clamp (RFC 8439 §2.5) is applied once at key setup; 39// never reapplied mid-stream so no key material leaks. 40// P4 Caller guarantees a *fresh* 256-bit key per message. 41// Poly1305 is not secure if the same r+s pair authenticates 42// two distinct messages. In ChaCha20-Poly1305 this is 43// enforced by deriving (r, s) from ChaCha20(key, nonce, 0). 44// 45// References: 46// - RFC 8439 section 2.5 (Poly1305 algorithm) 47// - RFC 8439 Appendix A.3 (test vectors) 48// - Bernstein 2005 "The Poly1305-AES MAC" 49// 50// nx_safety_envelope: 51// intended_use: "Poly1305 authenticator -- one-time MAC for 52// ChaCha20-Poly1305 AEAD (RFC 8439) + general 53// per-key-per-message authenticator" 54// sil_target: SIL3 (MAC primitive; forgery = arbitrary 55// message accepted) 56// asil_target: QM 57// dal_target: DAL B 58// evidence: [RFC_8439_canonical_basis, 59// Bernstein_2005_paper, no_FP, 60// constant_time_clamping_design] 61// hazard_register: [bug-tape-key-reuse-CATASTROPHIC, 62// bug-tape-tag-truncation-via-bad-length] 63// residual_risk: "Each (r, s) Poly1305 key is ONE-TIME by 64// construction (Wegman-Carter). Caller 65// MUST derive per-message via ChaCha20 66// keystream or equivalent; reuse breaks 67// unforgeability." 68// verdict: NOT_YET_EVALUATED 69 70import "nx_syscalls.nx" 71 72// Load a little-endian u32 from buf[off..off+4]. 73func p_load_u32_le(buf: *u8, off: i64) -> i64 { 74 let b0: i64 = buf[off + 0] 75 let b1: i64 = buf[off + 1] 76 let b2: i64 = buf[off + 2] 77 let b3: i64 = buf[off + 3] 78 return b0 | (b1 << 8) | (b2 << 16) | (b3 << 24) 79} 80 81// Store a little-endian u32 to buf[off..off+4]. 82func p_store_u32_le(buf: *u8, off: i64, v: i64) -> i64 { 83 buf[off + 0] = v & 0xFF 84 buf[off + 1] = (v >> 8) & 0xFF 85 buf[off + 2] = (v >> 16) & 0xFF 86 buf[off + 3] = (v >> 24) & 0xFF 87 return 0 88} 89 90// Clamp r per RFC 8439 §2.5.1: certain bits must be zero to keep 91// the multiply results bounded and the security proof valid. 92// r[3], r[7], r[11], r[15] top 4 bits cleared (mask 0x0f) 93// r[4], r[8], r[12] bottom 2 bits cleared (mask 0xfc) 94// We operate on the 16 raw bytes in-place. 95func poly1305_clamp(r: *u8) -> i64 { 96 r[3] = r[3] & 0x0F 97 r[7] = r[7] & 0x0F 98 r[11] = r[11] & 0x0F 99 r[15] = r[15] & 0x0F 100 r[4] = r[4] & 0xFC 101 r[8] = r[8] & 0xFC 102 r[12] = r[12] & 0xFC 103 return 0 104} 105 106// Full MAC computation. 107// key: 32 bytes = r(16) || s(16) 108// msg: message bytes to authenticate 109// n: message length in bytes 110// tag: 16-byte output buffer 111// 112// Uses a 5 x 26-bit limb representation for both r and acc. The 113// message is fed in 16-byte blocks (final partial block padded with 114// 0x01 then zero-extended); each block's 130-bit value is added to 115// acc (with the high "1" bit per full block), then acc *= r mod p. 116// After the last block, acc += s mod 2^128 and serializes. 117func poly1305_mac(key: *u8, msg: *u8, n: i64, tag: *u8) -> i64 { 118 // --- key setup --- 119 // r-clamp operates on a local copy; never mutate caller's key. 120 let rbuf: *u8 = sys_mmap(16) 121 var ki: i64 = 0 122 while ki < 16 { rbuf[ki] = key[ki]; ki = ki + 1 } 123 poly1305_clamp(rbuf) 124 125 // Split clamped r into 5 x 26-bit limbs. 126 let r_lo: i64 = p_load_u32_le(rbuf, 0) // bits 0..31 127 let r_m1: i64 = p_load_u32_le(rbuf, 4) // bits 32..63 128 let r_m2: i64 = p_load_u32_le(rbuf, 8) // bits 64..95 129 let r_hi: i64 = p_load_u32_le(rbuf, 12) // bits 96..127 130 131 let r0: i64 = r_lo & 0x3FFFFFF 132 let r1: i64 = ((r_lo >> 26) | (r_m1 << 6)) & 0x3FFFFFF 133 let r2: i64 = ((r_m1 >> 20) | (r_m2 << 12)) & 0x3FFFFFF 134 let r3: i64 = ((r_m2 >> 14) | (r_hi << 18)) & 0x3FFFFFF 135 let r4: i64 = (r_hi >> 8) & 0x3FFFFFF 136 137 // Precompute 5 * r1..r4 for the reduction step. (Each scaled 138 // value still fits in 32 bits since r_i <= 2^26 and 5 < 2^3.) 139 let s1: i64 = r1 * 5 140 let s2: i64 = r2 * 5 141 let s3: i64 = r3 * 5 142 let s4: i64 = r4 * 5 143 144 // Accumulator starts at 0. 145 var h0: i64 = 0 146 var h1: i64 = 0 147 var h2: i64 = 0 148 var h3: i64 = 0 149 var h4: i64 = 0 150 151 // --- block loop --- 152 let block: *u8 = sys_mmap(16) 153 var pos: i64 = 0 154 while pos < n { 155 // Build a 17-byte block: up to 16 message bytes, padded 0x01. 156 var take: i64 = 16 157 if n - pos < 16 { take = n - pos } 158 var bi: i64 = 0 159 while bi < take { block[bi] = msg[pos + bi]; bi = bi + 1 } 160 // Zero any remaining bytes in the 16-byte buffer. 161 while bi < 16 { block[bi] = 0; bi = bi + 1 } 162 163 // Load block as 5 x 26-bit limbs; the high "1" bit goes on 164 // the high limb, or becomes 2^(8*take) for the final partial. 165 let b_lo: i64 = p_load_u32_le(block, 0) 166 let b_m1: i64 = p_load_u32_le(block, 4) 167 let b_m2: i64 = p_load_u32_le(block, 8) 168 let b_hi: i64 = p_load_u32_le(block, 12) 169 170 var c0: i64 = b_lo & 0x3FFFFFF 171 var c1: i64 = ((b_lo >> 26) | (b_m1 << 6)) & 0x3FFFFFF 172 var c2: i64 = ((b_m1 >> 20) | (b_m2 << 12)) & 0x3FFFFFF 173 var c3: i64 = ((b_m2 >> 14) | (b_hi << 18)) & 0x3FFFFFF 174 var c4: i64 = (b_hi >> 8) & 0x3FFFFFF 175 176 // Add the "1" bit. For a full 16-byte block the bit is at 177 // position 128; for a short final block it's at position 178 // 8*take (so the tag is still unambiguous about length). 179 if take == 16 { 180 c4 = c4 | (1 << 24) 181 } else { 182 // Recompute c0..c4 from a zero-padded buffer where byte 183 // `take` holds 0x01 and the rest are zero -- simpler 184 // than patching individual limbs. 185 bi = 0 186 while bi < 16 { block[bi] = 0; bi = bi + 1 } 187 bi = 0 188 while bi < take { block[bi] = msg[pos + bi]; bi = bi + 1 } 189 block[take] = 0x01 190 let q_lo: i64 = p_load_u32_le(block, 0) 191 let q_m1: i64 = p_load_u32_le(block, 4) 192 let q_m2: i64 = p_load_u32_le(block, 8) 193 let q_hi: i64 = p_load_u32_le(block, 12) 194 c0 = q_lo & 0x3FFFFFF 195 c1 = ((q_lo >> 26) | (q_m1 << 6)) & 0x3FFFFFF 196 c2 = ((q_m1 >> 20) | (q_m2 << 12)) & 0x3FFFFFF 197 c3 = ((q_m2 >> 14) | (q_hi << 18)) & 0x3FFFFFF 198 c4 = (q_hi >> 8) & 0x3FFFFFF 199 } 200 201 // h += c 202 h0 = h0 + c0 203 h1 = h1 + c1 204 h2 = h2 + c2 205 h3 = h3 + c3 206 h4 = h4 + c4 207 208 // h = (h * r) mod p. Schoolbook multiplication of 5x5 limbs 209 // with the "high limb times 5" trick for reduction. 210 let d0: i64 = h0 * r0 + h1 * s4 + h2 * s3 + h3 * s2 + h4 * s1 211 let d1: i64 = h0 * r1 + h1 * r0 + h2 * s4 + h3 * s3 + h4 * s2 212 let d2: i64 = h0 * r2 + h1 * r1 + h2 * r0 + h3 * s4 + h4 * s3 213 let d3: i64 = h0 * r3 + h1 * r2 + h2 * r1 + h3 * r0 + h4 * s4 214 let d4: i64 = h0 * r4 + h1 * r3 + h2 * r2 + h3 * r1 + h4 * r0 215 216 // Carry-propagate back to 26-bit limbs. 217 var c_h0: i64 = d0 & 0x3FFFFFF 218 let k1: i64 = d0 >> 26 219 var c_h1: i64 = (d1 + k1) & 0x3FFFFFF 220 let k2: i64 = (d1 + k1) >> 26 221 var c_h2: i64 = (d2 + k2) & 0x3FFFFFF 222 let k3: i64 = (d2 + k2) >> 26 223 var c_h3: i64 = (d3 + k3) & 0x3FFFFFF 224 let k4: i64 = (d3 + k3) >> 26 225 var c_h4: i64 = (d4 + k4) & 0x3FFFFFF 226 let k5: i64 = (d4 + k4) >> 26 227 // Fold overflow back into h0 via the 2^130 = 5 mod p trick. 228 c_h0 = c_h0 + k5 * 5 229 c_h1 = c_h1 + (c_h0 >> 26) 230 c_h0 = c_h0 & 0x3FFFFFF 231 232 h0 = c_h0 233 h1 = c_h1 234 h2 = c_h2 235 h3 = c_h3 236 h4 = c_h4 237 238 pos = pos + take 239 } 240 241 // --- finalise --- 242 // Collapse 5 limbs back to a 128-bit value, then add s. 243 // First a final carry pass to get each limb into [0, 2^26). 244 h1 = h1 + (h0 >> 26); h0 = h0 & 0x3FFFFFF 245 h2 = h2 + (h1 >> 26); h1 = h1 & 0x3FFFFFF 246 h3 = h3 + (h2 >> 26); h2 = h2 & 0x3FFFFFF 247 h4 = h4 + (h3 >> 26); h3 = h3 & 0x3FFFFFF 248 h0 = h0 + (h4 >> 26) * 5 249 h4 = h4 & 0x3FFFFFF 250 h1 = h1 + (h0 >> 26) 251 h0 = h0 & 0x3FFFFFF 252 253 // Conditional subtract p = 2^130 - 5. If h >= p, set h := h - p. 254 // Implemented constant-time by computing h + 5 (which would 255 // overflow 2^130 iff h >= p) and selecting by the carry out. 256 var g0: i64 = h0 + 5 257 var g1: i64 = h1 + (g0 >> 26); g0 = g0 & 0x3FFFFFF 258 var g2: i64 = h2 + (g1 >> 26); g1 = g1 & 0x3FFFFFF 259 var g3: i64 = h3 + (g2 >> 26); g2 = g2 & 0x3FFFFFF 260 var g4: i64 = h4 + (g3 >> 26) - (1 << 26) 261 g3 = g3 & 0x3FFFFFF 262 263 // Shift-semantics-independent sign-bit extract. Both nxc2 264 // backends (RV64 + x86_64) emit ARITHMETIC right-shift for `>>`, 265 // so `(g4 >> 63)` gives -1 when g4<0, not 1; the single-line 266 // `^ -1` trick the original NaCl reference uses assumes a 267 // LOGICAL shift via uint32, which we don't have. Masking bit 0 268 // then negating produces -1 for g4<0 regardless of shift kind. 269 // (F17 cross-backend codegen divergence trap, except both 270 // backends are wrong here. Cardinal: bench/audit_rv64_honesty_sweep.) 271 let mask: i64 = 0 - ((g4 >> 63) & 1) // -1 if g4<0 (keep h), else 0 272 let nmask: i64 = mask ^ -1 // 0 if g4<0, else -1 273 h0 = (h0 & mask) | (g0 & nmask) 274 h1 = (h1 & mask) | (g1 & nmask) 275 h2 = (h2 & mask) | (g2 & nmask) 276 h3 = (h3 & mask) | (g3 & nmask) 277 h4 = (h4 & mask) | (g4 & nmask) 278 279 // Serialize h as 4 x u32 LE, adding s (bytes 16..31 of key) mod 2^128. 280 // Pack the 5x26-bit selected limbs into 4x32-bit u32 words. 281 // The `& 0xFFFFFFFF` mask MUST be applied here, not just on the 282 // sum: `(h1 << 26)` leaks bits 32..51 into the i64, which then 283 // contaminate the carry when we do `>> 32` on (a + s). Bug 284 // class F-poly-1: convert-to-u32 must mask BEFORE addition, not 285 // just when extracting the low 32 of the sum. (OpenSSL's 286 // poly1305_finish does this masking explicitly; the NaCl 32-bit 287 // reference uses unsigned types so masking is implicit.) 288 let a0: i64 = ( h0 | (h1 << 26)) & 0xFFFFFFFF 289 let a1: i64 = ((h1 >> 6) | (h2 << 20)) & 0xFFFFFFFF 290 let a2: i64 = ((h2 >> 12) | (h3 << 14)) & 0xFFFFFFFF 291 let a3: i64 = ((h3 >> 18) | (h4 << 8)) & 0xFFFFFFFF 292 293 let s0: i64 = p_load_u32_le(key, 16) 294 let s_s1: i64 = p_load_u32_le(key, 20) 295 let s_s2: i64 = p_load_u32_le(key, 24) 296 let s_s3: i64 = p_load_u32_le(key, 28) 297 298 var t0: i64 = (a0 + s0) & 0xFFFFFFFF 299 let ca0: i64 = (a0 + s0) >> 32 300 var t1: i64 = (a1 + s_s1 + ca0) & 0xFFFFFFFF 301 let ca1: i64 = (a1 + s_s1 + ca0) >> 32 302 var t2: i64 = (a2 + s_s2 + ca1) & 0xFFFFFFFF 303 let ca2: i64 = (a2 + s_s2 + ca1) >> 32 304 var t3: i64 = (a3 + s_s3 + ca2) & 0xFFFFFFFF 305 306 p_store_u32_le(tag, 0, t0) 307 p_store_u32_le(tag, 4, t1) 308 p_store_u32_le(tag, 8, t2) 309 p_store_u32_le(tag, 12, t3) 310 return 0 311} 312 313// Constant-time tag comparison. Returns 1 if a[0..16] == b[0..16], 314// 0 otherwise. TLS Finished verification MUST use this rather than 315// a short-circuiting memcmp; the timing leak otherwise lets a remote 316// attacker bisect the tag byte-by-byte. 317func poly1305_tag_equal(a: *u8, b: *u8) -> i64 { 318 var diff: i64 = 0 319 var i: i64 = 0 320 while i < 16 { 321 diff = diff | ((a[i] & 0xff) ^ (b[i] & 0xff)) 322 i = i + 1 323 } 324 let neg: i64 = 0 - diff 325 let neq: i64 = (neg >> 63) & 1 326 return 1 - neq 327} 328 329// Real KAT execution lives in runtime/nx_poly1305_test.nx, which 330// imports this module and runs RFC 8439 §2.5.2 (34-byte 331// "Cryptographic Forum Research Group" vector) against the 332// expected tag a8061dc1305136c6c22b8baf0c0127a9. Removed the 333// stub `main` here so importing this module from a test file 334// doesn't double-define main.