poly1305.nx source

1// poly1305.nx -- Bernstein's Poly1305 MAC (RFC 8439 variant). 2// 3// One-time authenticator over prime p = 2^130 - 5. Takes a 256-bit 4// one-time key (128-bit r clamped + 128-bit s), a message of any 5// length, and produces a 16-byte tag that is unforgeable under a 6// unique-per-message key assumption. 7// 8// Why Poly1305: 9// - Proven secure in the one-time-key model (Bernstein 2005). 10// - Pairs with ChaCha20 to form the RFC 8439 AEAD construction 11// (ChaCha20-Poly1305), the primary TLS 1.3 cipher suite that 12// avoids AES cache-side-channel concerns. 13// - Naturally constant-time on this design: only modular 14// multiplication and addition, no branches on key/message 15// bits. (Some implementations use table lookups for 16// performance -- we avoid those for side-channel reasons.) 17// - Under Grover's algorithm a 128-bit MAC has 64-bit effective 18// security against quantum second-preimage -- that's marginal, 19// but second-preimage on a MAC isn't a practical attack; the 20// one-time-key property is what matters. 21// 22// Arithmetic representation: 23// r and acc live as 5 x 26-bit limbs (total ~130 bits). Each 24// limb fits in i64 with headroom; partial products during 25// multiplication sum to at most ~5 * 2^52 = 2^54.3, still in 26// i64 range. After multiplication we carry-propagate and 27// reduce modulo p = 2^130 - 5 via the standard Bernstein trick 28// (multiply high bits by 5, add back to low). 29// 30// Invariants: 31// P1 No branch depends on secret data (key or message bytes). 32// P2 The message is processed exactly once per block; padding 33// of the final short block is explicit (append 0x01, zero- 34// extend), no early exit. 35// P3 The r-clamp (RFC 8439 §2.5) is applied once at key setup; 36// never reapplied mid-stream so no key material leaks. 37// P4 Caller guarantees a *fresh* 256-bit key per message. 38// Poly1305 is not secure if the same r+s pair authenticates 39// two distinct messages. In ChaCha20-Poly1305 this is 40// enforced by deriving (r, s) from ChaCha20(key, nonce, 0). 41// 42// References: 43// - RFC 8439 section 2.5 (Poly1305 algorithm) 44// - RFC 8439 Appendix A.3 (test vectors) 45// - Bernstein 2005 "The Poly1305-AES MAC" 46 47import "syscalls.nx" 48 49// Load a little-endian u32 from buf[off..off+4]. 50func p_load_u32_le(buf: *u8, off: i64) -> i64 { 51 let b0: i64 = buf[off + 0] 52 let b1: i64 = buf[off + 1] 53 let b2: i64 = buf[off + 2] 54 let b3: i64 = buf[off + 3] 55 return b0 | (b1 << 8) | (b2 << 16) | (b3 << 24) 56} 57 58// Store a little-endian u32 to buf[off..off+4]. 59func p_store_u32_le(buf: *u8, off: i64, v: i64) -> i64 { 60 buf[off + 0] = v & 0xFF 61 buf[off + 1] = (v >> 8) & 0xFF 62 buf[off + 2] = (v >> 16) & 0xFF 63 buf[off + 3] = (v >> 24) & 0xFF 64 return 0 65} 66 67// Clamp r per RFC 8439 §2.5.1: certain bits must be zero to keep 68// the multiply results bounded and the security proof valid. 69// r[3], r[7], r[11], r[15] top 4 bits cleared (mask 0x0f) 70// r[4], r[8], r[12] bottom 2 bits cleared (mask 0xfc) 71// We operate on the 16 raw bytes in-place. 72func poly1305_clamp(r: *u8) -> i64 { 73 r[3] = r[3] & 0x0F 74 r[7] = r[7] & 0x0F 75 r[11] = r[11] & 0x0F 76 r[15] = r[15] & 0x0F 77 r[4] = r[4] & 0xFC 78 r[8] = r[8] & 0xFC 79 r[12] = r[12] & 0xFC 80 return 0 81} 82 83// Full MAC computation. 84// key: 32 bytes = r(16) || s(16) 85// msg: message bytes to authenticate 86// n: message length in bytes 87// tag: 16-byte output buffer 88// 89// Uses a 5 x 26-bit limb representation for both r and acc. The 90// message is fed in 16-byte blocks (final partial block padded with 91// 0x01 then zero-extended); each block's 130-bit value is added to 92// acc (with the high "1" bit per full block), then acc *= r mod p. 93// After the last block, acc += s mod 2^128 and serializes. 94func poly1305_mac(key: *u8, msg: *u8, n: i64, tag: *u8) -> i64 { 95 // --- key setup --- 96 // r-clamp operates on a local copy; never mutate caller's key. 97 let rbuf: *u8 = sys_mmap(16) 98 var ki: i64 = 0 99 while ki < 16 { rbuf[ki] = key[ki]; ki = ki + 1 } 100 poly1305_clamp(rbuf) 101 102 // Split clamped r into 5 x 26-bit limbs. 103 let r_lo: i64 = p_load_u32_le(rbuf, 0) // bits 0..31 104 let r_m1: i64 = p_load_u32_le(rbuf, 4) // bits 32..63 105 let r_m2: i64 = p_load_u32_le(rbuf, 8) // bits 64..95 106 let r_hi: i64 = p_load_u32_le(rbuf, 12) // bits 96..127 107 108 let r0: i64 = r_lo & 0x3FFFFFF 109 let r1: i64 = ((r_lo >> 26) | (r_m1 << 6)) & 0x3FFFFFF 110 let r2: i64 = ((r_m1 >> 20) | (r_m2 << 12)) & 0x3FFFFFF 111 let r3: i64 = ((r_m2 >> 14) | (r_hi << 18)) & 0x3FFFFFF 112 let r4: i64 = (r_hi >> 8) & 0x3FFFFFF 113 114 // Precompute 5 * r1..r4 for the reduction step. (Each scaled 115 // value still fits in 32 bits since r_i <= 2^26 and 5 < 2^3.) 116 let s1: i64 = r1 * 5 117 let s2: i64 = r2 * 5 118 let s3: i64 = r3 * 5 119 let s4: i64 = r4 * 5 120 121 // Accumulator starts at 0. 122 var h0: i64 = 0 123 var h1: i64 = 0 124 var h2: i64 = 0 125 var h3: i64 = 0 126 var h4: i64 = 0 127 128 // --- block loop --- 129 let block: *u8 = sys_mmap(16) 130 var pos: i64 = 0 131 while pos < n { 132 // Build a 17-byte block: up to 16 message bytes, padded 0x01. 133 var take: i64 = 16 134 if n - pos < 16 { take = n - pos } 135 var bi: i64 = 0 136 while bi < take { block[bi] = msg[pos + bi]; bi = bi + 1 } 137 // Zero any remaining bytes in the 16-byte buffer. 138 while bi < 16 { block[bi] = 0; bi = bi + 1 } 139 140 // Load block as 5 x 26-bit limbs; the high "1" bit goes on 141 // the high limb, or becomes 2^(8*take) for the final partial. 142 let b_lo: i64 = p_load_u32_le(block, 0) 143 let b_m1: i64 = p_load_u32_le(block, 4) 144 let b_m2: i64 = p_load_u32_le(block, 8) 145 let b_hi: i64 = p_load_u32_le(block, 12) 146 147 var c0: i64 = b_lo & 0x3FFFFFF 148 var c1: i64 = ((b_lo >> 26) | (b_m1 << 6)) & 0x3FFFFFF 149 var c2: i64 = ((b_m1 >> 20) | (b_m2 << 12)) & 0x3FFFFFF 150 var c3: i64 = ((b_m2 >> 14) | (b_hi << 18)) & 0x3FFFFFF 151 var c4: i64 = (b_hi >> 8) & 0x3FFFFFF 152 153 // Add the "1" bit. For a full 16-byte block the bit is at 154 // position 128; for a short final block it's at position 155 // 8*take (so the tag is still unambiguous about length). 156 if take == 16 { 157 c4 = c4 | (1 << 24) 158 } else { 159 // Recompute c0..c4 from a zero-padded buffer where byte 160 // `take` holds 0x01 and the rest are zero -- simpler 161 // than patching individual limbs. 162 bi = 0 163 while bi < 16 { block[bi] = 0; bi = bi + 1 } 164 bi = 0 165 while bi < take { block[bi] = msg[pos + bi]; bi = bi + 1 } 166 block[take] = 0x01 167 let q_lo: i64 = p_load_u32_le(block, 0) 168 let q_m1: i64 = p_load_u32_le(block, 4) 169 let q_m2: i64 = p_load_u32_le(block, 8) 170 let q_hi: i64 = p_load_u32_le(block, 12) 171 c0 = q_lo & 0x3FFFFFF 172 c1 = ((q_lo >> 26) | (q_m1 << 6)) & 0x3FFFFFF 173 c2 = ((q_m1 >> 20) | (q_m2 << 12)) & 0x3FFFFFF 174 c3 = ((q_m2 >> 14) | (q_hi << 18)) & 0x3FFFFFF 175 c4 = (q_hi >> 8) & 0x3FFFFFF 176 } 177 178 // h += c 179 h0 = h0 + c0 180 h1 = h1 + c1 181 h2 = h2 + c2 182 h3 = h3 + c3 183 h4 = h4 + c4 184 185 // h = (h * r) mod p. Schoolbook multiplication of 5x5 limbs 186 // with the "high limb times 5" trick for reduction. 187 let d0: i64 = h0 * r0 + h1 * s4 + h2 * s3 + h3 * s2 + h4 * s1 188 let d1: i64 = h0 * r1 + h1 * r0 + h2 * s4 + h3 * s3 + h4 * s2 189 let d2: i64 = h0 * r2 + h1 * r1 + h2 * r0 + h3 * s4 + h4 * s3 190 let d3: i64 = h0 * r3 + h1 * r2 + h2 * r1 + h3 * r0 + h4 * s4 191 let d4: i64 = h0 * r4 + h1 * r3 + h2 * r2 + h3 * r1 + h4 * r0 192 193 // Carry-propagate back to 26-bit limbs. 194 var c_h0: i64 = d0 & 0x3FFFFFF 195 let k1: i64 = d0 >> 26 196 var c_h1: i64 = (d1 + k1) & 0x3FFFFFF 197 let k2: i64 = (d1 + k1) >> 26 198 var c_h2: i64 = (d2 + k2) & 0x3FFFFFF 199 let k3: i64 = (d2 + k2) >> 26 200 var c_h3: i64 = (d3 + k3) & 0x3FFFFFF 201 let k4: i64 = (d3 + k3) >> 26 202 var c_h4: i64 = (d4 + k4) & 0x3FFFFFF 203 let k5: i64 = (d4 + k4) >> 26 204 // Fold overflow back into h0 via the 2^130 = 5 mod p trick. 205 c_h0 = c_h0 + k5 * 5 206 c_h1 = c_h1 + (c_h0 >> 26) 207 c_h0 = c_h0 & 0x3FFFFFF 208 209 h0 = c_h0 210 h1 = c_h1 211 h2 = c_h2 212 h3 = c_h3 213 h4 = c_h4 214 215 pos = pos + take 216 } 217 218 // --- finalise --- 219 // Collapse 5 limbs back to a 128-bit value, then add s. 220 // First a final carry pass to get each limb into [0, 2^26). 221 h1 = h1 + (h0 >> 26); h0 = h0 & 0x3FFFFFF 222 h2 = h2 + (h1 >> 26); h1 = h1 & 0x3FFFFFF 223 h3 = h3 + (h2 >> 26); h2 = h2 & 0x3FFFFFF 224 h4 = h4 + (h3 >> 26); h3 = h3 & 0x3FFFFFF 225 h0 = h0 + (h4 >> 26) * 5 226 h4 = h4 & 0x3FFFFFF 227 h1 = h1 + (h0 >> 26) 228 h0 = h0 & 0x3FFFFFF 229 230 // Conditional subtract p = 2^130 - 5. If h >= p, set h := h - p. 231 // Implemented constant-time by computing h + 5 (which would 232 // overflow 2^130 iff h >= p) and selecting by the carry out. 233 var g0: i64 = h0 + 5 234 var g1: i64 = h1 + (g0 >> 26); g0 = g0 & 0x3FFFFFF 235 var g2: i64 = h2 + (g1 >> 26); g1 = g1 & 0x3FFFFFF 236 var g3: i64 = h3 + (g2 >> 26); g2 = g2 & 0x3FFFFFF 237 var g4: i64 = h4 + (g3 >> 26) - (1 << 26) 238 g3 = g3 & 0x3FFFFFF 239 240 // mask = 0 if g4 < 0 (i.e. h < p), else all-ones. 241 let mask: i64 = (g4 >> 63) ^ -1 // -1 when g4 < 0, else 0 242 let nmask: i64 = mask ^ -1 243 h0 = (h0 & mask) | (g0 & nmask) 244 h1 = (h1 & mask) | (g1 & nmask) 245 h2 = (h2 & mask) | (g2 & nmask) 246 h3 = (h3 & mask) | (g3 & nmask) 247 h4 = (h4 & mask) | (g4 & nmask) 248 249 // Serialize h as 4 x u32 LE, adding s (bytes 16..31 of key) mod 2^128. 250 let a0: i64 = h0 | (h1 << 26) 251 let a1: i64 = (h1 >> 6) | (h2 << 20) 252 let a2: i64 = (h2 >> 12) | (h3 << 14) 253 let a3: i64 = (h3 >> 18) | (h4 << 8) 254 255 let s0: i64 = p_load_u32_le(key, 16) 256 let s_s1: i64 = p_load_u32_le(key, 20) 257 let s_s2: i64 = p_load_u32_le(key, 24) 258 let s_s3: i64 = p_load_u32_le(key, 28) 259 260 var t0: i64 = (a0 + s0) & 0xFFFFFFFF 261 let ca0: i64 = (a0 + s0) >> 32 262 var t1: i64 = (a1 + s_s1 + ca0) & 0xFFFFFFFF 263 let ca1: i64 = (a1 + s_s1 + ca0) >> 32 264 var t2: i64 = (a2 + s_s2 + ca1) & 0xFFFFFFFF 265 let ca2: i64 = (a2 + s_s2 + ca1) >> 32 266 var t3: i64 = (a3 + s_s3 + ca2) & 0xFFFFFFFF 267 268 p_store_u32_le(tag, 0, t0) 269 p_store_u32_le(tag, 4, t1) 270 p_store_u32_le(tag, 8, t2) 271 p_store_u32_le(tag, 12, t3) 272 return 0 273} 274 275// Compile-only smoke. Real KAT validation (RFC 8439 Appendix A.3 276// test vector 2: key+msg -> a8 06 1d c1 30 51 36 c6 c2 2b 8b af 0c 277// 01 27 a9) requires execution harness pending. 278func main() -> i64 { 279 let key: *u8 = sys_mmap(32) 280 let msg: *u8 = sys_mmap(16) 281 let tag: *u8 = sys_mmap(16) 282 var i: i64 = 0 283 while i < 32 { key[i] = 0; i = i + 1 } 284 i = 0 285 while i < 16 { msg[i] = 0; i = i + 1 } 286 poly1305_mac(key, msg, 16, tag) 287 return tag[0] as i64 288}