Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions BIBLIOGRAPHY.md
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,17 @@ source code and documentation.
* Referenced from:
- [proofs/isabelle/neon_ntt/README.md](proofs/isabelle/neon_ntt/README.md)

### `DilithiumMemory`

* Dilithium for Memory Constrained Devices
* Author(s):
- Joppe W. Bos
- Joost Renes
- Amber Sprenkels
* URL: https://eprint.iacr.org/2022/323
* Referenced from:
- [mldsa/src/sign.c](mldsa/src/sign.c)

### `FIPS140_3_IG`

* Implementation Guidance for FIPS 140-3 and the Cryptographic Module Validation Program
Expand Down
8 changes: 8 additions & 0 deletions BIBLIOGRAPHY.yml
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,14 @@
author: National Institute of Standards and Technology
url: https://csrc.nist.gov/projects/cryptographic-module-validation-program/fips-140-3-ig-announcements

- id: DilithiumMemory
name: "Dilithium for Memory Constrained Devices"
author:
- Bos, Joppe W.
- Renes, Joost
- Sprenkels, Amber
url: https://eprint.iacr.org/2022/323

- id: Round3_Spec
name: "CRYSTALS-Dilithium Algorithm Specifications and Supporting Documentation (Version 3.1)"
author:
Expand Down
30 changes: 30 additions & 0 deletions integration/pavona/sign-work-buffer-size.patch
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
# Copyright (c) The mldsa-native project authors
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
#
# Track the reduced signing work buffer of mldsa-native. The crypto
# library wrapper pins the work buffer sizes and cross-checks them
# against MLD_TOTAL_ALLOC_* with a static assertion, so the signing
# sizes have to follow when mldsa-native allocates less.

diff --git a/sw/device/lib/crypto/include/mldsa.h b/sw/device/lib/crypto/include/mldsa.h
--- a/sw/device/lib/crypto/include/mldsa.h
+++ b/sw/device/lib/crypto/include/mldsa.h
@@ -42,15 +42,15 @@

// Work buffer sizes in 32-bit words
kOtcryptoMldsa44WorkBufferKeypairWords = 11584 / sizeof(uint32_t),
- kOtcryptoMldsa44WorkBufferSignWords = 13120 / sizeof(uint32_t),
+ kOtcryptoMldsa44WorkBufferSignWords = 9792 / sizeof(uint32_t),
kOtcryptoMldsa44WorkBufferVerifyWords = 9120 / sizeof(uint32_t),

kOtcryptoMldsa65WorkBufferKeypairWords = 14656 / sizeof(uint32_t),
- kOtcryptoMldsa65WorkBufferSignWords = 17248 / sizeof(uint32_t),
+ kOtcryptoMldsa65WorkBufferSignWords = 11872 / sizeof(uint32_t),
kOtcryptoMldsa65WorkBufferVerifyWords = 10208 / sizeof(uint32_t),

kOtcryptoMldsa87WorkBufferKeypairWords = 18752 / sizeof(uint32_t),
- kOtcryptoMldsa87WorkBufferSignWords = 21344 / sizeof(uint32_t),
+ kOtcryptoMldsa87WorkBufferSignWords = 14176 / sizeof(uint32_t),
kOtcryptoMldsa87WorkBufferVerifyWords = 12512 / sizeof(uint32_t),
};

12 changes: 10 additions & 2 deletions mldsa/mldsa_native.c
Original file line number Diff line number Diff line change
Expand Up @@ -274,6 +274,9 @@
#undef MLDSA_POLYW1_PACKEDBYTES
#undef MLDSA_POLYW1_PACKEDBYTES_32
#undef MLDSA_POLYW1_PACKEDBYTES_88
#undef MLDSA_POLYW1_PACKED_BITS
#undef MLDSA_POLYW1_PACKED_BITS_32
#undef MLDSA_POLYW1_PACKED_BITS_88
#undef MLDSA_POLYZ_PACKEDBYTES
#undef MLDSA_Q
#undef MLDSA_Q_HALF
Expand Down Expand Up @@ -316,18 +319,18 @@
#undef mld_polyeta_pack
#undef mld_polyeta_unpack
#undef mld_polyw1_pack
#undef mld_polyw1_unpack
#undef mld_polyz_pack
#undef mld_polyz_unpack
/* mldsa/src/polyvec.h */
#undef MLD_POLYVEC_H
#undef mld_polyveck
#undef mld_polyveck_caddq
#undef mld_polyveck_chknorm
#undef mld_polyveck_decompose
#undef mld_polyveck_decompose_pack_w1
#undef mld_polyveck_invntt_tomont
#undef mld_polyveck_ntt
#undef mld_polyveck_pack_eta
#undef mld_polyveck_pack_w1
#undef mld_polyveck_reduce
#undef mld_polyveck_unpack_eta
#undef mld_polyvecl
Expand Down Expand Up @@ -390,6 +393,9 @@
#undef mld_yvec_init_eager
#undef mld_yvec_init_lazy
#undef mld_yvec_lazy
#undef mld_yvec_scratch
#undef mld_yvec_scratch_eager
#undef mld_yvec_scratch_lazy
/* mldsa/src/rounding.h */
#undef MLD_2_POW_D
#undef MLD_ROUNDING_H
Expand Down Expand Up @@ -484,6 +490,8 @@
#undef mld_polyt1_unpack
#undef mld_polyw1_pack_32
#undef mld_polyw1_pack_88
#undef mld_polyw1_unpack_32
#undef mld_polyw1_unpack_88
/* mldsa/src/randombytes.h */
#undef MLD_RANDOMBYTES_H
/* mldsa/src/reduce.h */
Expand Down
24 changes: 12 additions & 12 deletions mldsa/mldsa_native.h
Original file line number Diff line number Diff line change
Expand Up @@ -889,35 +889,35 @@ int MLD_API_NAMESPACE(pk_from_sk)(
/* check-magic: off */
#if !defined(MLD_CONFIG_REDUCE_RAM)
#define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 26912
#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 48480
#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 48224
#define MLD_TOTAL_ALLOC_44_PK_FROM_SK 28480
#define MLD_TOTAL_ALLOC_44_SIGN 44704
#define MLD_TOTAL_ALLOC_44_SIGN 44448
#define MLD_TOTAL_ALLOC_44_VERIFY 24448
#define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 44320
#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 74624
#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 73344
#define MLD_TOTAL_ALLOC_65_PK_FROM_SK 46720
#define MLD_TOTAL_ALLOC_65_SIGN 69312
#define MLD_TOTAL_ALLOC_65_SIGN 68032
#define MLD_TOTAL_ALLOC_65_VERIFY 39872
#define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 75040
#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 115488
#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 114464
#define MLD_TOTAL_ALLOC_87_PK_FROM_SK 78272
#define MLD_TOTAL_ALLOC_87_SIGN 108224
#define MLD_TOTAL_ALLOC_87_SIGN 107200
#define MLD_TOTAL_ALLOC_87_VERIFY 68800
#else /* !MLD_CONFIG_REDUCE_RAM */
#define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 11584
#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 16896
#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 13568
#define MLD_TOTAL_ALLOC_44_PK_FROM_SK 13152
#define MLD_TOTAL_ALLOC_44_SIGN 13120
#define MLD_TOTAL_ALLOC_44_SIGN 9792
#define MLD_TOTAL_ALLOC_44_VERIFY 9120
#define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 14656
#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 22560
#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 17184
#define MLD_TOTAL_ALLOC_65_PK_FROM_SK 17056
#define MLD_TOTAL_ALLOC_65_SIGN 17248
#define MLD_TOTAL_ALLOC_65_SIGN 11872
#define MLD_TOTAL_ALLOC_65_VERIFY 10208
#define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 18752
#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 28608
#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 21440
#define MLD_TOTAL_ALLOC_87_PK_FROM_SK 21984
#define MLD_TOTAL_ALLOC_87_SIGN 21344
#define MLD_TOTAL_ALLOC_87_SIGN 14176
#define MLD_TOTAL_ALLOC_87_VERIFY 12512
#endif /* MLD_CONFIG_REDUCE_RAM */
/* check-magic: on */
Expand Down
12 changes: 10 additions & 2 deletions mldsa/mldsa_native_asm.S
Original file line number Diff line number Diff line change
Expand Up @@ -301,6 +301,9 @@
#undef MLDSA_POLYW1_PACKEDBYTES
#undef MLDSA_POLYW1_PACKEDBYTES_32
#undef MLDSA_POLYW1_PACKEDBYTES_88
#undef MLDSA_POLYW1_PACKED_BITS
#undef MLDSA_POLYW1_PACKED_BITS_32
#undef MLDSA_POLYW1_PACKED_BITS_88
#undef MLDSA_POLYZ_PACKEDBYTES
#undef MLDSA_Q
#undef MLDSA_Q_HALF
Expand Down Expand Up @@ -343,18 +346,18 @@
#undef mld_polyeta_pack
#undef mld_polyeta_unpack
#undef mld_polyw1_pack
#undef mld_polyw1_unpack
#undef mld_polyz_pack
#undef mld_polyz_unpack
/* mldsa/src/polyvec.h */
#undef MLD_POLYVEC_H
#undef mld_polyveck
#undef mld_polyveck_caddq
#undef mld_polyveck_chknorm
#undef mld_polyveck_decompose
#undef mld_polyveck_decompose_pack_w1
#undef mld_polyveck_invntt_tomont
#undef mld_polyveck_ntt
#undef mld_polyveck_pack_eta
#undef mld_polyveck_pack_w1
#undef mld_polyveck_reduce
#undef mld_polyveck_unpack_eta
#undef mld_polyvecl
Expand Down Expand Up @@ -417,6 +420,9 @@
#undef mld_yvec_init_eager
#undef mld_yvec_init_lazy
#undef mld_yvec_lazy
#undef mld_yvec_scratch
#undef mld_yvec_scratch_eager
#undef mld_yvec_scratch_lazy
/* mldsa/src/rounding.h */
#undef MLD_2_POW_D
#undef MLD_ROUNDING_H
Expand Down Expand Up @@ -511,6 +517,8 @@
#undef mld_polyt1_unpack
#undef mld_polyw1_pack_32
#undef mld_polyw1_pack_88
#undef mld_polyw1_unpack_32
#undef mld_polyw1_unpack_88
/* mldsa/src/randombytes.h */
#undef MLD_RANDOMBYTES_H
/* mldsa/src/reduce.h */
Expand Down
10 changes: 7 additions & 3 deletions mldsa/src/packing.c
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,8 @@ void mld_pack_sig_c(uint8_t sig[MLDSA_CRYPTO_BYTES],

MLD_INTERNAL_API
int mld_pack_sig_h(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_polyveck *w0,
const mld_polyveck *w1)
const uint8_t w1_packed[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES],
mld_poly *scratch)
{
unsigned int j, k, n;

Expand All @@ -100,11 +101,14 @@ int mld_pack_sig_h(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_polyveck *w0,
* before the call), so a data-dependent early return is fine. */
for (k = 0; k < MLDSA_K; k++)
__loop__(
assigns(k, j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES))
assigns(k, j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES),
memory_slice(scratch, sizeof(mld_poly)))
invariant(k <= MLDSA_K && n <= MLDSA_OMEGA)
decreases(MLDSA_K - k)
)
{
mld_polyw1_unpack(scratch, w1_packed + k * MLDSA_POLYW1_PACKEDBYTES);

for (j = 0; j < MLDSA_N; j++)
__loop__(
assigns(j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES))
Expand All @@ -113,7 +117,7 @@ int mld_pack_sig_h(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_polyveck *w0,
)
{
const unsigned int hint_bit =
mld_make_hint(w0->vec[k].coeffs[j], w1->vec[k].coeffs[j]);
mld_make_hint(w0->vec[k].coeffs[j], scratch->coeffs[j]);
if (hint_bit)
{
if (n == MLDSA_OMEGA)
Expand Down
16 changes: 11 additions & 5 deletions mldsa/src/packing.h
Original file line number Diff line number Diff line change
Expand Up @@ -107,9 +107,12 @@ __contract__(
* MakeHint valid only for the values arising during signing; see the block
* comment in mld_attempt_signature_generation (sign.c).}
*
* @param[in,out] sig Byte array containing signature.
* @param[in] w0 Pointer to low part of input vector.
* @param[in] w1 Pointer to high part of input vector.
* @param[in,out] sig Byte array containing signature.
* @param[in] w0 Pointer to low part of input vector.
* @param[in] w1_packed Bit-packed high part of input vector, as produced
* by mld_polyw1_pack.
* @param[out] scratch Scratch polynomial, used to unpack one row of the
* high part at a time.
*
* @retval 0 Success.
* @retval MLD_ERR_FAIL The total number of hints exceeds MLDSA_OMEGA. In this
Expand All @@ -120,12 +123,15 @@ __contract__(
MLD_INTERNAL_API
MLD_MUST_CHECK_RETURN_VALUE
int mld_pack_sig_h(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_polyveck *w0,
const mld_polyveck *w1)
const uint8_t w1_packed[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES],
mld_poly *scratch)
__contract__(
requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
requires(memory_no_alias(w0, sizeof(mld_polyveck)))
requires(memory_no_alias(w1, sizeof(mld_polyveck)))
requires(memory_no_alias(w1_packed, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))
requires(memory_no_alias(scratch, sizeof(mld_poly)))
assigns(memory_slice(sig + MLDSA_SIG_H_OFFSET, MLDSA_POLYVECH_PACKEDBYTES))
assigns(memory_slice(scratch, sizeof(mld_poly)))
ensures(return_value == 0 || return_value == MLD_ERR_FAIL)
);

Expand Down
11 changes: 9 additions & 2 deletions mldsa/src/params.h
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,12 @@

#define MLDSA_GAMMA2_88 ((MLDSA_Q - 1) / 88)
#define MLDSA_GAMMA2_32 ((MLDSA_Q - 1) / 32)
#define MLDSA_POLYW1_PACKEDBYTES_88 192
#define MLDSA_POLYW1_PACKEDBYTES_32 128
/* Bits per w1 coefficient: bitlen((MLDSA_Q-1)/(2*MLDSA_GAMMA2) - 1), i.e.
* bitlen(43) for MLDSA_GAMMA2_88 and bitlen(15) for MLDSA_GAMMA2_32. */
#define MLDSA_POLYW1_PACKED_BITS_88 6
#define MLDSA_POLYW1_PACKED_BITS_32 4
Comment on lines +21 to +22

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Introducing those is slightly inconsistent with existing packing routines, which hardcode their bit widths. E.g. mld_polyt1_[un]pack.

#define MLDSA_POLYW1_PACKEDBYTES_88 (MLDSA_N * MLDSA_POLYW1_PACKED_BITS_88 / 8)
#define MLDSA_POLYW1_PACKEDBYTES_32 (MLDSA_N * MLDSA_POLYW1_PACKED_BITS_32 / 8)

#if MLD_CONFIG_PARAMETER_SET == 44

Expand All @@ -32,6 +36,7 @@
#define MLDSA_CTILDEBYTES 32
#define MLDSA_POLYZ_PACKEDBYTES 576
#define MLDSA_POLYW1_PACKEDBYTES MLDSA_POLYW1_PACKEDBYTES_88
#define MLDSA_POLYW1_PACKED_BITS MLDSA_POLYW1_PACKED_BITS_88
#define MLDSA_POLYETA_PACKEDBYTES 96

#elif MLD_CONFIG_PARAMETER_SET == 65
Expand All @@ -47,6 +52,7 @@
#define MLDSA_CTILDEBYTES 48
#define MLDSA_POLYZ_PACKEDBYTES 640
#define MLDSA_POLYW1_PACKEDBYTES MLDSA_POLYW1_PACKEDBYTES_32
#define MLDSA_POLYW1_PACKED_BITS MLDSA_POLYW1_PACKED_BITS_32
#define MLDSA_POLYETA_PACKEDBYTES 128

#elif MLD_CONFIG_PARAMETER_SET == 87
Expand All @@ -62,6 +68,7 @@
#define MLDSA_CTILDEBYTES 64
#define MLDSA_POLYZ_PACKEDBYTES 640
#define MLDSA_POLYW1_PACKEDBYTES MLDSA_POLYW1_PACKEDBYTES_32
#define MLDSA_POLYW1_PACKED_BITS MLDSA_POLYW1_PACKED_BITS_32
#define MLDSA_POLYETA_PACKEDBYTES 96

#endif /* MLD_CONFIG_PARAMETER_SET == 87 */
Expand Down
51 changes: 51 additions & 0 deletions mldsa/src/poly.c
Original file line number Diff line number Diff line change
Expand Up @@ -1057,6 +1057,57 @@ void mld_polyw1_pack_32(uint8_t r[MLDSA_POLYW1_PACKEDBYTES_32],
|| MLD_CONFIG_PARAMETER_SET == 87 */
#endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */

#if !defined(MLD_CONFIG_NO_SIGN_API)
#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
MLD_INTERNAL_API
void mld_polyw1_unpack_88(mld_poly *r,

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I realize that those have no use prior to the final optimization, but can you still hoist the introduction of the w1 unpacking routines and their CBMC proofs into a separate commit?

const uint8_t a[MLDSA_POLYW1_PACKEDBYTES_88])
{
unsigned int i;

for (i = 0; i < MLDSA_N / 4; ++i)

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Inconsistent use of ++i vs prevailing i++ in the rest of the code base

__loop__(
invariant(i <= MLDSA_N/4)
invariant(array_bound(r->coeffs, 0, i*4, 0, 1 << 6))

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

MLDSA_POLYW1_PACKED_BITS_88

decreases(MLDSA_N / 4 - i))
{
r->coeffs[4 * i + 0] = a[3 * i + 0] & 0x3F;
r->coeffs[4 * i + 1] =
((a[3 * i + 0] >> 6) | ((int32_t)a[3 * i + 1] << 2)) & 0x3F;
r->coeffs[4 * i + 2] =
((a[3 * i + 1] >> 4) | ((int32_t)a[3 * i + 2] << 4)) & 0x3F;
r->coeffs[4 * i + 3] = a[3 * i + 2] >> 2;
}

mld_assert_bound(r->coeffs, MLDSA_N, 0, 1 << 6);
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
*/

#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
(MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
MLD_INTERNAL_API
void mld_polyw1_unpack_32(mld_poly *r,
const uint8_t a[MLDSA_POLYW1_PACKEDBYTES_32])
{
unsigned int i;

for (i = 0; i < MLDSA_N / 2; ++i)

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Inconsistent use of ++i vs prevailing i++ in the rest of the code base

__loop__(
invariant(i <= MLDSA_N/2)
invariant(array_bound(r->coeffs, 0, i*2, 0, 1 << 4))

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

MLDSA_POLYW1_PACKED_BITS_32

decreases(MLDSA_N / 2 - i))
{
r->coeffs[2 * i + 0] = a[i] & 0x0F;
r->coeffs[2 * i + 1] = a[i] >> 4;
}

mld_assert_bound(r->coeffs, MLDSA_N, 0, 1 << 4);
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
|| MLD_CONFIG_PARAMETER_SET == 87 */
#endif /* !MLD_CONFIG_NO_SIGN_API */

#else /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */
MLD_EMPTY_CU(mld_poly)
#endif /* MLD_CONFIG_MULTILEVEL_NO_SHARED */
Expand Down
Loading
Loading