Description

The file keccak/pad.go contains the function Pad101Bits for in-circuit calculation of the pad10*1 padding that is used for the Keccak hash. See Discussion section ref↗ for a brief description of this padding function.

The signature of the function is as follows:

func Pad101Bits(
	api frontend.API,
	inBits, inLenMin, inLenMax int,
	in []frontend.Variable, inLen frontend.Variable,
) []frontend.Variable

The input that is to be padded is passed as in. As this slice cannot have different lengths for different instances of the same circuit, it must always be of the same length. Thus, the circuit variable inLen contains the number of elements of in that should be considered as the input. Each component of in is not necessarily a single bit but encodes inBits-many bits. The number inBits needs to divide 8 for the function to work properly. Finally, inLenMin and inLenMax contain bounds for inLen, which is used to reduce unnecessary constraints. All lengths in the arguments are counted in terms of components of in, not in bits.

The return slice of circuit variables should be the pad10*1 padded input. As this again must be always of the same length for different instances of the same circuit, the length will be the length necessary for the padded input if the input is of maximum length (inLenMax components of inBits bits each). After the padded input, the remaining components of the return slice will be padded with the dummy value zero.

The function begins by calculating the number of bits of the padded output:

outBitsLen := ((inLenMax*inBits+8)/1088 + 1) * 1088

This formula is incorrect, however, whenever k*1088 - 8 < inLenMax*inBits <= k*1088 - 2 for some k. Take for example inBits = 1 and inLenMax = 1080. Then the above formula yields outBitsLen = 2 * 1088, even though eight bits are enough for the padding, so outBitsLen could be 1088.

A corrected formula would be

outBitsLen := ((inLenMax*inBits+2+1087)/1088) * 1088

Here, we add 2 to account for the padding, and 1087 = 1088 - 1 to ensure the division rounds up.

This mistake in itself only results in the return value of Pad101Bits having excessive length. However, as long as this extra unnecessary block would be filled with dummy zeroes after the real padding ended, this would only amount to an efficiency issue, as long as callers use the correct number of blocks from the result.

However, the analogous mistake also appears later when constructing the actual padding, so the actual padding will be incorrect for inputs in which there is only one byte left to a full round. The code calculating how many rounds to pad to is as follows:

rounds := (actualLen+8)/1088 + 1

Here, actualLen is the number of bits the data is long. If that is 1,080, the result will be 2, even though the data should be padded to only one round, as eight bits are enough for that. The correct formula would be

rounds := (actualLen + 2 + 1087) / 1088

analogously to how it was before.

One can check that the circuit Pad101Bits is indeed incorrect by modifying pad_test.go to use an input that is 1,080 bits long, which can be done by modifying the first couple of lines like this:

chunk := hexutil.MustDecode("0x1234")
-	inLenNibs := 1200
+	inLenNibs = 270
var data []byte
-	for i := 0; i < 300; i++ {
+	for i := 0; i < (inLenNibs / 4); i++ {
	data = append(data, chunk...)
}
var nibs []frontend.Variable
for _, b := range data {
	nibs = append(nibs, b>>4, b&15)
}
for i := len(nibs); i < inLenNibs; i++ {
	nibs = append(nibs, 0)
}

The test will succeed for inLenNibs = 268 (1,072 bits) as well as inLenNibs = 272 (1,088 bits) but fail for inLenNibs = 270 (1,080 bits).

Impact

Whenever k*1088 - 8 < inLenMax*inBits <= k*1088 - 2 for some natural number k, the padded data returned by the function will be incorrect. The Keccak hash calculated using this padding function will thus be incorrect as well for such inputs. The hash function resulting from this padding function combined with the Keccak implementation will still be as secure as a hash function as the correctly padded Keccak is, but the computed hashes will not match the Keccak specification or other implementations that do match the specification.

In Brevis's case, one place where Keccak is used is committing to outputs of app circuits. The Pad101Bits circuit is not used for this use case, however, because the output will always have the same number of bits for a particular circuit, so the padding can be computed out of circuit, as is done in the sdk's commitOutput function in sdk/host_circuit.go.

Hypothetically, should for example commitOutput use the Pad101Bits for padding, then for certain output lengths, the hash exposed as a public circuit variable by the circuit will not match the Keccak specification. Comparing this hash using a specification-conformant implementation of Keccak, for example in a smart contract on chain, would then result in the hashes not matching and, thereby, results that should be recognized as valid not being recognized as such.

However, Pad101Bits is currently not actually used in the in-scope code, except tests.

Recommendations

The calculation of outBitsLen should be corrected,

-outBitsLen := ((inLenMax*inBits+8)/1088 + 1) * 1088
+ outBitsLen := ((inLenMax*inBits+2+1087)/1088) * 1088

similarly for rounds:

-rounds := (actualLen+8)/1088 + 1
+    rounds := (actualLen + 2 + 1087) / 1088

Additionally, the code following the calculation of rounds that inserts the actual padding will also need to be changed to support the situation where the padding fits within one byte. This is because it currently inserts one byte with bits 10000000 (though in reversed order), then inserts some zeroes as necessary, and then the last 1.

One way to do that might be to fill the remaining bits with zero and afterwards overwrite the right bit with 1, so instead of

// insert the padding part
for ; j < actualLen+7; j++ {
	padded[i][j] = 0
}
padded[i][j] = 1
j++
for ; j < rounds*1088-8; j++ {
	padded[i][j] = 0
}
padded[i][j] = 1
j++

// populate the rest with dummy zeros
for ; j < outBitsLen; j++ {
	padded[i][j] = 0
}

do this:

      // populate the rest with zeros
for ; j < outBitsLen; j++ {
	padded[i][j] = 0
}

      // set the padding bits
      padded[i][actualLen + 7] = 1
      padded[i][rounds*1088 - 8] = 1

Remediation

This issue has been acknowledged by Brevis, and fixes were implemented in the following commits:

• 5a281f31↗

• ac16551↗

• fc8fc444↗