diff options
author | Adam Langley <agl@google.com> | 2014-11-04 22:22:01 +0300 |
---|---|---|
committer | Adam Langley <agl@google.com> | 2014-11-11 00:48:30 +0300 |
commit | 9ed9dae18e54fd50e5fb0a290f1d279fe0f02078 (patch) | |
tree | 34dd9f802746becbff6b9ca62830a0b2673b6a2b /crypto/internal.h | |
parent | a0b74eb241669476aab3cd9771d43695a61a6d12 (diff) |
Update constant-time operations.
(Based on upstream's 42af669ff2754dfbe1dd55a0ab56664f82284dc4)
Change-Id: I4d3954fea7471e274c626483a0dfb9d7b3250b74
Diffstat (limited to 'crypto/internal.h')
-rw-r--r-- | crypto/internal.h | 61 |
1 files changed, 46 insertions, 15 deletions
diff --git a/crypto/internal.h b/crypto/internal.h index e32f4604..5b980d83 100644 --- a/crypto/internal.h +++ b/crypto/internal.h @@ -172,21 +172,45 @@ void OPENSSL_cpuid_setup(void); * c = constant_time_select(lt, a, b); */ /* constant_time_msb returns the given value with the MSB copied to all the - * other bits. Uses the fact that arithmetic shift shifts-in the sign bit. - * However, this is not ensured by the C standard so you may need to replace - * this with something else on odd CPUs. */ + * other bits. */ static inline unsigned int constant_time_msb(unsigned int a) { return (unsigned int)((int)(a) >> (sizeof(int) * 8 - 1)); } /* constant_time_lt returns 0xff..f if a < b and 0 otherwise. */ static inline unsigned int constant_time_lt(unsigned int a, unsigned int b) { - unsigned int lt; - /* Case 1: msb(a) == msb(b). a < b iff the MSB of a - b is set.*/ - lt = ~(a ^ b) & (a - b); - /* Case 2: msb(a) != msb(b). a < b iff the MSB of b is set. */ - lt |= ~a & b; - return constant_time_msb(lt); + /* Consider the two cases of the problem: + * msb(a) == msb(b): a < b iff the MSB of a - b is set. + * msb(a) != msb(b): a < b iff the MSB of b is set. + * + * If msb(a) == msb(b) then the following evaluates as: + * msb(a^((a^b)|((a-b)^a))) == + * msb(a^((a-b) ^ a)) == (because msb(a^b) == 0) + * msb(a^a^(a-b)) == (rearranging) + * msb(a-b) (because ∀x. x^x == 0) + * + * Else, if msb(a) != msb(b) then the following evaluates as: + * msb(a^((a^b)|((a-b)^a))) == + * msb(a^(𝟙 | ((a-b)^a))) == (because msb(a^b) == 1 and 𝟙 + * represents a value s.t. msb(𝟙) = 1) + * msb(a^𝟙) == (because ORing with 1 results in 1) + * msb(b) + * + * + * Here is an SMT-LIB verification of this formula: + * + * (define-fun lt ((a (_ BitVec 32)) (b (_ BitVec 32))) (_ BitVec 32) + * (bvxor a (bvor (bvxor a b) (bvxor (bvsub a b) a))) + * ) + * + * (declare-fun a () (_ BitVec 32)) + * (declare-fun b () (_ BitVec 32)) + * + * (assert (not (= (= #x00000001 (bvlshr (lt a b) #x0000001f)) (bvult a b)))) + * (check-sat) + * (get-model) + */ + return constant_time_msb(a^((a^b)|((a-b)^a))); } /* constant_time_lt_8 acts like |constant_time_lt| but returns an 8-bit mask. */ @@ -196,12 +220,7 @@ static inline uint8_t constant_time_lt_8(unsigned int a, unsigned int b) { /* constant_time_gt returns 0xff..f if a >= b and 0 otherwise. */ static inline unsigned int constant_time_ge(unsigned int a, unsigned int b) { - unsigned int ge; - /* Case 1: msb(a) == msb(b). a >= b iff the MSB of a - b is not set.*/ - ge = ~((a ^ b) | (a - b)); - /* Case 2: msb(a) != msb(b). a >= b iff the MSB of a is set. */ - ge |= a & ~b; - return constant_time_msb(ge); + return ~constant_time_lt(a, b); } /* constant_time_ge_8 acts like |constant_time_ge| but returns an 8-bit mask. */ @@ -211,6 +230,18 @@ static inline uint8_t constant_time_ge_8(unsigned int a, unsigned int b) { /* constant_time_is_zero returns 0xff..f if a == 0 and 0 otherwise. */ static inline unsigned int constant_time_is_zero(unsigned int a) { + /* Here is an SMT-LIB verification of this formula: + * + * (define-fun is_zero ((a (_ BitVec 32))) (_ BitVec 32) + * (bvand (bvnot a) (bvsub a #x00000001)) + * ) + * + * (declare-fun a () (_ BitVec 32)) + * + * (assert (not (= (= #x00000001 (bvlshr (is_zero a) #x0000001f)) (= a #x00000000)))) + * (check-sat) + * (get-model) + */ return constant_time_msb(~a & (a - 1)); } |