# Avoiding Vulnerabilities in Crypto Code with SPARK

## by Daniel King –

Writing secure software in C is hard. It takes just one missed edge case to lead to a serious security vulnerability, and finding such edge cases is difficult. This blog post discusses a recent vulnerability in a popular SHA-3 library and how the same problems were avoided in my own SHA-3 library written in SPARK.

# The Vulnerability

The vulnerability is a buffer overflow in the eXtended Keccak Code Package (XKCP), recently discovered by Nicky Mouha and assigned CVE-2022-37454. The XKCP is a reference implementation of SHA-3 by its designers, written in C with some assembly for several platforms. It is used by several other projects such as the Python and PHP scripting languages, which are also impacted by the vulnerability.

Let's take a look into how the vulnerability occurs. Nicky's announcement provides a simple example of triggering the buffer overflow from some Python code:

` ````
import hashlib
h = hashlib.sha3_224()
h.update(b"\x00" * 1)
h.update(b"\x00" * 4294967295)
print(h.hexdigest())
```

The vulnerability occurs in the XKCP’s `SpongeAbsorb`

function, in KeccakSponge.inc:

` ````
partialBlock = (unsigned int)(dataByteLen - i);
if (partialBlock + instance->byteIOIndex > rateInBytes)
partialBlock = rateInBytes - instance->byteIOIndex;
SnP_AddBytes(instance->state, curData, instance->byteIOIndex, partialBlock);
```

During the second call to `h.update()`

, the variables in the above snippet have the following types and values:

`size_t dataByteLen = 4294967295`

`size_t i = 0`

`unsigned int rateInBytes = 144`

`unsigned int instance->byteIOIndex = 1`

The purpose of the `if`

statement in the above snippet is to clamp the value of `partialBlock`

so that `SnP_AddBytes`

does not write past the end of the `instance->state`

buffer. This check, however, is bypassed due to an unsigned integer overflow in the expression `partialBlock + instance->byteIOIndex`

, where the result wraps to zero. The subsequent comparison against `rateInBytes`

then evaluates to `false`

and so `partialBlock`

is not clamped to a suitable length. The large value of `partialBytes`

, 4294967295, is then passed to `SnP_AddBytes`

which writes past the end of the buffer.

A small variant of the code causes an infinite loop by replacing 4294967295 with 4294967296. This occurs due to casting a 64-bit `size_t`

value to a 32-bit `unsigned int`

which is too small to hold the value.

Nicky notes in their conclusion that:

The vulnerable code was released in January 2011, so it took well over a decade for this vulnerability to be found. It appears to be difficult to find vulnerabilities in cryptographic implementations, even though they play a critical role in the overall security of a system.

With SPARK, these kinds of edge cases can be found much earlier. By leveraging SPARK’s proof capabilities, we can demonstrate absence of runtime errors that can lead to these kinds of vulnerabilities such as integer overflow, buffer overflow, and termination of loops.

# SHA‑3 in SPARK #

In August 2015, NIST selected Keccak as the winner of the SHA‑3 competition. In that same month I started the libkeccak library to implement SHA‑3 and related algorithms in SPARK. The SPARK 2014 version of the language had been released the previous year, and being inspired by previous work where the SKEIN hash function had been implemented in SPARK I wanted to achieve the same for SHA‑3.

The goal of using SPARK for this project was to formally verify the correctness of the code at the silver level of assurance using the GNATprove formal verification tool. The silver level of SPARK usage gives strong guarantees that the library:

- never reads uninitialized data,
- accesses global data only as intended,
- does not contain any runtime errors (e.g., integer overflows, division by zero, or buffer overflows),
- respects key integrity properties (e.g., type invariants and predicates are never violated),
- functional properties expressed in contracts are respected.

The library does not attempt to use proof to show that the cryptographic algorithms are implemented correctly. Instead, it is tested against 35,982 test vectors and 146 unit tests to verify that the library produces the correct results for each of the supported algorithms.

## Proving Absence of Vulnerabilities #

The vulnerability in XKCP was an integer overflow in the `SpongeAbsorb`

function, which then lead to either a buffer overflow or an infinite loop. Libkeccak is able to avoid these vulnerabilities by leveraging SPARK’s proof capabilities to prove that runtime errors cannot occur for any possible input to the library.

To see how libkeccak avoids the same vulnerability, let’s look at the code equivalent to the vulnerable `SpongeAbsorb`

code from the XKCP. In libkeccak, this is the inner loop in the `Keccak.Generic_Sponge.Absorb`

procedure:

` ````
-- Process complete blocks
while Remaining_Bits >= Initial_Bit_Rate loop
pragma Loop_Invariant (Offset + Remaining_Bytes = Initial_Data_Len
and Remaining_Bytes <= Data'Length
and Remaining_Bytes = (Remaining_Bits + 7) / 8
and (Bit_Length mod 8) = (Remaining_Bits mod 8)
and Ctx.Curr_State = Absorbing
and Rate_Of (Ctx) = Initial_Bit_Rate);
pragma Loop_Variant (Decreases => Remaining_Bytes,
Decreases => Remaining_Bits,
Increases => Offset);
XOR_Bits_Into_State (Ctx.State,
Data (Data'First + Offset ..
Data'First + Offset + (Ctx.Rate - 1)),
Initial_Bit_Rate);
Permute (Ctx.State);
Offset := Offset + Ctx.Rate;
Remaining_Bytes := Remaining_Bytes - Ctx.Rate;
Remaining_Bits := Remaining_Bits - Initial_Bit_Rate;
end loop;
-- No more complete blocks. Store the leftovers
if Remaining_Bits > 0 then
Ctx.Block (0 .. Remaining_Bytes - 1)
:= Data (Data'First + Offset ..
Data'First + (Offset + (Remaining_Bytes - 1)));
end if;
```

To prove that this code does not contain runtime errors, GNATprove generates *verification conditions* (VCs) for each code construct that could potentially lead to an error. For example, overflow checks for arithmetic operations, bounds checks for array accesses, and an assertion check that the `Loop_Invariant`

is always true.

Each VC is a logical formula, which if proved true means that the code construct is correct and cannot lead to a runtime error. These VCs are sent to automatic theorem provers such as Z3, CVC4, and alt-ergo which answer “yes” or “no” as to whether the formula is true. If a prover answers “yes”, then the VC is valid and we know that the corresponding runtime error cannot occur.

For example, the following VC is generated for the addition `Offset + Ctx.Rate`

(near the end of the above loop) to verify that the result of the addition does not exceed the bounds of the datatype `Natural`

, which has an upper bound of 2147483647:

```
Offset + Ctx.Rate <= 2147483647
```

To be able to prove the validity of this VC, the provers need additional information about the potential values that `Offset`

and `Ctx.Rate`

could have at this point in the program. This information is provided by GNATprove and includes:

- the possible range of values the variables could have based on their data types, e.g.,
`Offset`

is of type`Natural`

which has the range`0 .. 2147483647`

, - the code paths leading up to the VC, e.g., the loop condition
`Remaining_Bits >= Initial_Bit_Rate`

is true when this VC is reached, - subprogram contracts (e.g., preconditions and postconditions),
- VCs in the code paths leading to the check. In this example, the
`Loop_Invariant`

adds extra information about how the value of`Offset`

relates to other variables which helps constrain the range of possible values.

In this example, the provers are able to use this information to automatically determine that `Offset`

cannot exceed `2147483647 - 199`

and `Ctx.Rate`

cannot exceed `199`

, so the addition never leads to an overflow.

In total, GNATprove emits 89 VCs for the `Absorb`

subprogram, all of which are automatically proved true. This proof provides assurance that this code does not have the same vulnerabilities as the XKCP for any possible combination of inputs into the subprogram:

- the arithmetic operations never overflow,
- the
`Data`

and`Ctx.Block`

arrays are always accessed within their bounds, - the
`while`

loop always terminates (thanks to the`Loop_Variant`

).

## Proving Libkeccak #

All code in libkeccak is implemented in SPARK and proved at the silver level. The entire proof takes about 15 minutes to complete on my 8‑core machine, and there are 21,689 VCs in total. The GNATprove report shows the breakdown of these VCs:

` ````
-------------------------------------------------------------------------------------------------------------------------------------
SPARK Analysis results Total Flow CodePeer Provers Justified Unproved
-------------------------------------------------------------------------------------------------------------------------------------
Data Dependencies 899 899 . . . .
Flow Dependencies 371 371 . . . .
Initialization 5069 4991 . . 78 .
Non-Aliasing 232 232 . . . .
Run-time Checks 11423 . . 11423 (CVC4 99%, Z3 1%, altergo 0%) . .
Assertions 1405 . . 1405 (CVC4 96%, Trivial 1%, Z3 2%, altergo 0%) . .
Functional Contracts 2176 . . 2176 (CVC4 100%, Z3 0%) . .
LSP Verification . . . . . .
Termination 114 . . 114 (CVC4) . .
Concurrency . . . . . .
-------------------------------------------------------------------------------------------------------------------------------------
Total 21689 6493 (30%) . 15118 (70%) 78 (0%) .
```

Out of all these checks, 78 initialization checks required manual review and justification. This was due to a limitation of earlier versions of the SPARK tools where the flow analysis could not handle cases where arrays were initialized via loops. This limitation has been relaxed in recent versions of SPARK with the introduction of the `Relaxed_Initialization`

aspect. Libkeccak could be updated in a future version to replace these manual justifications with proof using `Relaxed_Initialization`

to achieve a fully automatic proof.

Overall, these proofs give high confidence that all code in libkeccak is free from the vulnerabilities that have been found in C implementations such as the XKCP.