mirror of
https://github.com/ratspeak/C6-Reticulum-ASM
synced 2026-08-12 18:07:18 -04:00
56cddf1193
Cryptol modules compose vertically: HMACSHA256 layers RFC 2104
HMAC-SHA-256 over the verified SHA256Final.sha256_oneshot; HKDFSHA256
layers RFC 5869 Extract/Expand over HMACSHA256.
SAW drivers discharge:
* hmac_sha256: algebraic identities (ipad^opad=0x6a, xor_with
involution, in-place key flip), RFC 4231 TC1/TC2/TC3/TC6 (TC6
exercises the long-key SHA-256(K) path).
* hkdf_extract: RFC 5869 A.1/A.2/A.3 PRK vectors (A.2 long-salt
HMAC path; A.3 zero-salt substitution).
* hkdf_expand: RFC 5869 A.1/A.3 OKM vectors (42 bytes = 2 T-blocks).
angr verifiers cross-check the RV32 binary against Python oracles:
* hmac_sha256: 9 vectors (RFC 4231 TC1/2/3/4/6/7 + 64-byte boundary
+ random + empty/empty), match `hmac.new(k, m, hashlib.sha256)`.
* hkdf_extract: 4 vectors covering all three salt-length regimes.
* hkdf_expand: 7 vectors (RFC 5869 A.1/A.2/A.3 + 32/64/96-byte
OKM lengths + max info length 223), match an in-script RFC 5869
reference oracle.
verify.py: build CRYPTOLPATH from absolute proofs/<module>/* dirs so
cross-module imports (e.g. HMACSHA256 importing SHA256Final) resolve
without requiring the user to set CRYPTOLPATH manually.
End-to-end ./verify per function:
hmac_sha256: ~38 s (9 angr scenarios, each = 2 SHA-256 invocations)
hkdf_extract: ~19 s
hkdf_expand: ~53 s (8 T-blocks max in scenarios)
FUNCTIONS.md: 3 entries flip ◑ → ◉. Verified: 29 → 32.
Milestone-2 frontier next item is the AES-256-CBC stack (15 functions).
|
||
|---|---|---|
| .. | ||
| hmac_sha256.py | ||
| hmac_sha256.saw | ||
| HMACSHA256.cry | ||