Skip to content

Commit

Permalink
Update fiat-crypto to 0.2.1 (#352)
Browse files Browse the repository at this point in the history
* Bump fiat-crypto 0.2.1

* poly1305: Convert to fiat-crypto newtypes

* x25519: Use fiat-crypto newtypes
  • Loading branch information
brycx authored Sep 5, 2023
1 parent d91593f commit d077cfe
Show file tree
Hide file tree
Showing 4 changed files with 67 additions and 45 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ __Date:__ TBD.

__Changelog:__
- Bump MSRV to `1.70.0`.
- Bump `fiat-crypto` to `0.2.1`.

### 0.17.5

Expand Down
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ exclude = [
[dependencies]
subtle = { version = "^2.2.2", default-features = false }
zeroize = { version = "1.1.0", default-features = false }
fiat-crypto = {version = "0.1.11", default-features = false}
fiat-crypto = {version = "0.2.1", default-features = false}
getrandom = { version = "0.2.0", optional = true }
ct-codecs = { version = "1.1.1", optional = true }

Expand Down
71 changes: 45 additions & 26 deletions src/hazardous/ecc/x25519.rs
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,11 @@ use core::ops::{Add, Mul, Sub};

/// Formally verified Curve25519 field arithmetic from: <https://github.com/mit-plv/fiat-crypto>.
use fiat_crypto::curve25519_64 as fiat_curve25519_u64;
use fiat_curve25519_u64::{
fiat_25519_add, fiat_25519_carry, fiat_25519_carry_mul, fiat_25519_carry_scmul_121666,
fiat_25519_carry_square, fiat_25519_loose_field_element, fiat_25519_relax, fiat_25519_sub,
fiat_25519_tight_field_element,
};

/// The size of a public key used in X25519.
pub const PUBLIC_KEY_SIZE: usize = 32;
Expand All @@ -86,9 +91,9 @@ const BASEPOINT: [u8; 32] = [
/// The result of computing a shared secret with a low order point.
const LOW_ORDER_POINT_RESULT: [u8; 32] = [0u8; 32];

#[derive(Clone, Copy, Debug)]
#[derive(Clone, Copy)]
/// Represent an element in the curve field.
struct FieldElement([u64; 5]);
struct FieldElement(fiat_25519_tight_field_element);

impl Eq for FieldElement {}

Expand All @@ -99,15 +104,25 @@ impl PartialEq for FieldElement {
}
}

impl core::fmt::Debug for FieldElement {
fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
write!(f, "FieldElement({:?})", &self.0 .0)
}
}

/// The function fiat_25519_carry_mul multiplies two field elements and reduces the result.
impl Mul for FieldElement {
type Output = Self;

fn mul(self, rhs: Self) -> Self::Output {
use fiat_curve25519_u64::fiat_25519_carry_mul;
let mut ret = fiat_25519_tight_field_element([0u64; 5]);
let mut self_relaxed = fiat_25519_loose_field_element([0u64; 5]);
let mut rhs_relaxed = fiat_25519_loose_field_element([0u64; 5]);

fiat_25519_relax(&mut self_relaxed, &self.0);
fiat_25519_relax(&mut rhs_relaxed, &rhs.0);

let mut ret = [0u64; 5];
fiat_25519_carry_mul(&mut ret, &self.0, &rhs.0);
fiat_25519_carry_mul(&mut ret, &self_relaxed, &rhs_relaxed);

Self(ret)
}
Expand All @@ -118,12 +133,11 @@ impl Add for FieldElement {
type Output = Self;

fn add(self, rhs: Self) -> Self::Output {
use fiat_curve25519_u64::{fiat_25519_add, fiat_25519_carry};
let mut ret = fiat_25519_tight_field_element([0u64; 5]);
let mut ret_add = fiat_25519_loose_field_element([0u64; 5]);

let mut ret = [0u64; 5];
fiat_25519_add(&mut ret, &self.0, &rhs.0);
let tmp = ret;
fiat_25519_carry(&mut ret, &tmp);
fiat_25519_add(&mut ret_add, &self.0, &rhs.0);
fiat_25519_carry(&mut ret, &ret_add);

Self(ret)
}
Expand All @@ -134,12 +148,11 @@ impl Sub for FieldElement {
type Output = Self;

fn sub(self, rhs: Self) -> Self::Output {
use fiat_curve25519_u64::{fiat_25519_carry, fiat_25519_sub};
let mut ret = fiat_25519_tight_field_element([0u64; 5]);
let mut ret_sub = fiat_25519_loose_field_element([0u64; 5]);

let mut ret = [0u64; 5];
fiat_25519_sub(&mut ret, &self.0, &rhs.0);
let tmp = ret;
fiat_25519_carry(&mut ret, &tmp);
fiat_25519_sub(&mut ret_sub, &self.0, &rhs.0);
fiat_25519_carry(&mut ret, &ret_sub);

Self(ret)
}
Expand All @@ -148,12 +161,16 @@ impl Sub for FieldElement {
impl FieldElement {
/// Create a `FieldElement` that is `0`.
fn zero() -> Self {
Self([0u64, 0u64, 0u64, 0u64, 0u64])
Self(fiat_25519_tight_field_element([
0u64, 0u64, 0u64, 0u64, 0u64,
]))
}

/// Create a `FieldElement` that is `1`.
fn one() -> Self {
Self([1u64, 0u64, 0u64, 0u64, 0u64])
Self(fiat_25519_tight_field_element([
1u64, 0u64, 0u64, 0u64, 0u64,
]))
}

/// Serialize the `FieldElement` as a byte-array.
Expand All @@ -179,7 +196,7 @@ impl FieldElement {
temp[31] &= 127u8; // See RFC: "When receiving such an array, implementations of X25519
// (but not X448) MUST mask the most significant bit in the final byte."

let mut ret = [0u64; 5];
let mut ret = fiat_25519_tight_field_element([0u64; 5]);
fiat_25519_from_bytes(&mut ret, &temp);

Self(ret)
Expand All @@ -196,26 +213,28 @@ impl FieldElement {
let tmp_a = *a;
let tmp_b = *b;

fiat_25519_selectznz(&mut a.0, swap, &tmp_a.0, &tmp_b.0);
fiat_25519_selectznz(&mut b.0, swap, &tmp_b.0, &tmp_a.0);
fiat_25519_selectznz(&mut a.0 .0, swap, &tmp_a.0 .0, &tmp_b.0 .0);
fiat_25519_selectznz(&mut b.0 .0, swap, &tmp_b.0 .0, &tmp_a.0 .0);
}

/// Square the `FieldElement` and reduce the result.
fn square(&self) -> Self {
use fiat_curve25519_u64::fiat_25519_carry_square;
let mut self_relaxed = fiat_25519_loose_field_element([0u64; 5]);
let mut ret = fiat_25519_tight_field_element([0u64; 5]);

let mut ret = [0u64; 5];
fiat_25519_carry_square(&mut ret, &self.0);
fiat_25519_relax(&mut self_relaxed, &self.0);
fiat_25519_carry_square(&mut ret, &self_relaxed);

Self(ret)
}

/// Multiply the `FieldElement` by 121666 and reduce the result.
fn mul_121666(&self) -> Self {
use fiat_curve25519_u64::fiat_25519_carry_scmul_121666;
let mut self_relaxed = fiat_25519_loose_field_element([0u64; 5]);
let mut ret = fiat_25519_tight_field_element([0u64; 5]);

let mut ret = [0u64; 5];
fiat_25519_carry_scmul_121666(&mut ret, &self.0);
fiat_25519_relax(&mut self_relaxed, &self.0);
fiat_25519_carry_scmul_121666(&mut ret, &self_relaxed);

Self(ret)
}
Expand Down
38 changes: 20 additions & 18 deletions src/hazardous/mac/poly1305.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,8 +77,8 @@ use crate::{
};
use fiat_crypto::poly1305_32::{
fiat_poly1305_add, fiat_poly1305_carry, fiat_poly1305_carry_mul, fiat_poly1305_from_bytes,
fiat_poly1305_loose_field_element, fiat_poly1305_selectznz, fiat_poly1305_subborrowx_u26,
fiat_poly1305_tight_field_element, fiat_poly1305_u1,
fiat_poly1305_loose_field_element, fiat_poly1305_relax, fiat_poly1305_selectznz,
fiat_poly1305_subborrowx_u26, fiat_poly1305_tight_field_element, fiat_poly1305_u1,
};

/// The blocksize which Poly1305 operates on.
Expand Down Expand Up @@ -119,8 +119,8 @@ impl_from_trait!(Tag, POLY1305_OUTSIZE);
#[derive(Clone)]
/// Poly1305 streaming state.
pub struct Poly1305 {
a: [u32; 5],
r: [u32; 5],
a: fiat_poly1305_tight_field_element,
r: fiat_poly1305_loose_field_element,
s: [u32; 4],
leftover: usize,
buffer: [u8; POLY1305_BLOCKSIZE],
Expand All @@ -130,8 +130,8 @@ pub struct Poly1305 {
impl Drop for Poly1305 {
fn drop(&mut self) {
use zeroize::Zeroize;
self.a.zeroize();
self.r.zeroize();
self.a.0.zeroize();
self.r.0.zeroize();
self.s.zeroize();
self.buffer.zeroize();
}
Expand Down Expand Up @@ -164,11 +164,11 @@ impl Poly1305 {
// One byte is appended to detect trailing zeroes if not last chunk.
// See https://cr.yp.to/mac/poly1305-20050329.pdf, Section 2 "Conversion and padding".
mb[16] = u8::from(!self.is_finalized);
let mut m: fiat_poly1305_tight_field_element = [0u32; 5];
let mut m = fiat_poly1305_tight_field_element([0u32; 5]);
fiat_poly1305_from_bytes(&mut m, &mb);

// h += m
let mut h: fiat_poly1305_loose_field_element = [0u32; 5];
let mut h = fiat_poly1305_loose_field_element([0u32; 5]);
fiat_poly1305_add(&mut h, &self.a, &m);
// h *= r with partial reduction modulo p
fiat_poly1305_carry_mul(&mut self.a, &h, &self.r);
Expand All @@ -181,11 +181,13 @@ impl Poly1305 {
/// Remaining processing after all data blocks have been processed.
fn process_end_of_stream(&mut self) {
// full carry h
let mut buf_h: fiat_poly1305_tight_field_element = [0u32; 5];
fiat_poly1305_carry(&mut buf_h, &self.a);
let mut buf_h = fiat_poly1305_tight_field_element([0u32; 5]);
let mut a_relaxed = fiat_poly1305_loose_field_element([0u32; 5]);
fiat_poly1305_relax(&mut a_relaxed, &self.a);
fiat_poly1305_carry(&mut buf_h, &a_relaxed);

// compute h + -p
let mut p: fiat_poly1305_tight_field_element = [0u32; 5];
let mut p = fiat_poly1305_tight_field_element([0u32; 5]);
fiat_poly1305_from_bytes(&mut p, &Self::PRIME);

let mut carry: fiat_poly1305_u1 = 0;
Expand All @@ -197,7 +199,7 @@ impl Poly1305 {

// select h if h < p, or h + -p if h >= p
let mut ret = [0u32; 5];
fiat_poly1305_selectznz(&mut ret, carry,&[g0, g1, g2, g3, g4], &buf_h);
fiat_poly1305_selectznz(&mut ret, carry,&[g0, g1, g2, g3, g4], &buf_h.0);

let mut h0 = ret[0];
let mut h1 = ret[1];
Expand Down Expand Up @@ -228,8 +230,8 @@ impl Poly1305 {
/// Initialize a `Poly1305` struct with a given one-time key.
pub fn new(one_time_key: &OneTimeKey) -> Self {
let mut state = Self {
a: [0u32; 5],
r: [0u32; 5],
a: fiat_poly1305_tight_field_element([0u32; 5]),
r: fiat_poly1305_loose_field_element([0u32; 5]),
s: [0u32; 4],
leftover: 0,
buffer: [0u8; POLY1305_BLOCKSIZE],
Expand Down Expand Up @@ -280,7 +282,7 @@ impl Poly1305 {

/// Reset to `new()` state.
pub fn reset(&mut self) {
self.a = [0u32; 5];
self.a = fiat_poly1305_tight_field_element([0u32; 5]);
self.leftover = 0;
self.is_finalized = false;
self.buffer = [0u8; POLY1305_BLOCKSIZE];
Expand Down Expand Up @@ -358,7 +360,7 @@ impl Poly1305 {
}

self.process_end_of_stream();
store_u32_into_le(&self.a[0..4], &mut local_buffer);
store_u32_into_le(&self.a.0[0..4], &mut local_buffer);

Ok(Tag::from(local_buffer))
}
Expand Down Expand Up @@ -455,8 +457,8 @@ mod public {
}

fn compare_states(state_1: &Poly1305, state_2: &Poly1305) {
assert_eq!(state_1.a, state_2.a);
assert_eq!(state_1.r, state_2.r);
assert_eq!(state_1.a.0, state_2.a.0);
assert_eq!(state_1.r.0, state_2.r.0);
assert_eq!(state_1.s, state_2.s);
assert_eq!(state_1.leftover, state_2.leftover);
assert_eq!(state_1.buffer[..], state_2.buffer[..]);
Expand Down

0 comments on commit d077cfe

Please sign in to comment.