Repository files navigation

This project implements the Keccak family of sponge functions and relatedconstructions using the SPARK 2014 programming language, with static proofof type safety and good performance.

libkeccak supports the following cryptographic permutations:

• The Keccak-p permutation for state sizes of 25, 50, 100, 200, 400, 800, and 1600 bits (see [1] and [2]).
• The Gimli permutation [7]
• The Ascon permutation [8]

libkeccak implements the following generic constructions which canbe instantiated using the above permutations and with various parameters:

• The Sponge construction
• The Duplex construction
• The MonkeyDuplex construction
• The MonkeyWrap construction
• Hash functions based on the Sponge construction
• eXtendable Output Functions (XOF) based on the Sponge construction
• cSHAKE, KMAC, TupleHash, and ParallelHash as specified in NIST SP 800-185 [4]
• KangarooTwelve as specified by the Keccak team [5]

libkeccak also provides concrete implementations of the above constructions,as specified in [1,4,5,6,7]:

• Hash functions:
  • SHA-3 (224, 256, 384, and 512 bits)
  • Keccak (224, 256, 384, and 512 bits)
  • Gimli-Hash
  • Ascon-Hash
• XOFs:
  • SHAKE128 and SHAKE256
  • RawSHAKE128 and RawSHAKE256
  • Ascon-XOF
• cSHAKE:
  • cSHAKE128 and cSHAKE256
• KMAC:
  • KMAC128 and KMAC256
• TupleHash:
  • TupleHash128 and TupleHash256
• Parallel Hashes:
  • KangarooTwelve
  • MarsupilamiFourteen (256-bit security variant of KangarooTwelve)
  • ParallelHash128 and ParallelHash256
• Authenticated encryption:
  • Ketje (Jr, Sr, Minor, and Major variants)

Note that the difference between a hash function an a XOF function is that ahash function has a fixed output length (for example, 256 bits), whereas theXOFs have arbitrary output length.

The library's algorithms are implemented using Ada's powerful generics. Thisallows for extensive customization and re-use of the various algorithms. Thegeneric Sponge, XOF, and Hash packages can be instantiated for other permutationfunctions (other than just the Keccak permutation). This also permits use ofthis library based on platforms with hardware accelerated implementations ofthe Keccak permutation.

Here's an example of calculating the SHA3-256 hash of a byte array (array oftypeInterfaces.Unsigned_8):

withKeccak.Types;withSHA3;functionCompute_Hash(Data :in Keccak.Types.Byte_Array)return SHA3.SHA3_256.Digest_Typeis   Ctx    : SHA3.SHA3_256.Context;   Digest : SHA3.SHA3_256.Digest_Type;begin   SHA3.SHA3_256.Init(Ctx);   SHA3.SHA3_256.Update(Ctx, Data);   SHA3.SHA3_256.Final(Ctx, Digest);return Digest;endCompute_Hash;

Libkeccak is licensed under the 3-clause BSD license.

Libkeccak requires a GNAT compiler that supports theRelaxed_Initializationaspect, such as GNAT FSF 11 or newer.

Assuming you've cloned this repository and have Alire installed, libkeccakcan be built with the command:

alr build

libkeccak can be built to use SIMD instructions, if your platform supports them,by setting the following GPR variables:

⚠️SSE2 andAVX2 are only available onx86_64 architectures.

EnablingSSE2 will use SSE2 instructions to speed up parallel algorithmssuch as KangarooTwelve and ParallelHash. UsingLIBKECCAK_SIMD=AVX2 will enable theAVX2 instruction set in addition to SSE2.To disable SSE2 and AVX2 on x86_64, setLIBKECCAK_SIMD=none.

⚠️AVX2 is not guaranteed to work on Windows since GCC does not ensure 32-bytestack alignment. SeeGCC Bug #54412

Example:

alr build -- -XLIBKECCAK_ARCH=x86_64 -XLIBKECCAK_SIMD=SSE2

The following performance measurements were taken on an AMD Ryzen 7 5800X on Windows 10.The code was compiled using gnat 11.2.0-4 with the following configuration:

• LIBKECCAK_ARCH=x86_64
• LIBKECCAK_SIMD=AVX2
• All other settings at their default values.

The measurements shown are the output of the benchmark program.

Message size: 524288 bytesPerforming 200 measurements for each testGimli: 379 cyclesGimli Hash: 24.2 cycles/byteAscon (12 rounds): 113 cyclesAscon (8 rounds): 75 cyclesAscon (6 rounds): 74 cyclesAscon-Hash: 17.3 cycles/byteKangarooTwelve (Absorbing): 1.7 cycles/byteKangarooTwelve (Squeezing): 2.9 cycles/byteMarsupilamiFourteen (Absorbing): 2.1 cycles/byteMarsupilamiFourteen (Squeezing): 3.8 cycles/byteParallelHash128 (Absorbing): 2.4 cycles/byteParallelHash128 (Squeezing): 4.9 cycles/byteParallelHash256 (Absorbing): 2.9 cycles/byteParallelHash256 (Squeezing): 6.0 cycles/byteSHA3-224: 6.0 cycles/byteSHA3-256: 6.3 cycles/byteSHA3-384: 8.1 cycles/byteSHA3-512: 11.5 cycles/byteKeccak-224: 6.0 cycles/byteKeccak-256: 6.3 cycles/byteKeccak-384: 8.2 cycles/byteKeccak-512: 11.5 cycles/byteSHAKE128 (Absorbing): 5.2 cycles/byteSHAKE128 (Squeezing): 4.9 cycles/byteSHAKE256 (Absorbing): 6.3 cycles/byteSHAKE256 (Squeezing): 6.0 cycles/byteRawSHAKE128 (Absorbing): 5.2 cycles/byteRawSHAKE128 (Squeezing): 4.9 cycles/byteRawSHAKE256 (Absorbing): 6.3 cycles/byteRawSHAKE256 (Squeezing): 6.0 cycles/byteDuplex r1152c448: 949 cyclesDuplex r1088c512: 949 cyclesDuplex r832c768: 911 cyclesDuplex r576c1024: 911 cyclesKeccak-p[1600,24]: 759 cyclesKeccak-p[1600,24]×2: 1063 cyclesKeccak-p[1600,24]×4: 1063 cyclesKeccak-p[1600,24]×8: 2165 cyclesKeccak-p[1600,12]: 379 cyclesKeccak-p[1600,12]×2: 531 cyclesKeccak-p[1600,12]×4: 531 cyclesKeccak-p[1600,12]×8: 1139 cyclesKeccak-p[800,22]: 683 cyclesKeccak-p[400,20]: 683 cyclesKeccak-p[200,18]: 644 cyclesKeccak-p[100,16]: 799 cyclesKeccak-p[50,14]: 759 cyclesKeccak-p[25,12]: 416 cyclesKetje Jr (AAD): 38.3 cycles/byteKetje Jr (Encrypt): 44.3 cycles/byteKetje Jr (Decrypt): 44.3 cycles/byteKetje Jr (Tag): 44.1 cycles/byteKetje Sr (AAD): 21.7 cycles/byteKetje Sr (Encrypt): 26.9 cycles/byteKetje Sr (Decrypt): 26.9 cycles/byteKetje Sr (Tag): 23.2 cycles/byteKetje Minor (AAD): 4.9 cycles/byteKetje Minor (Encrypt): 8.3 cycles/byteKetje Minor (Decrypt): 8.3 cycles/byteKetje Minor (Tag): 6.5 cycles/byteKetje Major (AAD): 2.7 cycles/byteKetje Major (Encrypt): 4.0 cycles/byteKetje Major (Decrypt): 4.0 cycles/byteKetje Major (Tag): 3.2 cycles/byte

Libkeccak takes a "hybrid verification" approach by combining proof and testing.

The library has an auto-active proof of type safety i.e. that the codeis free of various run-time errors such as:

• use of uninitialised variables;
• integer overflows;
• division by zero;
• value out-of-range;
• out-of-bounds array accesses;
• non-terminating loops.

This achieves the silver level of assurance (absence of run-time errors)described in [9].

All checks are fully proved, except for a few initialisation checkswhich GNATprove's flow analysis cannot automatically verify due to the use ofloops to perform the initialisation.These checks are manually reviewed and suppressed usingpragma Annotate.It is planned to replace these instances withRelaxed_Initialization in thefuture to achieve a fully automatic proof.

The proofs do not extend to functional correctness, i.e. the proofs do notshow that the SHA-3 implementation produces the correct results.Conventional testing is used to provide assurance of the correctness of thealgorithms. The tests consist of Known Answer Tests (KAT) and unit tests.

The KATs comprise the bulk of the tests and provide the assurance that thealgorithms are implemented correctly.

The unit tests aim to cover the cases that are not covered by the KATs, suchas boundary conditions and testing multi-part hashing operations in variouscombinations of lengths.

Assuming you have Alire >= 1.2.0 installed, then:

cd provealrexec -- gnatprove -P../libkeccak -XLIBKECCAK_ARCH=generic -XLIBKECCAK_SIMD=none

💡 Change-XLIBKECCAK_ARCH and-XLIBKECCAK_SIMD to run the proofs usingdifferent SIMD instruction sets.

A summary of the proof results is stored inobj/<arch>_<simd>/gnatprove.out.

The project file configures the prover limits so that they should give the sameresults on all machines.

To see only failed proofs, pass--report=fail to gnatprove.

To run the Known Answer Tests using test vectors:

cd tests/katalr build -- -XLIBKECCAK_ARCH=generic -XLIBKECCAK_SIMD=none./run-all-tests.sh

The test vectors are located in thetests/kat/testvectors/ directory.

To run the unit tests:

cd tests/unit_testsalr build -- -XLIBKECCAK_ARCH=generic -XLIBKECCAK_SIMD=nonealr run

💡 Change-XLIBKECCAK_ARCH and-XLIBKECCAK_SIMD to run the tests usingdifferent SIMD instruction sets.

• [1] NIST FIPS PUB 202 - SHA-3 Standard: Permutation-Based Hash and Extendableoutput Functions. August 2015http://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.202.pdf
• [2] The Keccak Reference Version 3.0. January 2011http://keccak.noekeon.org/Keccak-reference-3.0.pdf
• [3] Cryptographic Sponge Functions Version 0.1. January 2011http://sponge.noekeon.org/CSF-0.1.pdf
• [4] NIST SP 800-185 - SHA-3 Derived Functions: cSHAKE, KMAC, TupleHash, and ParallelHash. December 2016http://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-185.pdf
• [5] KangarooTwelve: fast hashing based on Keccak-phttp://keccak.noekeon.org/kangarootwelve.html
• [6] CAESAR submission: Ketje v2https://keccak.team/files/Ketjev2-doc2.0.pdf
• [7] Gimli: a cross-platform permutationhttps://gimli.cr.yp.to/index.html
• [8] Asconhttps://ascon.iaik.tugraz.at/index.html
• [9] Implementation Guidance for the Adoption of SPARKhttps://www.adacore.com/books/implementation-guidance-spark