Re: [PATCH] crypto : ecc - Fix carry overflow in vli multiplication

[Stefan Berger]

On 5/8/26 7:48 AM, Anastasia Tishchenko wrote:
> The carry flag calculation fails when r01.m_high is saturated
> (0xFFFFFFFFFFFFFFFF) and addition of lower bits overflows.
>
> The condition (r01.m_high < product.m_high) doesn't handle the case
> where r01.m_high == product.m_high and an additional carry exists
> from lower-bit overflow.
>
> Add proper handling for this boundary by accounting for the carry
> from the lower addition.
>
> This issue was discovered during formal verification of ECC functions.

Thanks!

> Signed-off-by: Anastasia Tishchenko <sv3iry@xxxxxxxxx>
> ---
>   crypto/ecc.c | 10 ++++++++--
>   1 file changed, 8 insertions(+), 2 deletions(-)
>
> diff --git a/crypto/ecc.c b/crypto/ecc.c
> index 43b0def3a225..dfe96471407c 100644
> --- a/crypto/ecc.c
> +++ b/crypto/ecc.c
> @@ -427,7 +427,10 @@ static void vli_mult(u64 *result, const u64 *left, const u64 *right,
>   			product = mul_64_64(left[i], right[k - i]);
>   
>   			r01 = add_128_128(r01, product);
> -			r2 += (r01.m_high < product.m_high);

Maybe the following or something like lt_128(r01, product) would be 
'better' replacing 'r01 < product':

if (cmp_128(r01, product) < 0)
    r2++;

/* Compare two uint128_t; returns -1 if a<b, 0 if a == b, 1 otherwise */
static int cmp_128(uint128_t a, uint128_t b)
{
    if (a.m_high < b.m_high)
       return -1;
    if (a.m_high > b.m_high)
       return 1;
    if (a.m_low < b.m_low)
       return -1;
    if (a.m_low > b.m_low)
       return 1;
    return 0;
}



/* r01 < product */
if (lt_128(r01, product))
    r2++;

/* Check a < b; return 1 if a < b, 0 otherwise */
static int lt_128(uint128_t a, uint128_t b)
{
    if (a.m_high < b.m_high)
       return 1;
    if (a.m_high > b.m_high)
       return 0;
    if (a.m_low < b.m_low)
       return 1;
    return 0;
}

> +			if (r01.m_high != product.m_high)
> +				r2 += (r01.m_high < product.m_high);
> +			else
> +				r2 += (r01.m_low < product.m_low);
>   		}
>   
>   		result[k] = r01.m_low;
> @@ -488,7 +491,10 @@ static void vli_square(u64 *result, const u64 *left, unsigned int ndigits)
>   			}
>   
>   			r01 = add_128_128(r01, product);
> -			r2 += (r01.m_high < product.m_high);
> +			if (r01.m_high != product.m_high)
> +				r2 += (r01.m_high < product.m_high);
> +			else
> +				r2 += (r01.m_low < product.m_low);
>   		}
>   
>   		result[k] = r01.m_low;