upstream: https://github.com/mirage/mirage-crypto
ghash_pure: remove dead bmul32 code, clean up
+19
-71
+19
-71
src/ocaml/ghash_pure.ml
+19
-71
src/ocaml/ghash_pure.ml
···
1
1
(** Pure OCaml GHASH (GF(2^128) for AES-GCM).
2
2
3
-
Constant-time implementation using BearSSL's ctmul32 technique:
4
-
carryless multiplication via masked regular multiplication.
3
+
Constant-time shift-and-XOR implementation. All 128 iterations
4
+
execute identical operations regardless of input values.
5
5
No branches on secret data, no lookup tables.
6
6
7
-
Reference: Thomas Pornin, BearSSL ghash_ctmul32.c
8
-
https://bearssl.org/gitweb/?p=BearSSL&a=blob&f=src/hash/ghash_ctmul32.c *)
9
-
10
-
(** Carryless multiply of two 32-bit values, producing a 64-bit result
11
-
stored as two Int32 values (hi, lo).
12
-
13
-
Uses the BearSSL technique: mask inputs to isolate non-adjacent bits,
14
-
then regular multiplication is carryless for those bits. Four such
15
-
multiplications cover all bit positions. *)
16
-
17
-
let bmul32 (x : int) (y : int) : int * int =
18
-
(* We work with native ints. On 64-bit OCaml, int is 63 bits.
19
-
On 32-bit jsoo, int is 32 bits. We only use the low 32 bits. *)
20
-
let x = x land 0xFFFFFFFF in
21
-
let y = y land 0xFFFFFFFF in
22
-
(* Isolate every 4th bit *)
23
-
let x0 = x land 0x11111111 in
24
-
let x1 = x land 0x22222222 in
25
-
let x2 = x land 0x44444444 in
26
-
let x3 = x land 0x88888888 in
27
-
let y0 = y land 0x11111111 in
28
-
let y1 = y land 0x22222222 in
29
-
let y2 = y land 0x44444444 in
30
-
let y3 = y land 0x88888888 in
31
-
(* Multiply non-adjacent bits: no carry between them *)
32
-
(* Use Int32 to avoid overflow on 32-bit targets *)
33
-
let ( * ) a b = Int32.mul (Int32.of_int a) (Int32.of_int b) in
34
-
let ( lxor ) = Int32.logxor in
35
-
let ( land ) = Int32.logand in
36
-
let z0 = (x0 * y0) lxor (x1 * y3) lxor (x2 * y2) lxor (x3 * y1) in
37
-
let z1 = (x0 * y1) lxor (x1 * y0) lxor (x2 * y3) lxor (x3 * y2) in
38
-
let z2 = (x0 * y2) lxor (x1 * y1) lxor (x2 * y0) lxor (x3 * y3) in
39
-
let z3 = (x0 * y3) lxor (x1 * y2) lxor (x2 * y1) lxor (x3 * y0) in
40
-
(* Recombine: mask each contribution to its bit lane *)
41
-
let z0 = z0 land 0x11111111l in
42
-
let z1 = z1 land 0x22222222l in
43
-
let z2 = z2 land 0x44444444l in
44
-
let z3 = z3 land 0x88888888l in
45
-
let lo = z0 lxor z1 lxor z2 lxor z3 in
46
-
let z0h = Int32.shift_right_logical z0 0 in (* already masked *)
47
-
(* The high 32 bits come from the upper halves of the products.
48
-
For 32x32->64 we need the high word. Int32.mul truncates.
49
-
We need to use a different approach for the high bits. *)
50
-
(* Actually: with Int32.mul we only get the low 32 bits. For GF(2^128)
51
-
multiplication we need the full 64-bit product. Let's use the
52
-
Karatsuba approach at 16-bit granularity instead. *)
53
-
ignore (z0h);
54
-
(* Fall back to 16-bit multiply which fits in 32 bits *)
55
-
let lo32 = Int32.to_int lo in
56
-
(0, lo32) (* TODO: implement properly *)
7
+
Reference: BearSSL constant-time technique (Thomas Pornin)
8
+
https://bearssl.org/constanttime.html *)
57
9
58
-
(* Actually, let me use the approach that works on 32-bit: process
59
-
the 128-bit field elements as arrays of bytes, using the
60
-
shift-and-xor algorithm but with all operations unconditional. *)
10
+
(** Constant-time GF(2^128) multiply.
61
11
62
-
(** Constant-time GF(2^128) multiply using shift-and-XOR.
63
-
64
-
All 128 iterations execute the same operations regardless of input.
65
-
The conditional XOR is replaced with a mask: if bit is 1, mask is
66
-
all-ones; if 0, mask is all-zeros. AND with the mask makes the XOR
67
-
a no-op when the bit is 0. *)
68
-
12
+
Conditional operations use arithmetic masks:
13
+
- [(-bit) land 0xff] is [0xFF] when [bit = 1], [0x00] when [bit = 0]
14
+
- AND with the mask makes XOR a no-op when the bit is zero
15
+
- No branch, no table lookup, no data-dependent memory access *)
69
16
let gf128_mul_ct (x : bytes) (h : bytes) : bytes =
70
17
let z = Bytes.make 16 '\x00' in
71
18
let v = Bytes.copy h in
72
19
for i = 0 to 127 do
73
-
(* Constant-time: compute mask from bit i of x *)
74
20
let byte = Char.code (Bytes.get x (i / 8)) in
75
21
let bit = (byte lsr (7 - (i mod 8))) land 1 in
76
-
let mask = (-bit) land 0xff in (* 0xFF if bit=1, 0x00 if bit=0 *)
77
-
(* Conditional XOR: z ^= v & mask *)
22
+
let mask = (-bit) land 0xff in
78
23
for j = 0 to 15 do
79
24
let zj = Char.code (Bytes.get z j) in
80
25
let vj = Char.code (Bytes.get v j) in
81
26
Bytes.set z j (Char.chr (zj lxor (vj land mask)))
82
27
done;
83
-
(* Shift v right by 1, XOR with reduction polynomial if carry *)
84
28
let carry = Char.code (Bytes.get v 15) land 1 in
85
29
for j = 15 downto 1 do
86
30
let vj = Char.code (Bytes.get v j) in
87
31
let vj1 = Char.code (Bytes.get v (j - 1)) in
88
-
Bytes.set v j (Char.chr (((vj lsr 1) lor ((vj1 land 1) lsl 7)) land 0xff))
32
+
Bytes.set v j
33
+
(Char.chr (((vj lsr 1) lor ((vj1 land 1) lsl 7)) land 0xff))
89
34
done;
90
-
Bytes.set v 0 (Char.chr ((Char.code (Bytes.get v 0) lsr 1) land 0xff));
91
-
(* Constant-time conditional XOR with 0xE1 *)
35
+
Bytes.set v 0
36
+
(Char.chr ((Char.code (Bytes.get v 0) lsr 1) land 0xff));
92
37
let reduce_mask = (-carry) land 0xff in
93
38
let v0 = Char.code (Bytes.get v 0) in
94
39
Bytes.set v 0 (Char.chr (v0 lxor (0xe1 land reduce_mask)))
95
40
done;
96
41
z
97
42
98
-
let ghash (key : bytes) (tag : bytes) (data : string) (off : int) (len : int) =
43
+
let ghash (key : bytes) (tag : bytes) (data : string) (off : int)
44
+
(len : int) =
99
45
let h = Bytes.copy key in
100
46
let nblocks = len / 16 in
101
47
for b = 0 to nblocks - 1 do
···
116
62
Bytes.set x i
117
63
(Char.chr
118
64
(Char.code (Bytes.get tag i)
119
-
lxor Char.code (String.get data (off + (nblocks * 16) + i))))
65
+
lxor
66
+
Char.code
67
+
(String.get data (off + (nblocks * 16) + i))))
120
68
done;
121
69
for i = rem to 15 do
122
70
Bytes.set x i (Bytes.get tag i)