Merge pull request #703 from cryspen/keks/more-hacl-rs

Clean up Hacl-rs integration and add Poly1305 and ChaCha20Poly1305

Cargo.toml

@@ -23,6 +23,9 @@ members = [
     "sha2",
     "ed25519",
     "curve25519",
+    "poly1305",
+    "chacha20poly1305",
+    "rsa",
 ]
 
 [workspace.package]

chacha20poly1305/Cargo.toml

@@ -0,0 +1,23 @@
+[package]
+name = "libcrux-chacha20poly1305"
+description = "Formally verified ChaCha20-Poly1305 AEAD library"
+
+version.workspace = true
+authors.workspace = true
+license.workspace = true
+homepage.workspace = true
+edition.workspace = true
+repository.workspace = true
+readme.workspace = true
+
+[dependencies]
+libcrux-poly1305 = { version = "=0.0.2-beta.2", path = "../poly1305/", features = [
+    "expose-hacl",
+] }
+libcrux-hacl-rs = { version = "=0.0.2-beta.2", path = "../hacl-rs/" }
+libcrux-macros = { version = "=0.0.2-beta.2", path = "../macros" }
+
+[dev-dependencies]
+hex = { version = "0.4.3", features = ["serde"] }
+serde = { version = "1.0.216", features = ["derive"] }
+serde_json = "1.0.133"

chacha20poly1305/src/hacl/chacha20.rs

@@ -0,0 +1,191 @@
+#![allow(non_snake_case)]
+#![allow(non_upper_case_globals)]
+#![allow(non_camel_case_types)]
+#![allow(unused_assignments)]
+#![allow(unreachable_patterns)]
+
+//! This module contains generated hacl code.
+
+use libcrux_hacl_rs::prelude::*;
+use libcrux_macros as krml;
+
+pub(crate) const chacha20_constants: [u32; 4] =
+    [0x61707865u32, 0x3320646eu32, 0x79622d32u32, 0x6b206574u32];
+
+#[inline]
+fn quarter_round(st: &mut [u32], a: u32, b: u32, c: u32, d: u32) {
+    let sta: u32 = st[a as usize];
+    let stb: u32 = st[b as usize];
+    let std: u32 = st[d as usize];
+    let sta1: u32 = sta.wrapping_add(stb);
+    let std1: u32 = std ^ sta1;
+    let std2: u32 = std1.wrapping_shl(16u32) | std1.wrapping_shr(16u32);
+    st[a as usize] = sta1;
+    st[d as usize] = std2;
+    let sta0: u32 = st[c as usize];
+    let stb0: u32 = st[d as usize];
+    let std0: u32 = st[b as usize];
+    let sta10: u32 = sta0.wrapping_add(stb0);
+    let std10: u32 = std0 ^ sta10;
+    let std20: u32 = std10.wrapping_shl(12u32) | std10.wrapping_shr(20u32);
+    st[c as usize] = sta10;
+    st[b as usize] = std20;
+    let sta2: u32 = st[a as usize];
+    let stb1: u32 = st[b as usize];
+    let std3: u32 = st[d as usize];
+    let sta11: u32 = sta2.wrapping_add(stb1);
+    let std11: u32 = std3 ^ sta11;
+    let std21: u32 = std11.wrapping_shl(8u32) | std11.wrapping_shr(24u32);
+    st[a as usize] = sta11;
+    st[d as usize] = std21;
+    let sta3: u32 = st[c as usize];
+    let stb2: u32 = st[d as usize];
+    let std4: u32 = st[b as usize];
+    let sta12: u32 = sta3.wrapping_add(stb2);
+    let std12: u32 = std4 ^ sta12;
+    let std22: u32 = std12.wrapping_shl(7u32) | std12.wrapping_shr(25u32);
+    st[c as usize] = sta12;
+    st[b as usize] = std22
+}
+
+#[inline]
+fn double_round(st: &mut [u32]) {
+    crate::hacl::chacha20::quarter_round(st, 0u32, 4u32, 8u32, 12u32);
+    crate::hacl::chacha20::quarter_round(st, 1u32, 5u32, 9u32, 13u32);
+    crate::hacl::chacha20::quarter_round(st, 2u32, 6u32, 10u32, 14u32);
+    crate::hacl::chacha20::quarter_round(st, 3u32, 7u32, 11u32, 15u32);
+    crate::hacl::chacha20::quarter_round(st, 0u32, 5u32, 10u32, 15u32);
+    crate::hacl::chacha20::quarter_round(st, 1u32, 6u32, 11u32, 12u32);
+    crate::hacl::chacha20::quarter_round(st, 2u32, 7u32, 8u32, 13u32);
+    crate::hacl::chacha20::quarter_round(st, 3u32, 4u32, 9u32, 14u32)
+}
+
+#[inline]
+fn rounds(st: &mut [u32]) {
+    crate::hacl::chacha20::double_round(st);
+    crate::hacl::chacha20::double_round(st);
+    crate::hacl::chacha20::double_round(st);
+    crate::hacl::chacha20::double_round(st);
+    crate::hacl::chacha20::double_round(st);
+    crate::hacl::chacha20::double_round(st);
+    crate::hacl::chacha20::double_round(st);
+    crate::hacl::chacha20::double_round(st);
+    crate::hacl::chacha20::double_round(st);
+    crate::hacl::chacha20::double_round(st)
+}
+
+#[inline]
+fn chacha20_core(k: &mut [u32], ctx: &[u32], ctr: u32) {
+    (k[0usize..16usize]).copy_from_slice(&ctx[0usize..16usize]);
+    let ctr_u32: u32 = ctr;
+    k[12usize] = (k[12usize]).wrapping_add(ctr_u32);
+    crate::hacl::chacha20::rounds(k);
+    krml::unroll_for!(16, "i", 0u32, 1u32, {
+        let x: u32 = (k[i as usize]).wrapping_add(ctx[i as usize]);
+        let os: (&mut [u32], &mut [u32]) = k.split_at_mut(0usize);
+        os.1[i as usize] = x
+    });
+    k[12usize] = (k[12usize]).wrapping_add(ctr_u32)
+}
+
+fn chacha20_init(ctx: &mut [u32], k: &[u8], n: &[u8], ctr: u32) {
+    krml::unroll_for!(4, "i", 0u32, 1u32, {
+        let x: u32 = (&crate::hacl::chacha20::chacha20_constants)[i as usize];
+        let os: &mut [u32] = &mut (&mut ctx[0usize..])[0usize..];
+        os[i as usize] = x
+    });
+    let uu____0: (&mut [u32], &mut [u32]) = ctx.split_at_mut(4usize);
+    krml::unroll_for!(8, "i", 0u32, 1u32, {
+        let bj: (&[u8], &[u8]) = k.split_at(i.wrapping_mul(4u32) as usize);
+        let u: u32 = lowstar::endianness::load32_le(bj.1);
+        let r: u32 = u;
+        let x: u32 = r;
+        let os: (&mut [u32], &mut [u32]) = uu____0.1.split_at_mut(0usize);
+        os.1[i as usize] = x
+    });
+    ctx[12usize] = ctr;
+    let uu____1: (&mut [u32], &mut [u32]) = ctx.split_at_mut(13usize);
+    krml::unroll_for!(3, "i", 0u32, 1u32, {
+        let bj: (&[u8], &[u8]) = n.split_at(i.wrapping_mul(4u32) as usize);
+        let u: u32 = lowstar::endianness::load32_le(bj.1);
+        let r: u32 = u;
+        let x: u32 = r;
+        let os: (&mut [u32], &mut [u32]) = uu____1.1.split_at_mut(0usize);
+        os.1[i as usize] = x
+    })
+}
+
+fn chacha20_encrypt_block(ctx: &[u32], out: &mut [u8], incr: u32, text: &[u8]) {
+    let mut k: [u32; 16] = [0u32; 16usize];
+    crate::hacl::chacha20::chacha20_core(&mut k, ctx, incr);
+    let mut bl: [u32; 16] = [0u32; 16usize];
+    krml::unroll_for!(16, "i", 0u32, 1u32, {
+        let bj: (&[u8], &[u8]) = text.split_at(i.wrapping_mul(4u32) as usize);
+        let u: u32 = lowstar::endianness::load32_le(bj.1);
+        let r: u32 = u;
+        let x: u32 = r;
+        let os: (&mut [u32], &mut [u32]) = bl.split_at_mut(0usize);
+        os.1[i as usize] = x
+    });
+    krml::unroll_for!(16, "i", 0u32, 1u32, {
+        let x: u32 = (&bl)[i as usize] ^ (&k)[i as usize];
+        let os: (&mut [u32], &mut [u32]) = bl.split_at_mut(0usize);
+        os.1[i as usize] = x
+    });
+    krml::unroll_for!(
+        16,
+        "i",
+        0u32,
+        1u32,
+        lowstar::endianness::store32_le(
+            &mut out[i.wrapping_mul(4u32) as usize..],
+            (&bl)[i as usize]
+        )
+    )
+}
+
+#[inline]
+fn chacha20_encrypt_last(ctx: &[u32], len: u32, out: &mut [u8], incr: u32, text: &[u8]) {
+    let mut plain: [u8; 64] = [0u8; 64usize];
+    ((&mut plain)[0usize..len as usize]).copy_from_slice(&text[0usize..len as usize]);
+    let mut plain_copy: [u8; 64] = [0u8; 64usize];
+    ((&mut plain_copy)[0usize..64usize]).copy_from_slice(&(&plain)[0usize..64usize]);
+    crate::hacl::chacha20::chacha20_encrypt_block(ctx, &mut plain, incr, &plain_copy);
+    (out[0usize..len as usize]).copy_from_slice(&(&(&plain)[0usize..])[0usize..len as usize])
+}
+
+fn chacha20_update(ctx: &[u32], len: u32, out: &mut [u8], text: &[u8]) {
+    let rem: u32 = len.wrapping_rem(64u32);
+    let nb: u32 = len.wrapping_div(64u32);
+    let rem1: u32 = len.wrapping_rem(64u32);
+    for i in 0u32..nb {
+        crate::hacl::chacha20::chacha20_encrypt_block(
+            ctx,
+            &mut out[i.wrapping_mul(64u32) as usize..],
+            i,
+            &text[i.wrapping_mul(64u32) as usize..],
+        )
+    }
+    if rem1 > 0u32 {
+        crate::hacl::chacha20::chacha20_encrypt_last(
+            ctx,
+            rem,
+            &mut out[nb.wrapping_mul(64u32) as usize..],
+            nb,
+            &text[nb.wrapping_mul(64u32) as usize..],
+        )
+    }
+}
+
+pub fn chacha20_encrypt(len: u32, out: &mut [u8], text: &[u8], key: &[u8], n: &[u8], ctr: u32) {
+    let mut ctx: [u32; 16] = [0u32; 16usize];
+    crate::hacl::chacha20::chacha20_init(&mut ctx, key, n, ctr);
+    crate::hacl::chacha20::chacha20_update(&ctx, len, out, text)
+}
+
+#[allow(dead_code)]
+pub fn chacha20_decrypt(len: u32, out: &mut [u8], cipher: &[u8], key: &[u8], n: &[u8], ctr: u32) {
+    let mut ctx: [u32; 16] = [0u32; 16usize];
+    crate::hacl::chacha20::chacha20_init(&mut ctx, key, n, ctr);
+    crate::hacl::chacha20::chacha20_update(&ctx, len, out, cipher)
+}

chacha20poly1305/src/impl_hacl.rs

@@ -0,0 +1,111 @@
+use crate::{AeadError, KEY_LEN, NONCE_LEN, TAG_LEN};
+
+/// The ChaCha20-Poly1305 AEAD encryption function. Writes the concatenation of the ciphertexoft
+/// produced by ChaCha20 and the MAC tag into `ctxt` and returns the two pieces separately.
+///
+/// This implementation is backed by hacl-rs and can only handle inputs up to a length of `u32::MAX`.
+/// When provided longer values, this function will return an error.
+pub fn encrypt<'a>(
+    key: &[u8; KEY_LEN],
+    ptxt: &[u8],
+    ctxt: &'a mut [u8],
+    aad: &[u8],
+    nonce: &[u8; NONCE_LEN],
+) -> Result<(&'a [u8], &'a [u8; TAG_LEN]), AeadError> {
+    let ptxt_len: u32 = ptxt
+        .len()
+        .try_into()
+        .map_err(|_| AeadError::PlaintextTooLarge)?;
+
+    let aad_len: u32 = aad.len().try_into().map_err(|_| AeadError::AadTooLarge)?;
+
+    // we already knwo that ptxt.len() < u32::MAX, so we can safely add if we use u64.
+    if (ctxt.len() as u64) < (ptxt.len() as u64) + (TAG_LEN as u64) {
+        return Err(AeadError::CiphertextTooShort);
+    }
+
+    // ensure destination slice has just the right length
+    let (ctxt_cpa, tag) = ctxt.split_at_mut(ptxt.len());
+    let tag: &mut [u8; TAG_LEN] = tag.try_into().unwrap();
+
+    crate::hacl::aead_chacha20poly1305::encrypt(
+        ctxt_cpa, tag, ptxt, ptxt_len, aad, aad_len, key, nonce,
+    );
+
+    Ok((ctxt_cpa, tag))
+}
+
+/// The ChaCha20-Poly1305 AEAD decryption function. Writes the result of the decryption to `ptxt`,
+/// and returns the slice of appropriate length.
+///
+/// This implementation is backed by hacl-rs and can only handle inputs up to a length of `u32::MAX`.
+/// When provided longer values, this function will return an error.
+pub fn decrypt<'a>(
+    key: &[u8; KEY_LEN],
+    ptxt: &'a mut [u8],
+    ctxt: &[u8],
+    aad: &[u8],
+    nonce: &[u8; NONCE_LEN],
+) -> Result<&'a [u8], AeadError> {
+    if ctxt.len() < TAG_LEN {
+        return Err(AeadError::InvalidCiphertext);
+    }
+
+    // we know that ctxt.len() >= TAG_LEN, so we can subtract
+    if ptxt.len() < ctxt.len() - TAG_LEN {
+        return Err(AeadError::PlaintextTooShort);
+    }
+
+    let ctxt_len: u32 = ctxt
+        .len()
+        .try_into()
+        .map_err(|_| AeadError::CiphertextTooLarge)?;
+
+    let aad_len: u32 = aad.len().try_into().map_err(|_| AeadError::AadTooLarge)?;
+
+    let (ctxt_cpa, tag) = ctxt.split_at(ctxt.len() - TAG_LEN);
+    let ptxt = &mut ptxt[..ctxt_cpa.len()];
+
+    // this call should only ever produce 0 or 1, where 0 is success and 1 is error
+    match crate::hacl::aead_chacha20poly1305::decrypt(
+        ptxt, ctxt_cpa, ctxt_len, aad, aad_len, key, nonce, tag,
+    ) {
+        0 => Ok(ptxt),
+        _ => Err(AeadError::InvalidCiphertext),
+    }
+}
+
+/// The ChaCha20-Poly1305 AEAD decryption function. Writes the result of the decryption to `ptxt`,
+/// and returns the slice of appropriate length.
+///
+/// This implementation is backed by hacl-rs and can only handle inputs up to a length of `u32::MAX`.
+/// When provided longer values, this function will return an error.
+pub fn decrypt_detached<'a>(
+    key: &[u8; KEY_LEN],
+    ptxt: &'a mut [u8],
+    ctxt: &[u8],
+    tag: &[u8; TAG_LEN],
+    aad: &[u8],
+    nonce: &[u8; NONCE_LEN],
+) -> Result<&'a [u8], AeadError> {
+    if ptxt.len() < ctxt.len() {
+        return Err(AeadError::PlaintextTooShort);
+    }
+
+    let ctxt_len: u32 = ctxt
+        .len()
+        .try_into()
+        .map_err(|_| AeadError::CiphertextTooLarge)?;
+
+    let aad_len: u32 = aad.len().try_into().map_err(|_| AeadError::AadTooLarge)?;
+
+    let ptxt = &mut ptxt[..ctxt.len()];
+
+    // this call should only ever produce 0 or 1, where 0 is success and 1 is error
+    match crate::hacl::aead_chacha20poly1305::decrypt(
+        ptxt, ctxt, ctxt_len, aad, aad_len, key, nonce, tag,
+    ) {
+        0 => Ok(ptxt),
+        _ => Err(AeadError::InvalidCiphertext),
+    }
+}

chacha20poly1305/src/lib.rs

@@ -0,0 +1,47 @@
+#![no_std]
+
+/// The length of ChaCha20-Poly1305 keys.
+pub const KEY_LEN: usize = 32;
+
+/// The length of Poly1305 MAC tags.
+pub const TAG_LEN: usize = 16;
+
+/// The length of ChaCha20-Poly1305 nonces.
+pub const NONCE_LEN: usize = 12;
+
+/// Describes the error conditions of the  ChaCha20-Poly1305 AEAD.
+pub enum AeadError {
+    /// Indicates that the plaintext argument is too large for the library to handle.
+    PlaintextTooLarge,
+    /// Indicates that the ciphertext argument is too large for the library to handle.
+    CiphertextTooLarge,
+    /// Indicates that the associated data argument is too large for the library to handle.
+    AadTooLarge,
+    /// This indicates that the provided destination ciphertext does not fit the ciphertext and tag.
+    CiphertextTooShort,
+    /// This indicates that the provided destination plaintext is shorter than `ctxt.len() - TAG_LEN`
+    /// and thus will not fit the decrypted plaintext
+    PlaintextTooShort,
+    /// Indicates that the ciphertext is not a valid encryption under the given key and nonce.
+    InvalidCiphertext,
+}
+
+/// Describes the error conditions of the Poly1305 MAC.
+pub enum MacError {
+    /// Indicates that the message argument is too large for the library to handle.
+    MessageTooLarge,
+
+    /// Indicates that the MAC tag is invalid for that key and message.
+    InvalidMacTag,
+}
+
+mod hacl {
+    pub(crate) use libcrux_poly1305::hacl::mac_poly1305;
+
+    pub(crate) mod aead_chacha20poly1305;
+    pub(crate) mod chacha20;
+}
+
+mod impl_hacl;
+
+pub use impl_hacl::*;