|
|
@@ -177,6 +177,45 @@ void EVP_tls_cbc_copy_mac(uint8_t *out, unsigned md_size, |
|
|
|
* + md_size = 256 + 48 (since SHA-384 is the largest hash) = 304. */ |
|
|
|
assert(rotate_offset <= 304); |
|
|
|
|
|
|
|
/* Below is an SMT-LIB2 verification that the Barrett reductions below are |
|
|
|
* correct within this range: |
|
|
|
* |
|
|
|
* (define-fun barrett ( |
|
|
|
* (x (_ BitVec 32)) |
|
|
|
* (mul (_ BitVec 32)) |
|
|
|
* (shift (_ BitVec 32)) |
|
|
|
* (divisor (_ BitVec 32)) ) (_ BitVec 32) |
|
|
|
* (let ((q (bvsub x (bvmul divisor (bvlshr (bvmul x mul) shift))) )) |
|
|
|
* (ite (bvuge q divisor) |
|
|
|
* (bvsub q divisor) |
|
|
|
* q))) |
|
|
|
* |
|
|
|
* (declare-fun x () (_ BitVec 32)) |
|
|
|
* |
|
|
|
* (assert (or |
|
|
|
* (let ( |
|
|
|
* (divisor (_ bv20 32)) |
|
|
|
* (mul (_ bv25 32)) |
|
|
|
* (shift (_ bv9 32)) |
|
|
|
* (limit (_ bv853 32))) |
|
|
|
* |
|
|
|
* (and (bvule x limit) (not (= (bvurem x divisor) |
|
|
|
* (barrett x mul shift divisor))))) |
|
|
|
* |
|
|
|
* (let ( |
|
|
|
* (divisor (_ bv48 32)) |
|
|
|
* (mul (_ bv10 32)) |
|
|
|
* (shift (_ bv9 32)) |
|
|
|
* (limit (_ bv768 32))) |
|
|
|
* |
|
|
|
* (and (bvule x limit) (not (= (bvurem x divisor) |
|
|
|
* (barrett x mul shift divisor))))) |
|
|
|
* )) |
|
|
|
* |
|
|
|
* (check-sat) |
|
|
|
* (get-model) |
|
|
|
*/ |
|
|
|
|
|
|
|
if (md_size == 16) { |
|
|
|
rotate_offset &= 15; |
|
|
|
} else if (md_size == 20) { |
|
|
|