aead.nx source
↩ module page · 169 lines · 6239 B
1// aead.nx -- ChaCha20-Poly1305 AEAD (RFC 8439 section 2.8).
2//
3// Authenticated Encryption with Associated Data. Combines
4// ChaCha20 (confidentiality) + Poly1305 (integrity) into a single
5// primitive with a clean API:
6//
7// aead_seal(key, nonce, aad, plaintext) -> (ciphertext, tag)
8// aead_open(key, nonce, aad, ciphertext, tag) -> (plaintext | FAIL)
9//
10// The AEAD construction derives a fresh Poly1305 key per message
11// from the first 32 bytes of ChaCha20(key, nonce, counter=0),
12// enforcing the one-time-key requirement from poly1305.nx P4.
13// Subsequent counter values (starting at 1) encrypt the payload.
14//
15// MAC input format (RFC 8439 ยง2.8.1):
16// aad || pad16(aad) || ct || pad16(ct) || len(aad) || len(ct)
17// where pad16 zero-pads to the next 16-byte boundary and the
18// length fields are u64-little-endian byte counts.
19//
20// Invariants:
21// A1 Poly1305 otk is derived freshly per (key, nonce) pair;
22// reusing a nonce with the same key collapses AEAD security.
23// Callers are responsible for nonce uniqueness.
24// A2 Tag verification uses ct_memcmp (constant-time) so failure
25// doesn't leak the position of the first mismatched byte.
26// A3 aead_open does NOT write plaintext when tag fails -- the
27// output buffer is left untouched so callers cannot process
28// partially-decrypted data.
29// A4 Every byte of ciphertext participates in the MAC, enforced
30// by the padding layout; no "length-extension" style attack.
31//
32// References:
33// RFC 8439 section 2.8 (AEAD construction)
34// RFC 8439 Appendix A.5 (full AEAD test vector)
35
36import "syscalls.nx"
37import "chacha20.nx"
38import "poly1305.nx"
39import "ct.nx"
40
41// Number of bytes to pad so length becomes a multiple of 16.
42func pad16_len(n: i64) -> i64 {
43 let rem: i64 = n & 15
44 if rem == 0 { return 0 }
45 return 16 - rem
46}
47
48// Write a u64 little-endian to buf[off..off+8].
49func store_u64_le(buf: *u8, off: i64, v: i64) -> i64 {
50 var i: i64 = 0
51 while i < 8 {
52 buf[off + i] = (v >> (i * 8)) & 0xFF
53 i = i + 1
54 }
55 return 0
56}
57
58// Build the MAC input into a caller-supplied buffer `mac_buf`.
59// Returns the number of bytes written. Buffer must be sized to
60// aad_len + pad16_len(aad_len) + ct_len + pad16_len(ct_len) + 16.
61func build_mac_input(mac_buf: *u8,
62 aad: *u8, aad_len: i64,
63 ct: *u8, ct_len: i64) -> i64 {
64 var pos: i64 = 0
65 var i: i64 = 0
66 while i < aad_len { mac_buf[pos + i] = aad[i]; i = i + 1 }
67 pos = pos + aad_len
68 let pa: i64 = pad16_len(aad_len)
69 i = 0
70 while i < pa { mac_buf[pos + i] = 0; i = i + 1 }
71 pos = pos + pa
72
73 i = 0
74 while i < ct_len { mac_buf[pos + i] = ct[i]; i = i + 1 }
75 pos = pos + ct_len
76 let pc: i64 = pad16_len(ct_len)
77 i = 0
78 while i < pc { mac_buf[pos + i] = 0; i = i + 1 }
79 pos = pos + pc
80
81 store_u64_le(mac_buf, pos, aad_len); pos = pos + 8
82 store_u64_le(mac_buf, pos, ct_len); pos = pos + 8
83 return pos
84}
85
86// Maximum AEAD message size supported in one call. Picked to fit
87// comfortably within a single mmap region plus padding. Larger
88// payloads should be chunked into record-layer messages (TLS does
89// this naturally at 16 KiB records).
90const AEAD_MAX_BYTES: i64 = 1048576 // 1 MiB
91
92// Encrypt + authenticate. Writes ciphertext to `ct` (same length
93// as pt) and 16-byte tag to `tag`. Caller owns all buffers.
94func aead_seal(key: *u8, nonce: *u8,
95 aad: *u8, aad_len: i64,
96 pt: *u8, pt_len: i64,
97 ct: *u8, tag: *u8) -> i64 {
98 // 1. Derive Poly1305 one-time key from ChaCha20 block 0.
99 let otk_full: *u8 = sys_mmap(64)
100 chacha20_block(key, 0, nonce, otk_full)
101 let otk: *u8 = otk_full // first 32 bytes are the Poly1305 key
102
103 // 2. Encrypt plaintext with counter starting at 1.
104 chacha20_encrypt(key, 1, nonce, pt, pt_len, ct)
105
106 // 3. Build MAC input and tag.
107 let mac_cap: i64 = aad_len + pad16_len(aad_len) + pt_len + pad16_len(pt_len) + 16
108 let mac_buf: *u8 = sys_mmap(mac_cap)
109 let mlen: i64 = build_mac_input(mac_buf, aad, aad_len, ct, pt_len)
110 poly1305_mac(otk, mac_buf, mlen, tag)
111 return 0
112}
113
114// Verify + decrypt. Returns 0 on success, -1 on tag mismatch.
115// On failure the output `pt` is not written (A3).
116func aead_open(key: *u8, nonce: *u8,
117 aad: *u8, aad_len: i64,
118 ct: *u8, ct_len: i64, tag: *u8,
119 pt: *u8) -> i64 {
120 // Re-derive otk.
121 let otk_full: *u8 = sys_mmap(64)
122 chacha20_block(key, 0, nonce, otk_full)
123 let otk: *u8 = otk_full
124
125 // Compute expected tag over the received ciphertext.
126 let mac_cap: i64 = aad_len + pad16_len(aad_len) + ct_len + pad16_len(ct_len) + 16
127 let mac_buf: *u8 = sys_mmap(mac_cap)
128 let mlen: i64 = build_mac_input(mac_buf, aad, aad_len, ct, ct_len)
129 let expected: *u8 = sys_mmap(16)
130 poly1305_mac(otk, mac_buf, mlen, expected)
131
132 // A2: constant-time tag compare; doesn't short-circuit.
133 if ct_memcmp(expected, tag, 16) != 1 {
134 return -1
135 }
136
137 // Tag valid -- decrypt. ChaCha20 is its own inverse.
138 chacha20_encrypt(key, 1, nonce, ct, ct_len, pt)
139 return 0
140}
141
142// Compile-only smoke: seal then open. Confirms the round-trip
143// types and linking; real KAT (RFC 8439 Appendix A.5) pending on
144// execution harness.
145func main() -> i64 {
146 let key: *u8 = sys_mmap(32)
147 let nonce: *u8 = sys_mmap(12)
148 let aad: *u8 = sys_mmap(16)
149 let pt: *u8 = sys_mmap(32)
150 let ct: *u8 = sys_mmap(32)
151 let tag: *u8 = sys_mmap(16)
152 let pt_out: *u8 = sys_mmap(32)
153
154 var i: i64 = 0
155 while i < 32 { key[i] = 0; i = i + 1 }
156 i = 0
157 while i < 12 { nonce[i] = 0; i = i + 1 }
158 i = 0
159 while i < 16 { aad[i] = 0; i = i + 1 }
160 i = 0
161 while i < 32 { pt[i] = (i as i64) & 0xFF; i = i + 1 }
162
163 aead_seal(key, nonce, aad, 16, pt, 32, ct, tag)
164 let rc: i64 = aead_open(key, nonce, aad, 16, ct, 32, tag, pt_out)
165 if rc != 0 { return 1 }
166 // Verify round-trip matches.
167 if ct_memcmp(pt, pt_out, 32) != 1 { return 2 }
168 return 0
169}