AdaCore Blog

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 vul­ner­a­bil­i­ty occurs in the XKCP’s SpongeAbsorb func­tion, 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);

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.

SHA3 in SPARK #

In August 2015, NIST select­ed Kec­cak as the win­ner of the SHA3 com­pe­ti­tion. In that same month I start­ed the libkec­cak library to imple­ment SHA3 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 SHA3.

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:

--  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 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:

-------------------------------------------------------------------------------------------------------------------------------------
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 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.

Posted in #Security    #SPARK    #Cryptography    #Formal Verification   

About Daniel King

Daniel King

Daniel King is a Senior Embedded Software Engineer currently working in the IoT security industry. He enjoys using Ada and SPARK in his open source projects for embedded systems and cryptography.