From 6eb23d0bfeb82b9fbebb43fc66a00cdde15c67c2 Mon Sep 17 00:00:00 2001 From: Samuel Neves Date: Wed, 8 Aug 2018 00:44:00 +0100 Subject: curve25519-hacl64: correct u64_gte_mask Remove signed right shifts. Previously u64_gte_mask was only correct for x < 2^63. Z3 script proving correctness: >>> from z3 import * >>> >>> x = BitVec("x", 64) >>> y = BitVec("y", 64) >>> >>> t = LShR(x^((x^y)|((x-y)^y)), 63) - 1 >>> >>> prove(If(UGE(x, y), BitVecVal(-1, 64), BitVecVal(0, 64)) == t) proved Signed-off-by: Samuel Neves Signed-off-by: Jason A. Donenfeld --- src/crypto/curve25519-hacl64.h | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'src') diff --git a/src/crypto/curve25519-hacl64.h b/src/crypto/curve25519-hacl64.h index 5631cde..d2637ac 100644 --- a/src/crypto/curve25519-hacl64.h +++ b/src/crypto/curve25519-hacl64.h @@ -17,9 +17,7 @@ static __always_inline u64 u64_eq_mask(u64 x, u64 y) static __always_inline u64 u64_gte_mask(u64 x, u64 y) { - u64 low63 = ~((u64)((s64)((s64)(x & 0x7fffffffffffffffLLU) - (s64)(y & 0x7fffffffffffffffLLU)) >> 63)); - u64 high_bit = ~((u64)((s64)((s64)(x & 0x8000000000000000LLU) - (s64)(y & 0x8000000000000000LLU)) >> 63)); - return low63 & high_bit; + return ((x ^ ((x ^ y) | ((x - y) ^ y))) >> 63) - 1; } static __always_inline void modulo_carry_top(u64 *b) -- cgit v1.2.3