cryspen / libcrux

The formally verified crypto library for Rust
https://cryspen.com/libcrux
Apache License 2.0
86 stars 14 forks source link

ML-KEM cg/ extraction broken on big-endian systems #643

Open djmdjm opened 5 days ago

djmdjm commented 5 days ago

The libcrux-ml-kem/cg extraction is broken on big-endian systems. The root cause seems to be these functions in eurydice_glue.h:

static inline void core_num__u64_9__to_le_bytes(uint64_t v, uint8_t buf[8]) {
  memcpy(buf, &v, sizeof(v));
}
static inline uint64_t core_num__u64_9__from_le_bytes(uint8_t buf[8]) {
  uint64_t v;
  memcpy(&v, buf, sizeof(v));
  return v;
}

static inline uint32_t core_num__u32_8__from_le_bytes(uint8_t buf[4]) {
  uint32_t v;
  memcpy(&v, buf, sizeof(v));
  return v;
}

which don't do any byte-swapping. We just fixed them in OpenSSH using endian.h macros: https://github.com/openssh/openssh-portable/commit/cf3e48ee8ba1beeccddd2f203b558fa102be67a2#diff-36ddc54729ced4a7ff0c5351a9fa6db5229d806a9268fc33f10c61d6cef9811e but it would be nice for them to be fixed upstream.

jonathangray commented 5 days ago

https://github.com/AeneasVerif/eurydice/blob/dcfae68c874635956f71d4c05928841b29ad0a8b/include/eurydice_glue.h#L132 has byte swapping.

karthikbhargavan commented 3 days ago

Thanks for the report and good catch! The C code here has mainly been tested on Arm64 and X64/AVX2. We do indeed have the endian conversions code elsewhere, we will either integrate it here, or document how to use the current code safely on big-endian systems.

franziskuskiefer commented 1 day ago

Thanks for the report @djmdjm. We minimised the glue here and apparently went a little too far. We'll get this fixed. But I want to have a big endian CPU on CI as well to make sure this doesn't happen again.

djmdjm commented 1 day ago

Yes, we've faced the CI problem too - BE architectures are not very common these days. We're looking at using FreeBSD/ppc64 on qemu