zupt/AUDIT.md

Security Audit — Zupt v1.5.0

Date: March 28, 2026 Author: Cristian Cezar Moisés Audit type: Self-audit with formal verification (Jasmin) and NIST/RFC test vectors Status: No independent third-party audit performed

---

1. Cryptographic Test Vector Verification

All primitives tested against published reference vectors:

Primitive	Standard	Vectors	Status
SHA-256	FIPS 180-4	3 (empty, "abc", 448-bit)	PASS
HMAC-SHA256	RFC 4231	2 (TC2: "Jefe", TC3: 20×0xAA)	PASS
SHA3-256	FIPS 202	2 (empty, "abc")	PASS
SHAKE-128	FIPS 202	1 (empty, 128-bit output)	PASS
X25519	RFC 7748 §5.2	2 (both test vectors)	PASS
ML-KEM-768	FIPS 203	2 (5-trial roundtrip + implicit rejection)	PASS
XXH64	xxHash spec	1 (empty string, seed=0)	PASS
Total		13	13/13 PASS

Reproduction: make test-vectors && ./test_vectors

---

2. Functional Test Results

Suite	Tests	Result	What It Covers
Regression	16	16/16 PASS	All codecs, modes, encryption, edge cases, corruption detection
Multi-threaded	14	14/14 PASS	N=1/2/4/8 threads, large files, 1000 files, MT+encryption
Post-quantum	10	10/10 PASS	Keygen, PQ encrypt/decrypt, wrong key, password compat, PQ+MT, 2MB
Quick smoke	9	9/9 PASS	Normal, solid, encrypted, wrong pw, MT, fast, store, PQ, integrity
NIST vectors	13	13/13 PASS	See table above
Total	62	62/62 PASS

Reproduction: make test-all

---

3. Memory Safety

Tool	Command	Result
AddressSanitizer	make test-asan	Zero errors
UndefinedBehaviorSanitizer	Built with -fsanitize=address,undefined	Zero errors
All code paths tested	Normal + solid + encrypted + PQ + MT	Clean

Reproduction:

make test-asan
./zupt_asan compress /tmp/t.zupt /path/to/data/
./zupt_asan extract -o /tmp/out/ /tmp/t.zupt
./zupt_asan keygen -o /tmp/k.key
./zupt_asan compress --pq /tmp/pub.key /tmp/pq.zupt /path/to/data/
./zupt_asan extract --pq /tmp/k.key -o /tmp/pqout/ /tmp/pq.zupt

---

4. Compiler Warning Audit

Compiler	Flags	Warnings
GCC 13.x	-Wall -Wextra -Wpedantic -O2 -std=c11	Zero
Clang 18.x	-Wall -Wextra -Wpedantic -O2 -std=c11	Zero

---

5. Constant-Time Analysis

Function	Location	CT Method	Jasmin Verified?	Risk Level
HMAC comparison	zupt_crypto.c:252	4×u64 XOR accumulation	Yes — zupt_mac_verify_ct linked	None (Jasmin proven)
ML-KEM FO select	zupt_mlkem.c:593	4×u64 masked select	Yes — zupt_ct_select_32 linked	None (Jasmin proven)
ML-KEM NTT butterfly	zupt_mlkem.c	Montgomery reduction (branchless)	No	Low
ML-KEM CBD sampling	zupt_mlkem.c	Bitwise operations only	No	Low
X25519 fe_cswap	zupt_x25519.c:95	Masked XOR swap	No (limb mismatch)	Low (C is branchless)
X25519 Montgomery ladder	zupt_x25519.c:243	Fixed 255 iterations	No	Low
AES-256 encrypt	zupt_aes256.c:59	Table-based S-box	No	HIGH on shared HW
SHA-256	zupt_sha256.c	Table-based constants	No	Low (not secret-indexed)
Keccak-f[1600]	zupt_keccak.c	Bitwise XOR/ROT only	No	None
Key wipe	zupt_crypto.c	explicit_bzero / volatile	No	Low

Jasmin Assembly Verification

Two functions confirmed active in binary via nm:

0000000000014ae0 T zupt_mac_verify_ct    ← Jasmin assembly, CT proven
0000000000014b20 T zupt_ct_select_32     ← Jasmin assembly, CT proven

Assembly generated by jasminc 2026.03.0. Constant-time enforced by Jasmin type system: secret-typed variables cannot flow into branch conditions or memory indices.

Not Wired (with reason)

Function	Issue	Fallback
zupt_fe_cswap	Jasmin: 4×u64 limbs, C: 5×u51 — incompatible	C masked XOR (branchless)
zupt_aes256_blk	Stack offset bug: rk.[1] → [rsp+1] not [rsp+16]	C table-based AES

---

6. Key Material Lifecycle

Phase	Method	Verified
Generation	OS CSPRNG: getrandom(2) / /dev/urandom / RtlGenRandom	Hard fail if unavailable
Storage	Stack-local arrays (no heap allocation for keys)	ASAN verified
Usage	Passed by const pointer to AES-CTR / HMAC	No copies to heap
Wipe	zupt_secure_wipe(): explicit_bzero (glibc 2.25+), SecureZeroMemory (Win), volatile fallback	Compiler cannot optimize out
Scope exit	Stack frame destroyed	Keys were on stack

All intermediate buffers in PBKDF2, hybrid KEM, ML-KEM encaps/decaps, and X25519 wiped before return.

---

7. Nonce Security

Scheme: per_block_nonce = base_nonce XOR pad_le(block_seq, 8)

• base_nonce: 128-bit random from CSPRNG, generated once per archive.
• block_seq: monotonically increasing 0, 1, 2, ... per archive.
• Uniqueness within archive: Guaranteed (distinct seq → distinct nonce).
• Uniqueness across archives: 2^-128 collision probability per pair (birthday bound on random base).

---

8. Encrypt-then-MAC Ordering

Step	Action	Verified
1	Compute HMAC over nonce ‖ ciphertext	HMAC input is nonce+ct, not plaintext
2	Verify HMAC before any decryption	Code path: MAC check → early return if fail → decrypt only on success
3	Decrypt only authenticated data	No plaintext produced from unauthenticated ciphertext

Prevents: Chosen-ciphertext attacks, padding oracles, ciphertext tampering.

---

9. Bugs Found and Fixed (v0.5.1 → v1.5.0)

Bug	Severity	Version Fixed	Impact
Huffman Kraft-inequality violation	Critical	v0.5.1	Data corruption on specific inputs
Heap-buffer-overflow in LZ match finder	Critical	v0.5.1	Potential code execution
rand() CSPRNG fallback	Critical	v0.5.1	Predictable encryption keys
ML-KEM poly_basemul OOB	Critical	v1.0.0	Buffer overread in NTT
ML-KEM missing poly_tomont	Critical	v1.0.0	Public key in wrong domain
ML-KEM inverted FO cmov	Critical	v1.0.0	Always selected rejection key
ML-KEM inv_ntt wrong table	High	v1.0.0	NTT roundtrip failure
PQ nonce mismatch	High	v1.0.0	Encrypt/decrypt used different nonces
X25519 AA + a24*E formula	High	v1.1.0	Wrong curve, not interoperable
Dead match_cost()	Low	v1.1.0	Clang warning
const polyvec qualifier	Low	v1.1.0	Pedantic warnings
__int128 pedantic	Low	v1.1.0	Pedantic warning

---

10. Known Limitations

Limitation	Impact	Mitigation	Status
Table-based AES (C fallback)	Cache-timing on shared hardware	Jasmin AES-NI path exists but has offset bug	Open — fix .jazz source
Table-based SHA-256	Theoretical cache-timing	Not used on secret-indexed data	Accepted
PBKDF2 not quantum-safe	Quantum password brute-force	Use --pq mode	Documented
No mlock()	Keys swappable to disk	Short key lifetime + zupt_secure_wipe	Planned
No fuzzing performed	Undiscovered bugs	AFL++ setup in FUZZING.md	Planned
No independent audit	Self-assessed only	Open source + Jasmin proofs	Planned
X25519 Jasmin not linked	C fallback for fe_cswap	C is branchless but compiler-dependent	Open — limb mismatch

---

© 2026 Cristian Cezar Moisés — MIT License