typed/crypto: SHA-256/HMAC/HKDF kernels via FFI to RustCrypto
Jaime Fournier <jaimef@linbsd.org>
f27ff8debf377b3f645dea0e97beb0efbe0179f4
diff --git a/tests/crypto_vectors.rs b/tests/crypto_vectors.rs
new file mode 100644
index 0000000..6a2ed90
--- /dev/null
+++ b/tests/crypto_vectors.rs
@@ -0,0 +1,69 @@
+//! Known-answer vectors for the crypto kernels (jsecmon/typed/crypto.ss),
+//! which lower to FFI calls into the vetted RustCrypto crates. We pin standard
+//! published vectors so the typed→Rust crypto-prim lowering is checked against
+//! an external authority, not against itself:
+//!
+//! SHA-256 FIPS 180-4 examples ("", "abc")
+//! HMAC-SHA256 RFC 4231 Test Case 2
+//! HKDF-SHA256 RFC 5869 Test Cases 1 and 3 (TC3 = empty salt == None)
+//!
+//! This is what proves the kernels are real crypto and that an empty salt
+//! reproduces HKDF's "salt not provided" path that secmon's PSK relies on.
+
+use jerboa_typed_generated::jsecmon_typed_crypto::{
+ hkdf_sha256_derive, hmac_sha256_tag, sha256_digest,
+};
+
+fn hex(s: &str) -> Vec<u8> {
+ (0..s.len())
+ .step_by(2)
+ .map(|i| u8::from_str_radix(&s[i..i + 2], 16).unwrap())
+ .collect()
+}
+
+#[test]
+fn sha256_fips180_4_vectors() {
+ assert_eq!(
+ sha256_digest(b"".to_vec()),
+ hex("e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855")
+ );
+ assert_eq!(
+ sha256_digest(b"abc".to_vec()),
+ hex("ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad")
+ );
+}
+
+#[test]
+fn hmac_sha256_rfc4231_tc2() {
+ // key = "Jefe", msg = "what do ya want for nothing?"
+ let tag = hmac_sha256_tag(b"Jefe".to_vec(), b"what do ya want for nothing?".to_vec());
+ assert_eq!(
+ tag,
+ hex("5bdcc146bf60754e6a042426089575c75a003f089d2739839dec58b964ec3843")
+ );
+}
+
+#[test]
+fn hkdf_sha256_rfc5869_tc1() {
+ let ikm = vec![0x0b; 22];
+ let salt = hex("000102030405060708090a0b0c");
+ let info = hex("f0f1f2f3f4f5f6f7f8f9");
+ let okm = hkdf_sha256_derive(salt, ikm, info, 42);
+ assert_eq!(
+ okm,
+ hex("3cb25f25faacd57a90434f64d0362f2a2d2d0a90cf1a5a4c5db02d56ecc4c5bf34007208d5b887185865")
+ );
+}
+
+#[test]
+fn hkdf_sha256_rfc5869_tc3_empty_salt_is_none() {
+ // TC3 uses zero-length salt and info; the RFC computes it with "salt not
+ // provided", so matching it proves the kernel's Some(empty) == HKDF None —
+ // exactly what secmon's psk from_bytes (no salt) depends on.
+ let ikm = vec![0x0b; 22];
+ let okm = hkdf_sha256_derive(Vec::new(), ikm, Vec::new(), 42);
+ assert_eq!(
+ okm,
+ hex("8da4e775a563c18f715f802a063c5a31b8a11f5c5ee1879ec3454e5f3c738d2d9d201395faa4b61a96c8")
+ );
+}
diff --git a/typed/crypto.ss b/typed/crypto.ss
new file mode 100644
index 0000000..8ed5b3d
--- /dev/null
+++ b/typed/crypto.ss
@@ -0,0 +1,34 @@
+;;; jsecmon — established crypto primitives, in Typed Jerboa, lowered to FFI
+;;; calls into the vetted RustCrypto crates (sha2 / hmac / hkdf). We never
+;;; reimplement a hash or a KDF: each kernel is a thin typed wrapper whose body
+;;; is a single crypto-prim the typed→Rust backend turns into a `sha2::Sha256`,
+;;; `hmac::Hmac::<Sha256>`, or `hkdf::Hkdf::<Sha256>` call.
+;;;
+;;; These are the deterministic building blocks secmon's PSK auth and ECIES use
+;;; (src/crypto/psk.rs derives auth/transport keys with HKDF-SHA256 and proves a
+;;; challenge with SHA256). Putting them here lets the surrounding pure Jerboa
+;;; call vetted crypto across the FFI boundary without rolling its own.
+;;;
+;;; sha256-digest SHA-256 (psk compute_proof)
+;;; hmac-sha256-tag HMAC-SHA256 (MAC / PRF building block)
+;;; hkdf-sha256-derive HKDF-SHA256 extract+expand (psk from_bytes key split)
+;;;
+;;; hkdf-sha256-derive takes an explicit salt; passing an empty salt reproduces
+;;; RFC 5869's "salt not provided" (None) case exactly — verified against RFC
+;;; 5869 Test Case 3 in tests/crypto_vectors.rs — which is what psk uses.
+
+(typed-library (jsecmon typed crypto)
+ (export sha256-digest hmac-sha256-tag hkdf-sha256-derive)
+
+ ;; SHA-256 of an arbitrary byte string → 32-byte digest.
+ (def (sha256-digest (data : Bytes)) : Bytes
+ (sha256 data))
+
+ ;; HMAC-SHA256 under `key` over `msg` → 32-byte tag. Any key length is fine.
+ (def (hmac-sha256-tag (key : Bytes) (msg : Bytes)) : Bytes
+ (hmac-sha256 key msg))
+
+ ;; HKDF-SHA256 (extract-then-expand): derive `length` bytes of output keying
+ ;; material from `ikm` under `salt` and context `info`. Empty salt == None.
+ (def (hkdf-sha256-derive (salt : Bytes) (ikm : Bytes) (info : Bytes) (length : Nat)) : Bytes
+ (hkdf-sha256 salt ikm info length)))