Differential testing verifies an application's correct behavior by comparing it against a reference baseline. In addition, this software assurance technique becomes a force multiplier when coupled with a fuzzer.

"Differential Fuzzing" brings multiple advantages to standard "Differential Testing"; namely anomaly detection, automated input creation and coverage-guided input mutation. If we add an automated fuzz test-harness generator/executor into the mix, we can drastically reduce the time to achieve the desired level of software assurance.

However, the main caveat here is that we need a reference model, and this approach will not work for greenfield development. In some cases, a rapid prototyping approach may result in a reference model before a formal implementation, or there may be a standard library that can be referred to. In addition, having a reference model will often be the case during mid-life updates that include software implementation language transitions.

For some time now, we have seen new language adoption as a popular means of achieving security and safety assurance. Here a common approach is to adopt engineering programming languages that focus on safety and security and reimplement the applications previously written in memory-unsafe languages.

In November last year, Daniel King blogged about his adventures rewriting a popular C-based Secure Hash Algorithm 3 (SHA-3) library in the programming language SPARK. Daniel showed how a severe security vulnerability found in the eXtended Keccak Code Package (XKCP), would have been avoided if the library had been developed in SPARK. The SPARK library developed, called libkec­cak, was able to prevent the vul­ner­a­bil­i­ty (or any other runtime error) 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.

As noted in the blog, the aim was to develop Libkeccak to the SPARK silver formal proof analysis level, which guarantees that the scope analyzed is absent of runtime errors. This level of assurance is vital with critical software. However, unless the analysis is taken to a higher level to show proof of key integrity properties or full functional proof of requirements, it does not assure that the application is functionally correct.

Daniel also states that:

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

Therefore, this re-implementation provides a security-hardened library that is proven to be absent of runtime errors. In addition, the functional correctness of the SPARK cryptographic library is argued through unit-testing evidence.

Determining the strength of any functional correctness argument depends on the level of assurance you're trying to achieve, and mechanisms like coverage analysis can be used to bolster claims. However, the fact that the original XKCP library is a reference model for libkeccak immediately presents us with an interesting question:

"Can differential fuzz-testing increase the functional correctness assurance of Libkeccak?"

And because we're a very inquisitive bunch of engineers at AdaCore we set out to find the answer!

This blog describes the processes of setting up, executing and analyzing the results of a differential fuzzing campaign for the Libkeccak and XKCP cryptographic libraries.

The first step in this exploratory journey was to set up a fuzz test development environment that we could use to build and execute Libkeccak tests. Luckily this was a very straightforward process as Libkeccak is available within the Ada LIbrary REpository (ALIRE). ALIRE aims to fulfil a similar role to Rust's cargo or OCaml's opam repositories, and in my opinion, it achieves it. To install and build libkeccak I just needed to clone the repository and execute the command "alr build".

The second step was to understand the Libkeccak API protocol so that I could configure and utilize one of the cryptographic algorithms. For this I just reused the example from the repository readme:

The signature of this test application gave us a good starting point. The Ada type Keccak.Types.Byte_Array is, as the name would suggest, a representation of an array of bytes and, therefore, a data structure well suited to mutational fuzz testing. The final act is to create an Ada package for the test function and include it in the build process.

Step three involved generating a fuzz test harness for our new Compute_Hash function and, as discussed in previous blogs we can utilize the capabilities of GNATfuzz to automate this process.

To verify that the subprogram is fuzzable, we must execute GNATfuzz's "analyze" mode. The command we used is very straight forward:

All we need to do is pass the GPR file of Libkeccak to the analyze mode of GNATfuzz via "-P" switch. This generates a results file identifying all of the "fuzzable" components of the application. Searching through the list, we identified (as expected) that the Compute_Hash function can act as a fuzz test entry point.

To generate the harness, we identified the subprogram ID from the list of fuzzable subprograms that correlated with the Compute_Hash function and ran the following command:

Running the "generate" command concludes this step by successfully (and automatically) creating a complete fuzz test build and execution environment.

At this point, we could immediately run a fuzz test via the GNATfuzz "fuzz" command. However, this would only allow us to fuzz for standard anomaly detection (i.e. runtime constraint check failures and segmentation faults). Ordinarily, this is a valuable assurance activity. However, in this instance, the SPARK analyzer has already formally proven the algorithm absent of runtime errors; therefore, we wouldn't expect the fuzz test to find anything useful.

Step 4 involves configuring the differential aspects of the test and connecting up the equivalent XKCP SHA3 256bit cryptographic algorithm. GNATfuzz simplifies this by generating a "User Configuration" package within the test harness framework that allows you to tailor the fuzz test to meet your specific needs. The actual container is a child Ada package of the hosting package that contains the subprogram under test (in this case, Compute_Hash). This package includes a number of hooks into the GNATfuzz test execute runtime for manipulating the test and the one that plays a key role with differential fuzzing is called "Teardown". Much like the unit test concept of test-teardown, the subprogram is used to free up or reset memory in between test execution. In addition, the GNATfuzz runtime provides this subprogram with the mutated input data and the result of the call to the function under test. In our example the subprogram signature looks like this:

Therefore, to verify the return of the function under test against the reference model, we can feed the same input "GNATfuzz_Data" into the XKCP SHA3 256bit cryptographic algorithm and check that the returned message digest matches the Libkeccak result "GNATfuzz_Return".

As previously stated, XKCP is a library of cryptographic algorithms developed in the programming language C. Therefore, the next job is to create an Ada thin binding to invoke the corresponding C function. The GCC compiler's -fdump-ada-spec switch can help here. To reduce the complexity of the binding the self-contained version of XKCP (CompactFIPS202) was analyzed. The analysis resulted in an Ada package specification that included the following function.

To call the thin binding with the correct values, we need to convert from the Libkeccak Ada types to the C types (via the Ada thin binding). To keep the implementation nice and tidy, we created a "thick binding":

The safe data conversion into the corresponding thin binding types is straightforward. We know the data type sizes are equivalent; therefore, we can safely use instantiations of Ada.Unchecked_Conversion to convert between the two byte array types.

We can now go back and complete the Teardown function:

Now, each time we execute a data mutation through the Compute_Hash function, we are not just checking for anomalies but also verifying the functional correctness against the original XKCP reference model!

To further the work we can easily utilise Ada's powerful generics feature to reuse the thick binding code for all of the algorithms in the XKCP reference model. In order to make the function generic we just need to identify the specific components that are unique to each algorithm, more specifically:

• The return type of the calculated digest
• The size of the digest in bits
• The associated thin binding function

This gives us the following specification:

We can then easily instantiate and call the generic thick binding functions within the TearDown procedure like this:

The actual test then needs to be updated to ensure all of the SHA3 algorithms are called, as follows:

Note that the return type is now a simple record to hold all of the calculated cryptographic digests:

Execution of the differential fuzzing campaign now allows us to compare the results of all of the SHA3 cryptographic algorithms for every data mutation, with a minimal performance overhead.

So, to get back to the original question: "Can differential fuzz-testing increase the functional correctness assurance of Libkeccak?" we need to consider the assurance level achieved through Dan's original work. As stated, the Libkeccak verification suite is made up of 35,982 test vec­tors and 146 unit tests. Therefore our fuzzing campaign should include a target stop rule that complements and improves on these figures. As a demonstration of the capabilities of differential fuzzing we set the stopping rule at 10 times the original test vector size per fuzzing node. This amounts to 360 thousand executions per each of the 15 processor cores available on the test hardware architecture.

This amounts to over 5 million test executions. However, as each processing node is allowed to continue until all of the processing nodes have executed more than 36 thousand mutations, the actual figure will be much higher. This seems like a reasonable demonstration that we've added assurance to the library!

The fuzzing campaign was then executed and the following results observed:

To conclude: after over 11 million test executions through the Libkeccak and XKCP SHA3 cryptographic algorithms, GNATfuzz did not find a single bug. As Libkeccak was developed in SPARK and verified to the Silver level, it was already proven to be absent of runtime errors. In addition, and through the assurance provided by the original Libkeccak verification suite, it had an arguably reasonable proof that the algorithms are functionally correct. However, the additional evidence provided by this differential fuzzing campaign bolsters that claim and allows us to conclude that differential fuzzing can increase software assurance levels.

There is also more that we could do to raise the assurance further:

• Run the campaign for longer
• Run the campaign on more cores
• Utilise the GNATfuzz SHA_Test.GNATFuzz_User_Configuration.User_Provided_Seeds procedure to create a more interesting starting corpus, that varies the length of the byte arrays

In addition, it would be interesting to run the test again but this time use the branch of XKCP that contains the vulnerability Dan mentioned, and see how long it takes the fuzzer to identify CVE-2022-37454.

But that's for another day!

If you're interested in learning more about GNATfuzz, differential fuzzing or just fuzz testing in general please checkout our GNATfuzz webpage or get in touch with me directly.