nx_aead.nx source
↩ module page · 197 lines · 7573 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//
36// license_tier: INDEPENDENT_REDERIVE
37// genealogy_id: international-research-sources/ietf/rfc_8439
38//
39// nx_safety_envelope:
40// intended_use: "AEAD construction (ChaCha20-Poly1305 +
41// AES-GCM forthcoming) -- TLS 1.3 record
42// protection + general authenticated encryption"
43// sil_target: SIL3 (combined confidentiality + integrity
44// primitive; failure of EITHER axis
45// = full break)
46// asil_target: QM
47// dal_target: DAL B
48// iec_62304_class: B
49// evidence: [no_FP, sealed_verdict,
50// RFC_8439_test_vectors_VERIFIED,
51// inherits_nx_chacha20_constant_time_evidence,
52// Poly1305_authenticator_constant_time]
53// hazard_register: [bug-tape-nonce-reuse-CATASTROPHIC-disclose,
54// bug-tape-AAD-truncation-via-bad-length,
55// bug-tape-tag-comparison-non-constant-time]
56// residual_risk: "Nonce-reuse with AEAD is the SINGLE MOST
57// CATASTROPHIC failure mode in modern crypto
58// (Joux 2006 forbidden attack on AES-GCM).
59// Caller MUST guarantee 96-bit nonce uniqueness
60// per key. Substrate cannot enforce; documented
61// front-and-center."
62// verdict: NOT_YET_EVALUATED
63
64import "nx_syscalls.nx"
65import "nx_chacha20.nx"
66import "nx_poly1305.nx"
67import "nx_ct.nx"
68
69// Number of bytes to pad so length becomes a multiple of 16.
70func pad16_len(n: i64) -> i64 {
71 let rem: i64 = n & 15
72 if rem == 0 { return 0 }
73 return 16 - rem
74}
75
76// Write a u64 little-endian to buf[off..off+8].
77func store_u64_le(buf: *u8, off: i64, v: i64) -> i64 {
78 var i: i64 = 0
79 while i < 8 {
80 buf[off + i] = (v >> (i * 8)) & 0xFF
81 i = i + 1
82 }
83 return 0
84}
85
86// Build the MAC input into a caller-supplied buffer `mac_buf`.
87// Returns the number of bytes written. Buffer must be sized to
88// aad_len + pad16_len(aad_len) + ct_len + pad16_len(ct_len) + 16.
89func build_mac_input(mac_buf: *u8,
90 aad: *u8, aad_len: i64,
91 ct: *u8, ct_len: i64) -> i64 {
92 var pos: i64 = 0
93 var i: i64 = 0
94 while i < aad_len { mac_buf[pos + i] = aad[i]; i = i + 1 }
95 pos = pos + aad_len
96 let pa: i64 = pad16_len(aad_len)
97 i = 0
98 while i < pa { mac_buf[pos + i] = 0; i = i + 1 }
99 pos = pos + pa
100
101 i = 0
102 while i < ct_len { mac_buf[pos + i] = ct[i]; i = i + 1 }
103 pos = pos + ct_len
104 let pc: i64 = pad16_len(ct_len)
105 i = 0
106 while i < pc { mac_buf[pos + i] = 0; i = i + 1 }
107 pos = pos + pc
108
109 store_u64_le(mac_buf, pos, aad_len); pos = pos + 8
110 store_u64_le(mac_buf, pos, ct_len); pos = pos + 8
111 return pos
112}
113
114// Maximum AEAD message size supported in one call. Picked to fit
115// comfortably within a single mmap region plus padding. Larger
116// payloads should be chunked into record-layer messages (TLS does
117// this naturally at 16 KiB records).
118const AEAD_MAX_BYTES: i64 = 1048576 // 1 MiB
119
120// Encrypt + authenticate. Writes ciphertext to `ct` (same length
121// as pt) and 16-byte tag to `tag`. Caller owns all buffers.
122func aead_seal(key: *u8, nonce: *u8,
123 aad: *u8, aad_len: i64,
124 pt: *u8, pt_len: i64,
125 ct: *u8, tag: *u8) -> i64 {
126 // 1. Derive Poly1305 one-time key from ChaCha20 block 0.
127 let otk_full: *u8 = sys_mmap(64)
128 chacha20_block(key, 0, nonce, otk_full)
129 let otk: *u8 = otk_full // first 32 bytes are the Poly1305 key
130
131 // 2. Encrypt plaintext with counter starting at 1.
132 chacha20_encrypt(key, 1, nonce, pt, pt_len, ct)
133
134 // 3. Build MAC input and tag.
135 let mac_cap: i64 = aad_len + pad16_len(aad_len) + pt_len + pad16_len(pt_len) + 16
136 let mac_buf: *u8 = sys_mmap(mac_cap)
137 let mlen: i64 = build_mac_input(mac_buf, aad, aad_len, ct, pt_len)
138 poly1305_mac(otk, mac_buf, mlen, tag)
139 return 0
140}
141
142// Verify + decrypt. Returns 0 on success, -1 on tag mismatch.
143// On failure the output `pt` is not written (A3).
144func aead_open(key: *u8, nonce: *u8,
145 aad: *u8, aad_len: i64,
146 ct: *u8, ct_len: i64, tag: *u8,
147 pt: *u8) -> i64 {
148 // Re-derive otk.
149 let otk_full: *u8 = sys_mmap(64)
150 chacha20_block(key, 0, nonce, otk_full)
151 let otk: *u8 = otk_full
152
153 // Compute expected tag over the received ciphertext.
154 let mac_cap: i64 = aad_len + pad16_len(aad_len) + ct_len + pad16_len(ct_len) + 16
155 let mac_buf: *u8 = sys_mmap(mac_cap)
156 let mlen: i64 = build_mac_input(mac_buf, aad, aad_len, ct, ct_len)
157 let expected: *u8 = sys_mmap(16)
158 poly1305_mac(otk, mac_buf, mlen, expected)
159
160 // A2: constant-time tag compare; doesn't short-circuit.
161 if ct_memcmp(expected, tag, 16) != 1 {
162 return -1
163 }
164
165 // Tag valid -- decrypt. ChaCha20 is its own inverse.
166 chacha20_encrypt(key, 1, nonce, ct, ct_len, pt)
167 return 0
168}
169
170// Compile-only smoke: seal then open. Confirms the round-trip
171// types and linking; real KAT (RFC 8439 Appendix A.5) pending on
172// execution harness.
173func main() -> i64 {
174 let key: *u8 = sys_mmap(32)
175 let nonce: *u8 = sys_mmap(12)
176 let aad: *u8 = sys_mmap(16)
177 let pt: *u8 = sys_mmap(32)
178 let ct: *u8 = sys_mmap(32)
179 let tag: *u8 = sys_mmap(16)
180 let pt_out: *u8 = sys_mmap(32)
181
182 var i: i64 = 0
183 while i < 32 { key[i] = 0; i = i + 1 }
184 i = 0
185 while i < 12 { nonce[i] = 0; i = i + 1 }
186 i = 0
187 while i < 16 { aad[i] = 0; i = i + 1 }
188 i = 0
189 while i < 32 { pt[i] = (i as i64) & 0xFF; i = i + 1 }
190
191 aead_seal(key, nonce, aad, 16, pt, 32, ct, tag)
192 let rc: i64 = aead_open(key, nonce, aad, 16, ct, 32, tag, pt_out)
193 if rc != 0 { return 1 }
194 // Verify round-trip matches.
195 if ct_memcmp(pt, pt_out, 32) != 1 { return 2 }
196 return 0
197}