From 39bbd00fb3f62d6ee523f03df34464926c05920c Mon Sep 17 00:00:00 2001 From: manastasova Date: Wed, 2 Apr 2025 00:07:50 +0000 Subject: [PATCH 1/2] Type fix in mldsa The resulting array is of type 'int32_t* a', thus, uint32_t aux values t0, t1 cause cbmc proofs to fail due to potentional overflow. --- crypto/fipsmodule/ml_dsa/ml_dsa_ref/poly.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crypto/fipsmodule/ml_dsa/ml_dsa_ref/poly.c b/crypto/fipsmodule/ml_dsa/ml_dsa_ref/poly.c index 456f7b5aa3..adf3db1ce6 100644 --- a/crypto/fipsmodule/ml_dsa/ml_dsa_ref/poly.c +++ b/crypto/fipsmodule/ml_dsa/ml_dsa_ref/poly.c @@ -362,7 +362,7 @@ static unsigned int rej_eta(ml_dsa_params *params, (params->eta == 4)); unsigned int ctr, pos; - uint32_t t0, t1; + int32_t t0, t1; ctr = pos = 0; while(ctr < len && pos < buflen) { From 4d12ec89b3aeefe2deca7cea4aaf7f4c42ab5912 Mon Sep 17 00:00:00 2001 From: manastasova Date: Mon, 7 Apr 2025 21:37:25 +0000 Subject: [PATCH 2/2] Update types based on https://github.com/pq-code-package/mldsa-native/pull/86 --- crypto/fipsmodule/ml_dsa/ml_dsa_ref/poly.c | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/crypto/fipsmodule/ml_dsa/ml_dsa_ref/poly.c b/crypto/fipsmodule/ml_dsa/ml_dsa_ref/poly.c index adf3db1ce6..997e7d2e0b 100644 --- a/crypto/fipsmodule/ml_dsa/ml_dsa_ref/poly.c +++ b/crypto/fipsmodule/ml_dsa/ml_dsa_ref/poly.c @@ -362,7 +362,7 @@ static unsigned int rej_eta(ml_dsa_params *params, (params->eta == 4)); unsigned int ctr, pos; - int32_t t0, t1; + uint32_t t0, t1; ctr = pos = 0; while(ctr < len && pos < buflen) { @@ -372,19 +372,19 @@ static unsigned int rej_eta(ml_dsa_params *params, if (params->eta == 2) { if(t0 < 15) { t0 = t0 - (205*t0 >> 10)*5; - a[ctr++] = 2 - t0; + a[ctr++] = 2 - (int32_t)t0; } if(t1 < 15 && ctr < len) { t1 = t1 - (205*t1 >> 10)*5; - a[ctr++] = 2 - t1; + a[ctr++] = 2 - (int32_t)t1; } } else if (params->eta == 4) { if(t0 < 9) - a[ctr++] = 4 - t0; + a[ctr++] = 4 - (int32_t)t0; if(t1 < 9 && ctr < len) - a[ctr++] = 4 - t1; + a[ctr++] = 4 - (int32_t)t1; } } return ctr;