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:

The vul­ner­a­bil­i­ty occurs in the XKCP’s SpongeAbsorb func­tion, in KeccakSponge.inc:

Dur­ing the sec­ond call to h.update(), the vari­ables in the above snip­pet have the fol­low­ing types and values:

• size_t dataByteLen = 4294967295
• size_t i = 0
• unsigned int rateInBytes = 144
• unsigned int instance->byteIOIndex = 1

The pur­pose of the if state­ment in the above snip­pet is to clamp the val­ue of partialBlock so that SnP_AddBytes does not write past the end of the instance->state buffer. This check, how­ev­er, is bypassed due to an unsigned inte­ger over­flow in the expres­sion partialBlock + instance->byteIOIndex, where the result wraps to zero. The sub­se­quent com­par­i­son against rateInBytes then eval­u­ates to false and so partialBlock is not clamped to a suit­able length. The large val­ue of partialBytes, 4294967295, is then passed to SnP_AddBytes which writes past the end of the buffer.

A small vari­ant of the code caus­es an infi­nite loop by replac­ing 4294967295 with 4294967296. This occurs due to cast­ing a 64-bit size_t val­ue to a 32-bit unsigned int which is too small to hold the value.

Nicky notes in their con­clu­sion that:

The vul­ner­a­ble code was released in Jan­u­ary 2011, so it took well over a decade for this vul­ner­a­bil­i­ty to be found. It appears to be dif­fi­cult to find vul­ner­a­bil­i­ties in cryp­to­graph­ic imple­men­ta­tions, even though they play a crit­i­cal role in the over­all secu­ri­ty of a system. 

With SPARK, these kinds of edge cas­es can be found much ear­li­er. By lever­ag­ing SPARK’s proof capa­bil­i­ties, we can demon­strate absence of run­time errors that can lead to these kinds of vul­ner­a­bil­i­ties such as inte­ger over­flow, buffer over­flow, and ter­mi­na­tion of loops.

SHA‑3 in SPARK #

In August 2015, NIST select­ed Kec­cak as the win­ner of the SHA‑3 com­pe­ti­tion. In that same month I start­ed the libkec­cak library to imple­ment SHA‑3 and relat­ed algo­rithms in SPARK. The SPARK 2014 ver­sion of the lan­guage had been released the pre­vi­ous year, and being inspired by pre­vi­ous work where the SKEIN hash func­tion had been imple­ment­ed in SPARK I want­ed to achieve the same for SHA‑3.

The goal of using SPARK for this project was to for­mal­ly ver­i­fy the cor­rect­ness of the code at the sil­ver lev­el of assur­ance using the GNAT­prove for­mal ver­i­fi­ca­tion tool. The sil­ver lev­el of SPARK usage gives strong guar­an­tees that the library:

• nev­er reads unini­tial­ized data,
• access­es glob­al data only as intended,
• does not con­tain any run­time errors (e.g., inte­ger over­flows, divi­sion by zero, or buffer overflows),
• respects key integri­ty prop­er­ties (e.g., type invari­ants and pred­i­cates are nev­er violated),
• func­tion­al prop­er­ties expressed in con­tracts are respected.

The library does not attempt to use proof to show that the cryp­to­graph­ic algo­rithms are imple­ment­ed cor­rect­ly. Instead, it is test­ed against 35,982 test vec­tors and 146 unit tests to ver­i­fy that the library pro­duces the cor­rect results for each of the sup­port­ed algorithms. 

Prov­ing Absence of Vul­ner­a­bil­i­ties #

The vul­ner­a­bil­i­ty in XKCP was an inte­ger over­flow in the SpongeAbsorb func­tion, which then lead to either a buffer over­flow or an infi­nite loop. Libkec­cak is able to avoid these vul­ner­a­bil­i­ties by lever­ag­ing SPARK’s proof capa­bil­i­ties to prove that run­time errors can­not occur for any pos­si­ble input to the library.

To see how libkec­cak avoids the same vul­ner­a­bil­i­ty, let’s look at the code equiv­a­lent to the vul­ner­a­ble SpongeAbsorb code from the XKCP. In libkec­cak, this is the inner loop in the Keccak.Generic_Sponge.Absorb procedure:

To prove that this code does not con­tain run­time errors, GNAT­prove gen­er­ates ver­i­fi­ca­tion con­di­tions (VCs) for each code con­struct that could poten­tial­ly lead to an error. For exam­ple, over­flow checks for arith­metic oper­a­tions, bounds checks for array access­es, and an asser­tion check that the Loop_Invariant is always true.

Each VC is a log­i­cal for­mu­la, which if proved true means that the code con­struct is cor­rect and can­not lead to a run­time error. These VCs are sent to auto­mat­ic the­o­rem provers such as Z3, CVC4, and alt-ergo which answer ​“yes” or ​“no” as to whether the for­mu­la is true. If a prover answers ​“yes”, then the VC is valid and we know that the cor­re­spond­ing run­time error can­not occur.

For exam­ple, the fol­low­ing VC is gen­er­at­ed for the addi­tion Offset + Ctx.Rate (near the end of the above loop) to ver­i­fy that the result of the addi­tion 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 valid­i­ty of this VC, the provers need addi­tion­al infor­ma­tion about the poten­tial val­ues that Offset and Ctx.Rate could have at this point in the pro­gram. This infor­ma­tion is pro­vid­ed by GNAT­prove and includes:

• the pos­si­ble range of val­ues the vari­ables could have based on their data types, e.g., Offset is of type Natural which has the range 0 .. 2147483647,
• the code paths lead­ing up to the VC, e.g., the loop con­di­tion Remaining_Bits >= Initial_Bit_Rate is true when this VC is reached,
• sub­pro­gram con­tracts (e.g., pre­con­di­tions and postconditions),
• VCs in the code paths lead­ing to the check. In this exam­ple, the Loop_Invariant adds extra infor­ma­tion about how the val­ue of Offset relates to oth­er vari­ables which helps con­strain the range of pos­si­ble values.

In this exam­ple, the provers are able to use this infor­ma­tion to auto­mat­i­cal­ly deter­mine that Offset can­not exceed 2147483647 - 199 and Ctx.Rate can­not exceed 199, so the addi­tion nev­er leads to an overflow.

In total, GNAT­prove emits 89 VCs for the Absorb sub­pro­gram, all of which are auto­mat­i­cal­ly proved true. This proof pro­vides assur­ance that this code does not have the same vul­ner­a­bil­i­ties as the XKCP for any pos­si­ble com­bi­na­tion of inputs into the subprogram:

• the arith­metic oper­a­tions nev­er overflow,
• the Data and Ctx.Block arrays are always accessed with­in their bounds,
• the while loop always ter­mi­nates (thanks to the Loop_Variant).

Prov­ing Libkec­cak #

All code in libkec­cak is imple­ment­ed in SPARK and proved at the sil­ver lev­el. The entire proof takes about 15 min­utes to com­plete on my 8‑core machine, and there are 21,689 VCs in total. The GNAT­prove report shows the break­down of these VCs:

Out of all these checks, 78 ini­tial­iza­tion checks required man­u­al review and jus­ti­fi­ca­tion. This was due to a lim­i­ta­tion of ear­li­er ver­sions of the SPARK tools where the flow analy­sis could not han­dle cas­es where arrays were ini­tial­ized via loops. This lim­i­ta­tion has been relaxed in recent ver­sions of SPARK with the intro­duc­tion of the Relaxed_Initialization aspect. Libkec­cak could be updat­ed in a future ver­sion to replace these man­u­al jus­ti­fi­ca­tions with proof using Relaxed_Initialization to achieve a ful­ly auto­mat­ic proof.

Over­all, these proofs give high con­fi­dence that all code in libkec­cak is free from the vul­ner­a­bil­i­ties that have been found in C imple­men­ta­tions such as the XKCP.