diff --git a/hosts/ocaml/bin/run_tests.ml b/hosts/ocaml/bin/run_tests.ml index ea4736c7..d7a57b58 100644 --- a/hosts/ocaml/bin/run_tests.ml +++ b/hosts/ocaml/bin/run_tests.ml @@ -1467,6 +1467,25 @@ let run_foundation_tests () = (Bool false) (call "ed25519-verify" [Integer 1; Integer 2; Integer 3]); + Printf.printf "\nSuite: rsa-sha256\n"; + (* Fixed RSA-2048 vector: one-off python-cryptography keygen + + PKCS1v15/SHA-256 sign of "fed-sx phase F rsa test". *) + let rhx = Sx_rsa.unhex in + let spki = rhx "30820122300d06092a864886f70d01010105000382010f003082010a0282010100a117b573480bce5a08b54a98384001df26d062e9173caaee2e3a2d0045c6d16f99b2a1e7fb60763f65f95f8c39ff82c18b8590338042914331db3440a06d2dbe65a2f82c82f37d293f67a8b57a1f9014b55150a093cfee90257ef3b4a215d5ab002579bd92b6fcb3536777d51b639347d01e307ddafb209073dd9b8d6a507157c44c624a19b3b9275931472462870ae02132630159132a85c1c889adfb358b6bbd3760ce3fffe6285964833a10ee436d5bc33dfab7f9ed630a74e9a32e5688f5a7797f7cc839ad2494dd1c4c4a8fab844cd26208794bf2602c16b9d12bde434066d8c0dd2d20489f4070f883bae2b4508ead4a1b80b44c576e9e37bdb5df69f10203010001" in + let rmsg = rhx "6665642d73782070686173652046207273612074657374" in + let rsig = rhx "5e1593d674ed15c0172546d38efdf1aebd252f4b0c0dfbe1f7996fd569d0bfd9f3e8689ea2b14aa45b5fc3f0a05d4f23c6b02b8820d71f6998ea3b5b0d071bb33142236e388b1226ece3ec447d33b38999f189c37564cf052cf038de94c67b2ddf9a97d5a73554bb88818f615824517209a4083258965adace55658f344104eaa0d5f2f44ea00cfac8754674aade87b40d955cccd1ccd9b7649a08b66ce3bc5dba2de96b3e859488ded3ef9fb3744a1e3495fd14841d8319b3cc08054c729d1c02739ee314eba2b20fac46e463f47eb67183d8455583eca73ba37448164612dd9cd77877135d30d12084c2843f986a5b8ad59c6600f9855b91d7cbdf7c6c4b0e" in + let rsav s m g = call "rsa-sha256-verify" [String s; String m; String g] in + assert_eq "rsa valid" (Bool true) (rsav spki rmsg rsig); + assert_eq "rsa tampered msg" (Bool false) + (rsav spki (rmsg ^ "x") rsig); + assert_eq "rsa tampered sig" (Bool false) + (rsav spki rmsg + (rhx "5f1593d674ed15c0172546d38efdf1aebd252f4b0c0dfbe1f7996fd569d0bfd9f3e8689ea2b14aa45b5fc3f0a05d4f23c6b02b8820d71f6998ea3b5b0d071bb33142236e388b1226ece3ec447d33b38999f189c37564cf052cf038de94c67b2ddf9a97d5a73554bb88818f615824517209a4083258965adace55658f344104eaa0d5f2f44ea00cfac8754674aade87b40d955cccd1ccd9b7649a08b66ce3bc5dba2de96b3e859488ded3ef9fb3744a1e3495fd14841d8319b3cc08054c729d1c02739ee314eba2b20fac46e463f47eb67183d8455583eca73ba37448164612dd9cd77877135d30d12084c2843f986a5b8ad59c6600f9855b91d7cbdf7c6c4b0e")); + assert_eq "rsa garbage spki" (Bool false) + (rsav "not der" rmsg rsig); + assert_eq "rsa non-string args" (Bool false) + (call "rsa-sha256-verify" [Integer 1; Integer 2; Integer 3]); + Printf.printf "\nSuite: vm-extension-dispatch\n"; let make_bc op = ({ vc_arity = 0; vc_rest_arity = -1; vc_locals = 0; diff --git a/hosts/ocaml/lib/sx_primitives.ml b/hosts/ocaml/lib/sx_primitives.ml index bf05f806..2eaea0d9 100644 --- a/hosts/ocaml/lib/sx_primitives.ml +++ b/hosts/ocaml/lib/sx_primitives.ml @@ -4209,4 +4209,10 @@ let () = | [String pk; String msg; String sg] -> Bool (try Sx_ed25519.verify ~pubkey:pk ~msg ~sig_:sg with _ -> false) + | _ -> Bool false); + + register "rsa-sha256-verify" (fun args -> + match args with + | [String spki; String msg; String sg] -> + Bool (try Sx_rsa.verify ~spki ~msg ~sig_:sg with _ -> false) | _ -> Bool false) diff --git a/hosts/ocaml/lib/sx_rsa.ml b/hosts/ocaml/lib/sx_rsa.ml new file mode 100644 index 00000000..a6bf5b90 --- /dev/null +++ b/hosts/ocaml/lib/sx_rsa.ml @@ -0,0 +1,220 @@ +(** RSASSA-PKCS1-v1_5 verification with SHA-256 — pure OCaml, + WASM-safe. Self-contained minimal bignum (modexp only), a tiny + DER reader for SubjectPublicKeyInfo, and the fixed SHA-256 + DigestInfo prefix. Verify only on public data — constant time + not required. Reference: RFC 8017 §8.2.2, §9.2. No deps. *) + +(* ---- Minimal unsigned bignum: int array, little-endian, base 2^26 ---- *) + +let bits = 26 +let base = 1 lsl bits +let mask = base - 1 + +type bn = int array + +let norm a = + let n = ref (Array.length a) in + while !n > 1 && a.(!n - 1) = 0 do decr n done; + if !n = Array.length a then a else Array.sub a 0 !n + +let bzero : bn = [| 0 |] +let is_zero a = Array.length a = 1 && a.(0) = 0 + +let cmp a b = + let a = norm a and b = norm b in + let la = Array.length a and lb = Array.length b in + if la <> lb then compare la lb + else begin + let r = ref 0 and i = ref (la - 1) in + while !r = 0 && !i >= 0 do + if a.(!i) <> b.(!i) then r := compare a.(!i) b.(!i); + decr i + done; !r + end + +let add a b = + let la = Array.length a and lb = Array.length b in + let n = (max la lb) + 1 in + let r = Array.make n 0 and carry = ref 0 in + for i = 0 to n - 1 do + let s = !carry + (if i < la then a.(i) else 0) + + (if i < lb then b.(i) else 0) in + r.(i) <- s land mask; carry := s lsr bits + done; + norm r + +let sub a b = (* requires a >= b *) + let la = Array.length a and lb = Array.length b in + let r = Array.make la 0 and borrow = ref 0 in + for i = 0 to la - 1 do + let s = a.(i) - !borrow - (if i < lb then b.(i) else 0) in + if s < 0 then (r.(i) <- s + base; borrow := 1) + else (r.(i) <- s; borrow := 0) + done; + norm r + +let mul a b = + let la = Array.length a and lb = Array.length b in + let r = Array.make (la + lb) 0 in + for i = 0 to la - 1 do + let carry = ref 0 in + for j = 0 to lb - 1 do + let s = r.(i + j) + a.(i) * b.(j) + !carry in + r.(i + j) <- s land mask; carry := s lsr bits + done; + r.(i + lb) <- r.(i + lb) + !carry + done; + norm r + +let numbits a = + let a = norm a in + let hi = Array.length a - 1 in + if hi = 0 && a.(0) = 0 then 0 + else begin + let b = ref 0 and v = ref a.(hi) in + while !v > 0 do incr b; v := !v lsr 1 done; + hi * bits + !b + end + +let bit a i = + let limb = i / bits and off = i mod bits in + if limb >= Array.length a then 0 else (a.(limb) lsr off) land 1 + +let bn_mod a m = (* binary long division, m > 0 *) + if cmp a m < 0 then norm a + else begin + let r = ref bzero in + for i = numbits a - 1 downto 0 do + r := add !r !r; + if bit a i = 1 then r := add !r [| 1 |]; + if cmp !r m >= 0 then r := sub !r m + done; + !r + end + +let powmod b0 e m = + let result = ref [| 1 |] and b = ref (bn_mod b0 m) in + for i = 0 to numbits e - 1 do + if bit e i = 1 then result := bn_mod (mul !result !b) m; + b := bn_mod (mul !b !b) m + done; + !result + +let of_bytes_be (s : string) : bn = + let acc = ref bzero in + for i = 0 to String.length s - 1 do + acc := add (mul !acc [| 256 |]) [| Char.code s.[i] |] + done; + !acc + +let div_small a d = + let la = Array.length a in + let q = Array.make la 0 and rem = ref 0 in + for i = la - 1 downto 0 do + let cur = (!rem lsl bits) lor a.(i) in + q.(i) <- cur / d; rem := cur mod d + done; + norm q + +let to_bytes_be (a : bn) (n : int) : string = + let b = Bytes.make n '\000' in + let cur = ref (norm a) in + for i = n - 1 downto 0 do + let q = div_small !cur 256 in + let r = + let d = sub !cur (mul q [| 256 |]) in + if is_zero d then 0 else d.(0) + in + Bytes.set b i (Char.chr r); + cur := q + done; + Bytes.unsafe_to_string b + +(* ---- Minimal DER reader (for SubjectPublicKeyInfo) ---- *) + +exception Der of string + +(* Returns (tag, content_start, content_len, next). *) +let der_tlv s pos = + if pos + 2 > String.length s then raise (Der "short"); + let tag = Char.code s.[pos] in + let l0 = Char.code s.[pos + 1] in + let len, hdr = + if l0 < 0x80 then l0, 2 + else begin + let nb = l0 land 0x7f in + if pos + 2 + nb > String.length s then raise (Der "short len"); + let v = ref 0 in + for i = 0 to nb - 1 do + v := (!v lsl 8) lor Char.code s.[pos + 2 + i] + done; + !v, 2 + nb + end + in + (tag, pos + hdr, len, pos + hdr + len) + +(* SPKI DER -> (n, e) as bignums. *) +let parse_spki (der : string) : bn * bn = + let tag, c, _l, _ = der_tlv der 0 in + if tag <> 0x30 then raise (Der "spki: outer not SEQUENCE"); + (* AlgorithmIdentifier SEQUENCE — skip. *) + let _, _, _, after_alg = der_tlv der c in + (* BIT STRING. *) + let bt, bc, bl, _ = der_tlv der after_alg in + if bt <> 0x03 then raise (Der "spki: expected BIT STRING"); + (* First content byte = unused bits (must be 0). *) + let rpk_start = bc + 1 in + ignore bl; + let st, sc, _, _ = der_tlv der rpk_start in + if st <> 0x30 then raise (Der "spki: RSAPublicKey not SEQUENCE"); + let nt, nc, nl, after_n = der_tlv der sc in + if nt <> 0x02 then raise (Der "spki: modulus not INTEGER"); + let et, ec, el, _ = der_tlv der after_n in + if et <> 0x02 then raise (Der "spki: exponent not INTEGER"); + let n = of_bytes_be (String.sub der nc nl) in + let e = of_bytes_be (String.sub der ec el) in + (n, e) + +(* SHA-256 DigestInfo DER prefix (RFC 8017 §9.2 note 1). *) +let sha256_digestinfo_prefix = + "\x30\x31\x30\x0d\x06\x09\x60\x86\x48\x01\x65\x03\x04\x02\x01\x05\x00\x04\x20" + +let unhex h = + let n = String.length h / 2 in + let b = Bytes.create n in + for i = 0 to n - 1 do + Bytes.set b i (Char.chr (int_of_string ("0x" ^ String.sub h (2 * i) 2))) + done; + Bytes.unsafe_to_string b + +(* RSASSA-PKCS1-v1_5 verify with SHA-256. Total: any malformed + input yields false (caller wraps, but be defensive here too). *) +let verify ~spki ~msg ~sig_ : bool = + try + let n, e = parse_spki spki in + let k = (numbits n + 7) / 8 in + if String.length sig_ <> k then false + else begin + let s = of_bytes_be sig_ in + if cmp s n >= 0 then false + else begin + let m = powmod s e n in + let em = to_bytes_be m k in + (* EM = 0x00 01 FF..FF 00 || DigestInfo || H *) + let h = unhex (Sx_sha2.sha256_hex msg) in + let t = sha256_digestinfo_prefix ^ h in + let tlen = String.length t in + if k < tlen + 11 then false + else begin + let ok = ref (em.[0] = '\x00' && em.[1] = '\x01') in + let ps_end = k - tlen - 1 in + for i = 2 to ps_end - 1 do + if em.[i] <> '\xff' then ok := false + done; + if em.[ps_end] <> '\x00' then ok := false; + if String.sub em (ps_end + 1) tlen <> t then ok := false; + !ok + end + end + end + with _ -> false diff --git a/plans/fed-sx-host-primitives.md b/plans/fed-sx-host-primitives.md index 04fe6d5e..6e912649 100644 --- a/plans/fed-sx-host-primitives.md +++ b/plans/fed-sx-host-primitives.md @@ -115,7 +115,7 @@ check** → tests → commit → tick box → Progress-log line → push. - **Acceptance:** all RFC 8032 vectors pass; WASM links. Satisfies fed-sx Step 2 (Ed25519 sig-suite). -### Phase F — RSA-SHA256 verify (PKCS#1 v1.5), pure OCaml +### Phase F — RSA-SHA256 verify (PKCS#1 v1.5), pure OCaml ✅ DONE - Minimal pure-OCaml bignum (only need modexp + DER parse). Parse SPKI DER → (n, e). RSASSA-PKCS1-v1_5 verify with SHA-256 (Phase A). - Primitive `rsa-sha256-verify (der-spki msg sig) -> bool`. @@ -205,6 +205,14 @@ printf '(epoch 1)\n(crypto-sha256 "abc")\n' | \ _Newest first._ +- 2026-05-18 — Phase F: pure-OCaml `lib/sx_rsa.ml` (self-contained + bignum modexp, minimal DER SPKI reader, RFC 8017 §8.2.2 PKCS#1 + v1.5 verify with SHA-256 DigestInfo prefix). Primitive + `rsa-sha256-verify` total. 5 tests on a fixed RSA-2048 vector + (one-off python-cryptography keygen, hardcoded): valid, tampered + msg/sig, garbage SPKI, non-string. WASM boot green with new lib + module; Erlang 530/530; run_tests +5. Satisfies fed-sx Step 2 + (rsa-sha256-2018 sig-suite). - 2026-05-18 — Phase E: pure-OCaml `lib/sx_ed25519.ml` (minimal base-2^26 bignum, edwards25519 extended-coord points, RFC 8032 §5.1.7 cofactorless verify reusing Phase-A sha512). Primitive