From 418466250b0a2f608045627aef5470d9a8def640 Mon Sep 17 00:00:00 2001 From: armfazh Date: Mon, 16 Oct 2023 16:41:23 -0700 Subject: [PATCH 01/18] zeta: updating format rule and removing linter rule. --- zeta/.clang-format | 2 +- zeta/Makefile | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/zeta/.clang-format b/zeta/.clang-format index 8c826f32067e9..72d680c57861b 100644 --- a/zeta/.clang-format +++ b/zeta/.clang-format @@ -675,7 +675,7 @@ SpaceBeforeInheritanceColon: true SpaceBeforeParens: ControlStatementsExceptForEachMacros SpaceBeforeRangeBasedForLoopColon: true SpaceInEmptyParentheses: false -SpacesBeforeTrailingComments: 1 +SpacesBeforeTrailingComments: 2 SpacesInAngles: false SpacesInContainerLiterals: false SpacesInCStyleCastParentheses: false diff --git a/zeta/Makefile b/zeta/Makefile index c16b40572124c..4e0d502ee7806 100644 --- a/zeta/Makefile +++ b/zeta/Makefile @@ -28,4 +28,4 @@ format: check-env lint: check-env # Tested with cpplint v1.5.5 - cpplint --filter=-whitespace/braces,-readability/casting ${ALL_FILES} + cpplint --filter=-whitespace/braces,-readability/casting,-build/include_subdir ${ALL_FILES} From 7ac92cec892e95ef3d2cd9325ce856946915fdbc Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Thu, 5 Oct 2023 14:54:13 +0200 Subject: [PATCH 02/18] HACL SHA2 code --- crypto/hacl_hash.h | 392 +++++++++++++++ crypto/hacl_lib.h | 231 +++++++++ crypto/sha2-hacl-generated.c | 939 +++++++++++++++++++++++++++++++++++ crypto/sha2-hacl.c | 187 +++++++ 4 files changed, 1749 insertions(+) create mode 100644 crypto/hacl_hash.h create mode 100644 crypto/hacl_lib.h create mode 100644 crypto/sha2-hacl-generated.c create mode 100644 crypto/sha2-hacl.c diff --git a/crypto/hacl_hash.h b/crypto/hacl_hash.h new file mode 100644 index 0000000000000..38901e36dbe8c --- /dev/null +++ b/crypto/hacl_hash.h @@ -0,0 +1,392 @@ +/* + * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation + * Copyright (c) 2022-2023 HACL* Contributors + * Copyright (c) 2023 Cryspen + */ + +#ifndef CRYPTO_HACL_HASH_H_ +#define CRYPTO_HACL_HASH_H_ + +#include "./hacl_lib.h" + +#define Spec_Hash_Definitions_SHA2_224 0 +#define Spec_Hash_Definitions_SHA2_256 1 +#define Spec_Hash_Definitions_SHA2_384 2 +#define Spec_Hash_Definitions_SHA2_512 3 +#define Spec_Hash_Definitions_SHA1 4 +#define Spec_Hash_Definitions_MD5 5 +#define Spec_Hash_Definitions_Blake2S 6 +#define Spec_Hash_Definitions_Blake2B 7 +#define Spec_Hash_Definitions_SHA3_256 8 +#define Spec_Hash_Definitions_SHA3_224 9 +#define Spec_Hash_Definitions_SHA3_384 10 +#define Spec_Hash_Definitions_SHA3_512 11 +#define Spec_Hash_Definitions_Shake128 12 +#define Spec_Hash_Definitions_Shake256 13 + +typedef uint8_t Spec_Hash_Definitions_hash_alg; + +#define Hacl_Streaming_Types_Success 0 +#define Hacl_Streaming_Types_InvalidAlgorithm 1 +#define Hacl_Streaming_Types_InvalidLength 2 +#define Hacl_Streaming_Types_MaximumLengthExceeded 3 + +uint32_t Hacl_Hash_Definitions_word_len(Spec_Hash_Definitions_hash_alg a); + +uint32_t Hacl_Hash_Definitions_block_len(Spec_Hash_Definitions_hash_alg a); + +uint32_t Hacl_Hash_Definitions_hash_word_len(Spec_Hash_Definitions_hash_alg a); + +uint32_t Hacl_Hash_Definitions_hash_len(Spec_Hash_Definitions_hash_alg a); + +typedef uint8_t *Hacl_Hash_Definitions_hash_t; + +typedef uint8_t Hacl_Streaming_Types_error_code; + +typedef struct Hacl_Streaming_MD_state_32_s { + uint32_t *block_state; + uint8_t *buf; + uint64_t total_len; +} Hacl_Streaming_MD_state_32; + +typedef struct Hacl_Streaming_MD_state_64_s { + uint64_t *block_state; + uint8_t *buf; + uint64_t total_len; +} Hacl_Streaming_MD_state_64; + +static const uint32_t Hacl_Impl_SHA2_Generic_h224[8U] = { + (uint32_t)0xc1059ed8U, (uint32_t)0x367cd507U, (uint32_t)0x3070dd17U, + (uint32_t)0xf70e5939U, (uint32_t)0xffc00b31U, (uint32_t)0x68581511U, + (uint32_t)0x64f98fa7U, (uint32_t)0xbefa4fa4U +}; + +static const uint32_t Hacl_Impl_SHA2_Generic_h256[8U] = { + (uint32_t)0x6a09e667U, (uint32_t)0xbb67ae85U, (uint32_t)0x3c6ef372U, + (uint32_t)0xa54ff53aU, (uint32_t)0x510e527fU, (uint32_t)0x9b05688cU, + (uint32_t)0x1f83d9abU, (uint32_t)0x5be0cd19U +}; + +static const uint64_t Hacl_Impl_SHA2_Generic_h384[8U] = { + (uint64_t)0xcbbb9d5dc1059ed8U, (uint64_t)0x629a292a367cd507U, + (uint64_t)0x9159015a3070dd17U, (uint64_t)0x152fecd8f70e5939U, + (uint64_t)0x67332667ffc00b31U, (uint64_t)0x8eb44a8768581511U, + (uint64_t)0xdb0c2e0d64f98fa7U, (uint64_t)0x47b5481dbefa4fa4U +}; + +static const uint64_t Hacl_Impl_SHA2_Generic_h512[8U] = { + (uint64_t)0x6a09e667f3bcc908U, (uint64_t)0xbb67ae8584caa73bU, + (uint64_t)0x3c6ef372fe94f82bU, (uint64_t)0xa54ff53a5f1d36f1U, + (uint64_t)0x510e527fade682d1U, (uint64_t)0x9b05688c2b3e6c1fU, + (uint64_t)0x1f83d9abfb41bd6bU, (uint64_t)0x5be0cd19137e2179U +}; + +static const uint32_t Hacl_Impl_SHA2_Generic_k224_256[64U] = { + (uint32_t)0x428a2f98U, (uint32_t)0x71374491U, (uint32_t)0xb5c0fbcfU, + (uint32_t)0xe9b5dba5U, (uint32_t)0x3956c25bU, (uint32_t)0x59f111f1U, + (uint32_t)0x923f82a4U, (uint32_t)0xab1c5ed5U, (uint32_t)0xd807aa98U, + (uint32_t)0x12835b01U, (uint32_t)0x243185beU, (uint32_t)0x550c7dc3U, + (uint32_t)0x72be5d74U, (uint32_t)0x80deb1feU, (uint32_t)0x9bdc06a7U, + (uint32_t)0xc19bf174U, (uint32_t)0xe49b69c1U, (uint32_t)0xefbe4786U, + (uint32_t)0x0fc19dc6U, (uint32_t)0x240ca1ccU, (uint32_t)0x2de92c6fU, + (uint32_t)0x4a7484aaU, (uint32_t)0x5cb0a9dcU, (uint32_t)0x76f988daU, + (uint32_t)0x983e5152U, (uint32_t)0xa831c66dU, (uint32_t)0xb00327c8U, + (uint32_t)0xbf597fc7U, (uint32_t)0xc6e00bf3U, (uint32_t)0xd5a79147U, + (uint32_t)0x06ca6351U, (uint32_t)0x14292967U, (uint32_t)0x27b70a85U, + (uint32_t)0x2e1b2138U, (uint32_t)0x4d2c6dfcU, (uint32_t)0x53380d13U, + (uint32_t)0x650a7354U, (uint32_t)0x766a0abbU, (uint32_t)0x81c2c92eU, + (uint32_t)0x92722c85U, (uint32_t)0xa2bfe8a1U, (uint32_t)0xa81a664bU, + (uint32_t)0xc24b8b70U, (uint32_t)0xc76c51a3U, (uint32_t)0xd192e819U, + (uint32_t)0xd6990624U, (uint32_t)0xf40e3585U, (uint32_t)0x106aa070U, + (uint32_t)0x19a4c116U, (uint32_t)0x1e376c08U, (uint32_t)0x2748774cU, + (uint32_t)0x34b0bcb5U, (uint32_t)0x391c0cb3U, (uint32_t)0x4ed8aa4aU, + (uint32_t)0x5b9cca4fU, (uint32_t)0x682e6ff3U, (uint32_t)0x748f82eeU, + (uint32_t)0x78a5636fU, (uint32_t)0x84c87814U, (uint32_t)0x8cc70208U, + (uint32_t)0x90befffaU, (uint32_t)0xa4506cebU, (uint32_t)0xbef9a3f7U, + (uint32_t)0xc67178f2U +}; + +static const uint64_t Hacl_Impl_SHA2_Generic_k384_512[80U] = { + (uint64_t)0x428a2f98d728ae22U, (uint64_t)0x7137449123ef65cdU, + (uint64_t)0xb5c0fbcfec4d3b2fU, (uint64_t)0xe9b5dba58189dbbcU, + (uint64_t)0x3956c25bf348b538U, (uint64_t)0x59f111f1b605d019U, + (uint64_t)0x923f82a4af194f9bU, (uint64_t)0xab1c5ed5da6d8118U, + (uint64_t)0xd807aa98a3030242U, (uint64_t)0x12835b0145706fbeU, + (uint64_t)0x243185be4ee4b28cU, (uint64_t)0x550c7dc3d5ffb4e2U, + (uint64_t)0x72be5d74f27b896fU, (uint64_t)0x80deb1fe3b1696b1U, + (uint64_t)0x9bdc06a725c71235U, (uint64_t)0xc19bf174cf692694U, + (uint64_t)0xe49b69c19ef14ad2U, (uint64_t)0xefbe4786384f25e3U, + (uint64_t)0x0fc19dc68b8cd5b5U, (uint64_t)0x240ca1cc77ac9c65U, + (uint64_t)0x2de92c6f592b0275U, (uint64_t)0x4a7484aa6ea6e483U, + (uint64_t)0x5cb0a9dcbd41fbd4U, (uint64_t)0x76f988da831153b5U, + (uint64_t)0x983e5152ee66dfabU, (uint64_t)0xa831c66d2db43210U, + (uint64_t)0xb00327c898fb213fU, (uint64_t)0xbf597fc7beef0ee4U, + (uint64_t)0xc6e00bf33da88fc2U, (uint64_t)0xd5a79147930aa725U, + (uint64_t)0x06ca6351e003826fU, (uint64_t)0x142929670a0e6e70U, + (uint64_t)0x27b70a8546d22ffcU, (uint64_t)0x2e1b21385c26c926U, + (uint64_t)0x4d2c6dfc5ac42aedU, (uint64_t)0x53380d139d95b3dfU, + (uint64_t)0x650a73548baf63deU, (uint64_t)0x766a0abb3c77b2a8U, + (uint64_t)0x81c2c92e47edaee6U, (uint64_t)0x92722c851482353bU, + (uint64_t)0xa2bfe8a14cf10364U, (uint64_t)0xa81a664bbc423001U, + (uint64_t)0xc24b8b70d0f89791U, (uint64_t)0xc76c51a30654be30U, + (uint64_t)0xd192e819d6ef5218U, (uint64_t)0xd69906245565a910U, + (uint64_t)0xf40e35855771202aU, (uint64_t)0x106aa07032bbd1b8U, + (uint64_t)0x19a4c116b8d2d0c8U, (uint64_t)0x1e376c085141ab53U, + (uint64_t)0x2748774cdf8eeb99U, (uint64_t)0x34b0bcb5e19b48a8U, + (uint64_t)0x391c0cb3c5c95a63U, (uint64_t)0x4ed8aa4ae3418acbU, + (uint64_t)0x5b9cca4f7763e373U, (uint64_t)0x682e6ff3d6b2b8a3U, + (uint64_t)0x748f82ee5defb2fcU, (uint64_t)0x78a5636f43172f60U, + (uint64_t)0x84c87814a1f0ab72U, (uint64_t)0x8cc702081a6439ecU, + (uint64_t)0x90befffa23631e28U, (uint64_t)0xa4506cebde82bde9U, + (uint64_t)0xbef9a3f7b2c67915U, (uint64_t)0xc67178f2e372532bU, + (uint64_t)0xca273eceea26619cU, (uint64_t)0xd186b8c721c0c207U, + (uint64_t)0xeada7dd6cde0eb1eU, (uint64_t)0xf57d4f7fee6ed178U, + (uint64_t)0x06f067aa72176fbaU, (uint64_t)0x0a637dc5a2c898a6U, + (uint64_t)0x113f9804bef90daeU, (uint64_t)0x1b710b35131c471bU, + (uint64_t)0x28db77f523047d84U, (uint64_t)0x32caab7b40c72493U, + (uint64_t)0x3c9ebe0a15c9bebcU, (uint64_t)0x431d67c49c100d4cU, + (uint64_t)0x4cc5d4becb3e42b6U, (uint64_t)0x597f299cfc657e2aU, + (uint64_t)0x5fcb6fab3ad6faecU, (uint64_t)0x6c44198c4a475817U +}; + +void Hacl_SHA2_Scalar32_sha256_init(uint32_t *hash); + +void Hacl_SHA2_Scalar32_sha256_update_nblocks(uint32_t len, uint8_t *b, + uint32_t *st); + +void Hacl_SHA2_Scalar32_sha256_update_last(uint64_t totlen, uint32_t len, + uint8_t *b, uint32_t *hash); + +void Hacl_SHA2_Scalar32_sha256_finish(uint32_t *st, uint8_t *h); + +void Hacl_SHA2_Scalar32_sha224_init(uint32_t *hash); + +void Hacl_SHA2_Scalar32_sha224_update_last(uint64_t totlen, uint32_t len, + uint8_t *b, uint32_t *st); + +void Hacl_SHA2_Scalar32_sha224_finish(uint32_t *st, uint8_t *h); + +void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash); + +void Hacl_SHA2_Scalar32_sha512_update_nblocks(uint32_t len, uint8_t *b, + uint64_t *st); + +void Hacl_SHA2_Scalar32_sha512_update_last(FStar_UInt128_uint128 totlen, + uint32_t len, uint8_t *b, + uint64_t *hash); + +void Hacl_SHA2_Scalar32_sha512_finish(uint64_t *st, uint8_t *h); + +void Hacl_SHA2_Scalar32_sha384_init(uint64_t *hash); + +void Hacl_SHA2_Scalar32_sha384_update_nblocks(uint32_t len, uint8_t *b, + uint64_t *st); + +void Hacl_SHA2_Scalar32_sha384_update_last(FStar_UInt128_uint128 totlen, + uint32_t len, uint8_t *b, + uint64_t *st); + +void Hacl_SHA2_Scalar32_sha384_finish(uint64_t *st, uint8_t *h); + +typedef Hacl_Streaming_MD_state_32 Hacl_Streaming_SHA2_state_sha2_224; + +typedef Hacl_Streaming_MD_state_32 Hacl_Streaming_SHA2_state_sha2_256; + +typedef Hacl_Streaming_MD_state_64 Hacl_Streaming_SHA2_state_sha2_384; + +typedef Hacl_Streaming_MD_state_64 Hacl_Streaming_SHA2_state_sha2_512; + +/** +Allocate initial state for the SHA2_256 hash. The state is to be freed by +calling `free_256`. +*/ +Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_256(void); + +/** +Copies the state passed as argument into a newly allocated state (deep copy). +The state is to be freed by calling `free_256`. Cloning the state this way is +useful, for instance, if your control-flow diverges and you need to feed +more (different) data into the hash in each branch. +*/ +Hacl_Streaming_MD_state_32 * +Hacl_Streaming_SHA2_copy_256(Hacl_Streaming_MD_state_32 *s0); + +/** +Reset an existing state to the initial hash state with empty data. +*/ +void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s); + +/** +Feed an arbitrary amount of data into the hash. This function returns 0 for +success, or 1 if the combined length of all of the data passed to `update_256` +(since the last call to `init_256`) exceeds 2^61-1 bytes. + +This function is identical to the update function for SHA2_224. +*/ +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_256(Hacl_Streaming_MD_state_32 *p, uint8_t *input, + uint32_t input_len); + +/** +Write the resulting hash into `dst`, an array of 32 bytes. The state remains +valid after a call to `finish_256`, meaning the user may feed more data into +the hash via `update_256`. (The finish_256 function operates on an internal copy +of the state and therefore does not invalidate the client-held state `p`.) +*/ +void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, + uint8_t *dst); + +/** +Free a state allocated with `create_in_256`. + +This function is identical to the free function for SHA2_224. +*/ +void Hacl_Streaming_SHA2_free_256(Hacl_Streaming_MD_state_32 *s); + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. +*/ +void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, + uint8_t *dst); + +Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_224(void); + +void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s); + +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_224(Hacl_Streaming_MD_state_32 *p, uint8_t *input, + uint32_t input_len); + +/** +Write the resulting hash into `dst`, an array of 28 bytes. The state remains +valid after a call to `finish_224`, meaning the user may feed more data into +the hash via `update_224`. +*/ +void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, + uint8_t *dst); + +void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_MD_state_32 *p); + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. +*/ +void Hacl_Streaming_SHA2_hash_224(uint8_t *input, uint32_t input_len, + uint8_t *dst); + +Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_512(void); + +/** +Copies the state passed as argument into a newly allocated state (deep copy). +The state is to be freed by calling `free_512`. Cloning the state this way is +useful, for instance, if your control-flow diverges and you need to feed +more (different) data into the hash in each branch. +*/ +Hacl_Streaming_MD_state_64 * +Hacl_Streaming_SHA2_copy_512(Hacl_Streaming_MD_state_64 *s0); + +void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s); + +/** +Feed an arbitrary amount of data into the hash. This function returns 0 for +success, or 1 if the combined length of all of the data passed to `update_512` +(since the last call to `init_512`) exceeds 2^125-1 bytes. + +This function is identical to the update function for SHA2_384. +*/ +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_512(Hacl_Streaming_MD_state_64 *p, uint8_t *input, + uint32_t input_len); + +/** +Write the resulting hash into `dst`, an array of 64 bytes. The state remains +valid after a call to `finish_512`, meaning the user may feed more data into +the hash via `update_512`. (The finish_512 function operates on an internal copy +of the state and therefore does not invalidate the client-held state `p`.) +*/ +void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, + uint8_t *dst); + +/** +Free a state allocated with `create_in_512`. + +This function is identical to the free function for SHA2_384. +*/ +void Hacl_Streaming_SHA2_free_512(Hacl_Streaming_MD_state_64 *s); + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes. +*/ +void Hacl_Streaming_SHA2_hash_512(uint8_t *input, uint32_t input_len, + uint8_t *dst); + +Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_384(void); + +void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s); + +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_384(Hacl_Streaming_MD_state_64 *p, uint8_t *input, + uint32_t input_len); + +/** +Write the resulting hash into `dst`, an array of 48 bytes. The state remains +valid after a call to `finish_384`, meaning the user may feed more data into +the hash via `update_384`. +*/ +void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, + uint8_t *dst); + +void Hacl_Streaming_SHA2_free_384(Hacl_Streaming_MD_state_64 *p); + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. +*/ +void Hacl_Streaming_SHA2_hash_384(uint8_t *input, uint32_t input_len, + uint8_t *dst); + +typedef struct Hacl_Impl_SHA2_Types_uint8_2p_s { + uint8_t *fst; + uint8_t *snd; +} Hacl_Impl_SHA2_Types_uint8_2p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_3p_s { + uint8_t *fst; + Hacl_Impl_SHA2_Types_uint8_2p snd; +} Hacl_Impl_SHA2_Types_uint8_3p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_4p_s { + uint8_t *fst; + Hacl_Impl_SHA2_Types_uint8_3p snd; +} Hacl_Impl_SHA2_Types_uint8_4p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_5p_s { + uint8_t *fst; + Hacl_Impl_SHA2_Types_uint8_4p snd; +} Hacl_Impl_SHA2_Types_uint8_5p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_6p_s { + uint8_t *fst; + Hacl_Impl_SHA2_Types_uint8_5p snd; +} Hacl_Impl_SHA2_Types_uint8_6p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_7p_s { + uint8_t *fst; + Hacl_Impl_SHA2_Types_uint8_6p snd; +} Hacl_Impl_SHA2_Types_uint8_7p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_8p_s { + uint8_t *fst; + Hacl_Impl_SHA2_Types_uint8_7p snd; +} Hacl_Impl_SHA2_Types_uint8_8p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_2x4p_s { + Hacl_Impl_SHA2_Types_uint8_4p fst; + Hacl_Impl_SHA2_Types_uint8_4p snd; +} Hacl_Impl_SHA2_Types_uint8_2x4p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_2x8p_s { + Hacl_Impl_SHA2_Types_uint8_8p fst; + Hacl_Impl_SHA2_Types_uint8_8p snd; +} Hacl_Impl_SHA2_Types_uint8_2x8p; + +#define __Hacl_Hash_H_DEFINED +#endif // CRYPTO_HACL_HASH_H_ diff --git a/crypto/hacl_lib.h b/crypto/hacl_lib.h new file mode 100644 index 0000000000000..44c8038ed124d --- /dev/null +++ b/crypto/hacl_lib.h @@ -0,0 +1,231 @@ +/* + * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation + * Copyright (c) 2022-2023 HACL* Contributors + * Copyright (c) 2023 Cryspen + */ + +#ifndef CRYPTO_HACL_LIB_H_ +#define CRYPTO_HACL_LIB_H_ + +#include +#include +#include +#include +#include + +typedef u128 FStar_UInt128_uint128; + +static inline u128 FStar_UInt128_shift_left(u128 x, u32 y) +{ + return (x << y); +} + +static inline u128 FStar_UInt128_add(u128 x, u128 y) +{ + return (x + y); +} + +static inline u128 FStar_UInt128_uint64_to_uint128(u64 x) +{ + return ((u128)x); +} + +/* Loads and stores. These avoid undefined behavior due to unaligned memory + * accesses, via memcpy. */ + +#define load32_be(b) (get_unaligned_be32(b)) +#define store32_be(b, i) put_unaligned_be32(i, b); +#define load64_be(b) (get_unaligned_be64(b)) +#define store64_be(b, i) put_unaligned_be64(i, b); + +static inline void store128_be(u8 *buf, u128 x) +{ + store64_be(buf, (u64)(x >> 64)); + store64_be(buf + 8, (u64)(x)); +} + +/* Macros for prettier unrolling of loops */ +#define KRML_LOOP1(i, n, x) \ + { \ + x i += n; \ + } + +#define KRML_LOOP2(i, n, x) \ + KRML_LOOP1(i, n, x) \ + KRML_LOOP1(i, n, x) + +#define KRML_LOOP3(i, n, x) \ + KRML_LOOP2(i, n, x) \ + KRML_LOOP1(i, n, x) + +#define KRML_LOOP4(i, n, x) \ + KRML_LOOP2(i, n, x) \ + KRML_LOOP2(i, n, x) + +#define KRML_LOOP5(i, n, x) \ + KRML_LOOP4(i, n, x) \ + KRML_LOOP1(i, n, x) + +#define KRML_LOOP6(i, n, x) \ + KRML_LOOP4(i, n, x) \ + KRML_LOOP2(i, n, x) + +#define KRML_LOOP7(i, n, x) \ + KRML_LOOP4(i, n, x) \ + KRML_LOOP3(i, n, x) + +#define KRML_LOOP8(i, n, x) \ + KRML_LOOP4(i, n, x) \ + KRML_LOOP4(i, n, x) + +#define KRML_LOOP9(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP1(i, n, x) + +#define KRML_LOOP10(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP2(i, n, x) + +#define KRML_LOOP11(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP3(i, n, x) + +#define KRML_LOOP12(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP4(i, n, x) + +#define KRML_LOOP13(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP5(i, n, x) + +#define KRML_LOOP14(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP6(i, n, x) + +#define KRML_LOOP15(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP7(i, n, x) + +#define KRML_LOOP16(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP8(i, n, x) + +#define KRML_UNROLL_FOR(i, z, n, k, x) \ + do { \ + uint32_t i = z; \ + KRML_LOOP##n(i, k, x) \ + } while (0) + +#define KRML_ACTUAL_FOR(i, z, n, k, x) \ + do { \ + for (uint32_t i = z; i < n; i += k) { \ + x \ + } \ + } while (0) + +#define KRML_UNROLL_MAX 16 + +/* 1 is the number of loop iterations, i.e. (n - z)/k as evaluated by krml */ +#if 0 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR0(i, z, n, k, x) +#else +#define KRML_MAYBE_FOR0(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 1 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 1, k, x) +#else +#define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 2 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 2, k, x) +#else +#define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 3 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 3, k, x) +#else +#define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 4 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 4, k, x) +#else +#define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 5 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 5, k, x) +#else +#define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 6 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 6, k, x) +#else +#define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 7 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 7, k, x) +#else +#define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 8 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 8, k, x) +#else +#define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 9 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 9, k, x) +#else +#define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 10 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 10, k, x) +#else +#define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 11 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 11, k, x) +#else +#define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 12 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 12, k, x) +#else +#define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 13 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 13, k, x) +#else +#define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 14 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 14, k, x) +#else +#define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 15 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 15, k, x) +#else +#define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 16 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 16, k, x) +#else +#define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#endif // CRYPTO_HACL_LIB_H_" diff --git a/crypto/sha2-hacl-generated.c b/crypto/sha2-hacl-generated.c new file mode 100644 index 0000000000000..9a5e081915b74 --- /dev/null +++ b/crypto/sha2-hacl-generated.c @@ -0,0 +1,939 @@ +/* GPLv2 or MIT License + * + * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation + * Copyright (c) 2022-2023 HACL* Contributors + * + */ + +#include "./hacl_hash.h" +#include "./hacl_lib.h" + +void Hacl_SHA2_Scalar32_sha256_init(uint32_t *hash) +{ + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + uint32_t *os = hash; + uint32_t x = Hacl_Impl_SHA2_Generic_h256[i]; + os[i] = x;); +} + +static inline void sha256_update_(uint8_t *b, uint32_t *hash) +{ + uint32_t hash_old[8U] = { 0U }; + uint32_t ws[16U] = { 0U }; + memcpy(hash_old, hash, (uint32_t)8U * sizeof(uint32_t)); + uint8_t *b10 = b; + uint32_t u = load32_be(b10); + ws[0U] = u; + uint32_t u0 = load32_be(b10 + (uint32_t)4U); + ws[1U] = u0; + uint32_t u1 = load32_be(b10 + (uint32_t)8U); + ws[2U] = u1; + uint32_t u2 = load32_be(b10 + (uint32_t)12U); + ws[3U] = u2; + uint32_t u3 = load32_be(b10 + (uint32_t)16U); + ws[4U] = u3; + uint32_t u4 = load32_be(b10 + (uint32_t)20U); + ws[5U] = u4; + uint32_t u5 = load32_be(b10 + (uint32_t)24U); + ws[6U] = u5; + uint32_t u6 = load32_be(b10 + (uint32_t)28U); + ws[7U] = u6; + uint32_t u7 = load32_be(b10 + (uint32_t)32U); + ws[8U] = u7; + uint32_t u8 = load32_be(b10 + (uint32_t)36U); + ws[9U] = u8; + uint32_t u9 = load32_be(b10 + (uint32_t)40U); + ws[10U] = u9; + uint32_t u10 = load32_be(b10 + (uint32_t)44U); + ws[11U] = u10; + uint32_t u11 = load32_be(b10 + (uint32_t)48U); + ws[12U] = u11; + uint32_t u12 = load32_be(b10 + (uint32_t)52U); + ws[13U] = u12; + uint32_t u13 = load32_be(b10 + (uint32_t)56U); + ws[14U] = u13; + uint32_t u14 = load32_be(b10 + (uint32_t)60U); + ws[15U] = u14; + KRML_MAYBE_FOR4( + i0, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + KRML_MAYBE_FOR16( + i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, + uint32_t k_t = Hacl_Impl_SHA2_Generic_k224_256 + [(uint32_t)16U * i0 + i]; + uint32_t ws_t = ws[i]; uint32_t a0 = hash[0U]; + uint32_t b0 = hash[1U]; uint32_t c0 = hash[2U]; + uint32_t d0 = hash[3U]; uint32_t e0 = hash[4U]; + uint32_t f0 = hash[5U]; uint32_t g0 = hash[6U]; + uint32_t h02 = hash[7U]; uint32_t k_e_t = k_t; + uint32_t t1 = + h02 + + ((e0 << (uint32_t)26U | e0 >> (uint32_t)6U) ^ + ((e0 << (uint32_t)21U | e0 >> (uint32_t)11U) ^ + (e0 << (uint32_t)7U | e0 >> (uint32_t)25U))) + + ((e0 & f0) ^ (~e0 & g0)) + k_e_t + ws_t; + uint32_t t2 = + ((a0 << (uint32_t)30U | a0 >> (uint32_t)2U) ^ + ((a0 << (uint32_t)19U | a0 >> (uint32_t)13U) ^ + (a0 << (uint32_t)10U | a0 >> (uint32_t)22U))) + + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); + uint32_t a1 = t1 + t2; uint32_t b1 = a0; + uint32_t c1 = b0; uint32_t d1 = c0; + uint32_t e1 = d0 + t1; uint32_t f1 = e0; + uint32_t g1 = f0; uint32_t h12 = g0; hash[0U] = a1; + hash[1U] = b1; hash[2U] = c1; hash[3U] = d1; + hash[4U] = e1; hash[5U] = f1; hash[6U] = g1; + hash[7U] = h12;); + if (i0 < (uint32_t)3U) { + KRML_MAYBE_FOR16( + i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, + uint32_t t16 = ws[i]; + uint32_t t15 = + ws[(i + (uint32_t)1U) % (uint32_t)16U]; + uint32_t t7 = + ws[(i + (uint32_t)9U) % (uint32_t)16U]; + uint32_t t2 = + ws[(i + (uint32_t)14U) % (uint32_t)16U]; + uint32_t s1 = (t2 << (uint32_t)15U | + t2 >> (uint32_t)17U) ^ + ((t2 << (uint32_t)13U | + t2 >> (uint32_t)19U) ^ + t2 >> (uint32_t)10U); + uint32_t s0 = (t15 << (uint32_t)25U | + t15 >> (uint32_t)7U) ^ + ((t15 << (uint32_t)14U | + t15 >> (uint32_t)18U) ^ + t15 >> (uint32_t)3U); + ws[i] = s1 + t7 + s0 + t16;); + }); + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + uint32_t *os = hash; + uint32_t x = hash[i] + hash_old[i]; os[i] = x;); +} + +void Hacl_SHA2_Scalar32_sha256_update_nblocks(uint32_t len, uint8_t *b, + uint32_t *st) +{ + uint32_t blocks = len / (uint32_t)64U; + for (uint32_t i = (uint32_t)0U; i < blocks; i++) { + uint8_t *b0 = b; + uint8_t *mb = b0 + i * (uint32_t)64U; + sha256_update_(mb, st); + } +} + +void Hacl_SHA2_Scalar32_sha256_update_last(uint64_t totlen, uint32_t len, + uint8_t *b, uint32_t *hash) +{ + uint32_t blocks; + if (len + (uint32_t)8U + (uint32_t)1U <= (uint32_t)64U) { + blocks = (uint32_t)1U; + } else { + blocks = (uint32_t)2U; + } + uint32_t fin = blocks * (uint32_t)64U; + uint8_t last[128U] = { 0U }; + uint8_t totlen_buf[8U] = { 0U }; + uint64_t total_len_bits = totlen << (uint32_t)3U; + store64_be(totlen_buf, total_len_bits); + uint8_t *b0 = b; + memcpy(last, b0, len * sizeof(uint8_t)); + last[len] = (uint8_t)0x80U; + memcpy(last + fin - (uint32_t)8U, totlen_buf, + (uint32_t)8U * sizeof(uint8_t)); + uint8_t *last00 = last; + uint8_t *last10 = last + (uint32_t)64U; + uint8_t *l0 = last00; + uint8_t *l1 = last10; + uint8_t *lb0 = l0; + uint8_t *lb1 = l1; + uint8_t *last0 = lb0; + uint8_t *last1 = lb1; + sha256_update_(last0, hash); + if (blocks > (uint32_t)1U) { + sha256_update_(last1, hash); + return; + } +} + +void Hacl_SHA2_Scalar32_sha256_finish(uint32_t *st, uint8_t *h) +{ + uint8_t hbuf[32U] = { 0U }; + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + store32_be(hbuf + i * (uint32_t)4U, st[i]);); + memcpy(h, hbuf, (uint32_t)32U * sizeof(uint8_t)); +} + +void Hacl_SHA2_Scalar32_sha224_init(uint32_t *hash) +{ + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + uint32_t *os = hash; + uint32_t x = Hacl_Impl_SHA2_Generic_h224[i]; + os[i] = x;); +} + +static inline void sha224_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st) +{ + Hacl_SHA2_Scalar32_sha256_update_nblocks(len, b, st); +} + +void Hacl_SHA2_Scalar32_sha224_update_last(uint64_t totlen, uint32_t len, + uint8_t *b, uint32_t *st) +{ + Hacl_SHA2_Scalar32_sha256_update_last(totlen, len, b, st); +} + +void Hacl_SHA2_Scalar32_sha224_finish(uint32_t *st, uint8_t *h) +{ + uint8_t hbuf[32U] = { 0U }; + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + store32_be(hbuf + i * (uint32_t)4U, st[i]);); + memcpy(h, hbuf, (uint32_t)28U * sizeof(uint8_t)); +} + +/** +Reset an existing state to the initial hash state with empty data. +*/ +void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s) +{ + Hacl_Streaming_MD_state_32 scrut = *s; + uint8_t *buf = scrut.buf; + uint32_t *block_state = scrut.block_state; + Hacl_SHA2_Scalar32_sha256_init(block_state); + Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, + .buf = buf, + .total_len = + (uint64_t)(uint32_t)0U }; + s[0U] = tmp; +} + +static inline Hacl_Streaming_Types_error_code +update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) +{ + Hacl_Streaming_MD_state_32 s = *p; + uint64_t total_len = s.total_len; + if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len) { + return Hacl_Streaming_Types_MaximumLengthExceeded; + } + uint32_t sz; + if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len > (uint64_t)0U) { + sz = (uint32_t)64U; + } else { + sz = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); + } + if (len <= (uint32_t)64U - sz) { + Hacl_Streaming_MD_state_32 s1 = *p; + uint32_t *block_state1 = s1.block_state; + uint8_t *buf = s1.buf; + uint64_t total_len1 = s1.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)64U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); + } + uint8_t *buf2 = buf + sz1; + memcpy(buf2, data, len * sizeof(uint8_t)); + uint64_t total_len2 = total_len1 + (uint64_t)len; + *p = ((Hacl_Streaming_MD_state_32){ .block_state = block_state1, + .buf = buf, + .total_len = total_len2 }); + } else if (sz == (uint32_t)0U) { + Hacl_Streaming_MD_state_32 s1 = *p; + uint32_t *block_state1 = s1.block_state; + uint8_t *buf = s1.buf; + uint64_t total_len1 = s1.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)64U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); + } + if (!(sz1 == (uint32_t)0U)) { + Hacl_SHA2_Scalar32_sha256_update_nblocks( + (uint32_t)64U, buf, block_state1); + } + uint32_t ite; + if ((uint64_t)len % (uint64_t)(uint32_t)64U == (uint64_t)0U && + (uint64_t)len > (uint64_t)0U) { + ite = (uint32_t)64U; + } else { + ite = (uint32_t)((uint64_t)len % + (uint64_t)(uint32_t)64U); + } + uint32_t n_blocks = (len - ite) / (uint32_t)64U; + uint32_t data1_len = n_blocks * (uint32_t)64U; + uint32_t data2_len = len - data1_len; + uint8_t *data1 = data; + uint8_t *data2 = data + data1_len; + Hacl_SHA2_Scalar32_sha256_update_nblocks( + data1_len / (uint32_t)64U * (uint32_t)64U, data1, + block_state1); + uint8_t *dst = buf; + memcpy(dst, data2, data2_len * sizeof(uint8_t)); + *p = ((Hacl_Streaming_MD_state_32){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)len }); + } else { + uint32_t diff = (uint32_t)64U - sz; + uint8_t *data1 = data; + uint8_t *data2 = data + diff; + Hacl_Streaming_MD_state_32 s1 = *p; + uint32_t *block_state10 = s1.block_state; + uint8_t *buf0 = s1.buf; + uint64_t total_len10 = s1.total_len; + uint32_t sz10; + if (total_len10 % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len10 > (uint64_t)0U) { + sz10 = (uint32_t)64U; + } else { + sz10 = (uint32_t)(total_len10 % + (uint64_t)(uint32_t)64U); + } + uint8_t *buf2 = buf0 + sz10; + memcpy(buf2, data1, diff * sizeof(uint8_t)); + uint64_t total_len2 = total_len10 + (uint64_t)diff; + *p = ((Hacl_Streaming_MD_state_32){ .block_state = + block_state10, + .buf = buf0, + .total_len = total_len2 }); + Hacl_Streaming_MD_state_32 s10 = *p; + uint32_t *block_state1 = s10.block_state; + uint8_t *buf = s10.buf; + uint64_t total_len1 = s10.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)64U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); + } + if (!(sz1 == (uint32_t)0U)) { + Hacl_SHA2_Scalar32_sha256_update_nblocks( + (uint32_t)64U, buf, block_state1); + } + uint32_t ite; + if ((uint64_t)(len - diff) % (uint64_t)(uint32_t)64U == + (uint64_t)0U && + (uint64_t)(len - diff) > (uint64_t)0U) { + ite = (uint32_t)64U; + } else { + ite = (uint32_t)((uint64_t)(len - diff) % + (uint64_t)(uint32_t)64U); + } + uint32_t n_blocks = (len - diff - ite) / (uint32_t)64U; + uint32_t data1_len = n_blocks * (uint32_t)64U; + uint32_t data2_len = len - diff - data1_len; + uint8_t *data11 = data2; + uint8_t *data21 = data2 + data1_len; + Hacl_SHA2_Scalar32_sha256_update_nblocks( + data1_len / (uint32_t)64U * (uint32_t)64U, data11, + block_state1); + uint8_t *dst = buf; + memcpy(dst, data21, data2_len * sizeof(uint8_t)); + *p = ((Hacl_Streaming_MD_state_32){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)(len - diff) }); + } + return Hacl_Streaming_Types_Success; +} + +/** +Feed an arbitrary amount of data into the hash. This function returns 0 for +success, or 1 if the combined length of all of the data passed to `update_256` +(since the last call to `init_256`) exceeds 2^61-1 bytes. + +This function is identical to the update function for SHA2_224. +*/ +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_256(Hacl_Streaming_MD_state_32 *p, uint8_t *input, + uint32_t input_len) +{ + return update_224_256(p, input, input_len); +} + +/** +Write the resulting hash into `dst`, an array of 32 bytes. The state remains +valid after a call to `finish_256`, meaning the user may feed more data into +the hash via `update_256`. (The finish_256 function operates on an internal copy +of the state and therefore does not invalidate the client-held state `p`.) +*/ +void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, uint8_t *dst) +{ + Hacl_Streaming_MD_state_32 scrut = *p; + uint32_t *block_state = scrut.block_state; + uint8_t *buf_ = scrut.buf; + uint64_t total_len = scrut.total_len; + uint32_t r; + if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len > (uint64_t)0U) { + r = (uint32_t)64U; + } else { + r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); + } + uint8_t *buf_1 = buf_; + uint32_t tmp_block_state[8U] = { 0U }; + memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof(uint32_t)); + uint32_t ite; + if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U) { + ite = (uint32_t)64U; + } else { + ite = r % (uint32_t)64U; + } + uint8_t *buf_last = buf_1 + r - ite; + uint8_t *buf_multi = buf_1; + Hacl_SHA2_Scalar32_sha256_update_nblocks((uint32_t)0U, buf_multi, + tmp_block_state); + uint64_t prev_len_last = total_len - (uint64_t)r; + Hacl_SHA2_Scalar32_sha256_update_last(prev_len_last + (uint64_t)r, r, + buf_last, tmp_block_state); + Hacl_SHA2_Scalar32_sha256_finish(tmp_block_state, dst); +} + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. +*/ +void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, + uint8_t *dst) +{ + uint8_t *ib = input; + uint8_t *rb = dst; + uint32_t st[8U] = { 0U }; + Hacl_SHA2_Scalar32_sha256_init(st); + uint32_t rem = input_len % (uint32_t)64U; + uint64_t len_ = (uint64_t)input_len; + Hacl_SHA2_Scalar32_sha256_update_nblocks(input_len, ib, st); + uint32_t rem1 = input_len % (uint32_t)64U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + Hacl_SHA2_Scalar32_sha256_update_last(len_, rem, lb, st); + Hacl_SHA2_Scalar32_sha256_finish(st, rb); +} + +void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s) +{ + Hacl_Streaming_MD_state_32 scrut = *s; + uint8_t *buf = scrut.buf; + uint32_t *block_state = scrut.block_state; + Hacl_SHA2_Scalar32_sha224_init(block_state); + Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, + .buf = buf, + .total_len = + (uint64_t)(uint32_t)0U }; + s[0U] = tmp; +} + +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_224(Hacl_Streaming_MD_state_32 *p, uint8_t *input, + uint32_t input_len) +{ + return update_224_256(p, input, input_len); +} + +/** +Write the resulting hash into `dst`, an array of 28 bytes. The state remains +valid after a call to `finish_224`, meaning the user may feed more data into +the hash via `update_224`. +*/ +void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, uint8_t *dst) +{ + Hacl_Streaming_MD_state_32 scrut = *p; + uint32_t *block_state = scrut.block_state; + uint8_t *buf_ = scrut.buf; + uint64_t total_len = scrut.total_len; + uint32_t r; + if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len > (uint64_t)0U) { + r = (uint32_t)64U; + } else { + r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); + } + uint8_t *buf_1 = buf_; + uint32_t tmp_block_state[8U] = { 0U }; + memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof(uint32_t)); + uint32_t ite; + if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U) { + ite = (uint32_t)64U; + } else { + ite = r % (uint32_t)64U; + } + uint8_t *buf_last = buf_1 + r - ite; + uint8_t *buf_multi = buf_1; + sha224_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state); + uint64_t prev_len_last = total_len - (uint64_t)r; + Hacl_SHA2_Scalar32_sha224_update_last(prev_len_last + (uint64_t)r, r, + buf_last, tmp_block_state); + Hacl_SHA2_Scalar32_sha224_finish(tmp_block_state, dst); +} + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. +*/ +void Hacl_Streaming_SHA2_hash_224(uint8_t *input, uint32_t input_len, + uint8_t *dst) +{ + uint8_t *ib = input; + uint8_t *rb = dst; + uint32_t st[8U] = { 0U }; + Hacl_SHA2_Scalar32_sha224_init(st); + uint32_t rem = input_len % (uint32_t)64U; + uint64_t len_ = (uint64_t)input_len; + sha224_update_nblocks(input_len, ib, st); + uint32_t rem1 = input_len % (uint32_t)64U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + Hacl_SHA2_Scalar32_sha224_update_last(len_, rem, lb, st); + Hacl_SHA2_Scalar32_sha224_finish(st, rb); +} + +void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash) +{ + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + uint64_t *os = hash; + uint64_t x = Hacl_Impl_SHA2_Generic_h512[i]; + os[i] = x;); +} + +static inline void sha512_update(uint8_t *b, uint64_t *hash) +{ + uint64_t hash_old[8U] = { 0U }; + uint64_t ws[16U] = { 0U }; + memcpy(hash_old, hash, (uint32_t)8U * sizeof(uint64_t)); + uint8_t *b10 = b; + uint64_t u = load64_be(b10); + ws[0U] = u; + uint64_t u0 = load64_be(b10 + (uint32_t)8U); + ws[1U] = u0; + uint64_t u1 = load64_be(b10 + (uint32_t)16U); + ws[2U] = u1; + uint64_t u2 = load64_be(b10 + (uint32_t)24U); + ws[3U] = u2; + uint64_t u3 = load64_be(b10 + (uint32_t)32U); + ws[4U] = u3; + uint64_t u4 = load64_be(b10 + (uint32_t)40U); + ws[5U] = u4; + uint64_t u5 = load64_be(b10 + (uint32_t)48U); + ws[6U] = u5; + uint64_t u6 = load64_be(b10 + (uint32_t)56U); + ws[7U] = u6; + uint64_t u7 = load64_be(b10 + (uint32_t)64U); + ws[8U] = u7; + uint64_t u8 = load64_be(b10 + (uint32_t)72U); + ws[9U] = u8; + uint64_t u9 = load64_be(b10 + (uint32_t)80U); + ws[10U] = u9; + uint64_t u10 = load64_be(b10 + (uint32_t)88U); + ws[11U] = u10; + uint64_t u11 = load64_be(b10 + (uint32_t)96U); + ws[12U] = u11; + uint64_t u12 = load64_be(b10 + (uint32_t)104U); + ws[13U] = u12; + uint64_t u13 = load64_be(b10 + (uint32_t)112U); + ws[14U] = u13; + uint64_t u14 = load64_be(b10 + (uint32_t)120U); + ws[15U] = u14; + KRML_MAYBE_FOR5( + i0, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, + KRML_MAYBE_FOR16( + i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, + uint64_t k_t = Hacl_Impl_SHA2_Generic_k384_512 + [(uint32_t)16U * i0 + i]; + uint64_t ws_t = ws[i]; uint64_t a0 = hash[0U]; + uint64_t b0 = hash[1U]; uint64_t c0 = hash[2U]; + uint64_t d0 = hash[3U]; uint64_t e0 = hash[4U]; + uint64_t f0 = hash[5U]; uint64_t g0 = hash[6U]; + uint64_t h02 = hash[7U]; uint64_t k_e_t = k_t; + uint64_t t1 = + h02 + + ((e0 << (uint32_t)50U | e0 >> (uint32_t)14U) ^ + ((e0 << (uint32_t)46U | e0 >> (uint32_t)18U) ^ + (e0 << (uint32_t)23U | e0 >> (uint32_t)41U))) + + ((e0 & f0) ^ (~e0 & g0)) + k_e_t + ws_t; + uint64_t t2 = + ((a0 << (uint32_t)36U | a0 >> (uint32_t)28U) ^ + ((a0 << (uint32_t)30U | a0 >> (uint32_t)34U) ^ + (a0 << (uint32_t)25U | a0 >> (uint32_t)39U))) + + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); + uint64_t a1 = t1 + t2; uint64_t b1 = a0; + uint64_t c1 = b0; uint64_t d1 = c0; + uint64_t e1 = d0 + t1; uint64_t f1 = e0; + uint64_t g1 = f0; uint64_t h12 = g0; hash[0U] = a1; + hash[1U] = b1; hash[2U] = c1; hash[3U] = d1; + hash[4U] = e1; hash[5U] = f1; hash[6U] = g1; + hash[7U] = h12;); + if (i0 < (uint32_t)4U) { + KRML_MAYBE_FOR16( + i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, + uint64_t t16 = ws[i]; + uint64_t t15 = + ws[(i + (uint32_t)1U) % (uint32_t)16U]; + uint64_t t7 = + ws[(i + (uint32_t)9U) % (uint32_t)16U]; + uint64_t t2 = + ws[(i + (uint32_t)14U) % (uint32_t)16U]; + uint64_t s1 = (t2 << (uint32_t)45U | + t2 >> (uint32_t)19U) ^ + ((t2 << (uint32_t)3U | + t2 >> (uint32_t)61U) ^ + t2 >> (uint32_t)6U); + uint64_t s0 = (t15 << (uint32_t)63U | + t15 >> (uint32_t)1U) ^ + ((t15 << (uint32_t)56U | + t15 >> (uint32_t)8U) ^ + t15 >> (uint32_t)7U); + ws[i] = s1 + t7 + s0 + t16;); + }); + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + uint64_t *os = hash; + uint64_t x = hash[i] + hash_old[i]; os[i] = x;); +} + +void Hacl_SHA2_Scalar32_sha512_update_nblocks(uint32_t len, uint8_t *b, + uint64_t *st) +{ + uint32_t blocks = len / (uint32_t)128U; + for (uint32_t i = (uint32_t)0U; i < blocks; i++) { + uint8_t *b0 = b; + uint8_t *mb = b0 + i * (uint32_t)128U; + sha512_update(mb, st); + } +} + +void Hacl_SHA2_Scalar32_sha512_update_last(FStar_UInt128_uint128 totlen, + uint32_t len, uint8_t *b, + uint64_t *hash) +{ + uint32_t blocks; + if (len + (uint32_t)16U + (uint32_t)1U <= (uint32_t)128U) { + blocks = (uint32_t)1U; + } else { + blocks = (uint32_t)2U; + } + uint32_t fin = blocks * (uint32_t)128U; + uint8_t last[256U] = { 0U }; + uint8_t totlen_buf[16U] = { 0U }; + FStar_UInt128_uint128 total_len_bits = + FStar_UInt128_shift_left(totlen, (uint32_t)3U); + store128_be(totlen_buf, total_len_bits); + uint8_t *b0 = b; + memcpy(last, b0, len * sizeof(uint8_t)); + last[len] = (uint8_t)0x80U; + memcpy(last + fin - (uint32_t)16U, totlen_buf, + (uint32_t)16U * sizeof(uint8_t)); + uint8_t *last00 = last; + uint8_t *last10 = last + (uint32_t)128U; + uint8_t *l0 = last00; + uint8_t *l1 = last10; + uint8_t *lb0 = l0; + uint8_t *lb1 = l1; + uint8_t *last0 = lb0; + uint8_t *last1 = lb1; + sha512_update(last0, hash); + if (blocks > (uint32_t)1U) { + sha512_update(last1, hash); + return; + } +} + +void Hacl_SHA2_Scalar32_sha512_finish(uint64_t *st, uint8_t *h) +{ + uint8_t hbuf[64U] = { 0U }; + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + store64_be(hbuf + i * (uint32_t)8U, st[i]);); + memcpy(h, hbuf, (uint32_t)64U * sizeof(uint8_t)); +} + +void Hacl_SHA2_Scalar32_sha384_init(uint64_t *hash) +{ + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + uint64_t *os = hash; + uint64_t x = Hacl_Impl_SHA2_Generic_h384[i]; + os[i] = x;); +} + +void Hacl_SHA2_Scalar32_sha384_update_nblocks(uint32_t len, uint8_t *b, + uint64_t *st) +{ + Hacl_SHA2_Scalar32_sha512_update_nblocks(len, b, st); +} + +void Hacl_SHA2_Scalar32_sha384_update_last(FStar_UInt128_uint128 totlen, + uint32_t len, uint8_t *b, + uint64_t *st) +{ + Hacl_SHA2_Scalar32_sha512_update_last(totlen, len, b, st); +} + +void Hacl_SHA2_Scalar32_sha384_finish(uint64_t *st, uint8_t *h) +{ + uint8_t hbuf[64U] = { 0U }; + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + store64_be(hbuf + i * (uint32_t)8U, st[i]);); + memcpy(h, hbuf, (uint32_t)48U * sizeof(uint8_t)); +} + +void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s) +{ + Hacl_Streaming_MD_state_64 scrut = *s; + uint8_t *buf = scrut.buf; + uint64_t *block_state = scrut.block_state; + Hacl_SHA2_Scalar32_sha512_init(block_state); + Hacl_Streaming_MD_state_64 tmp = { .block_state = block_state, + .buf = buf, + .total_len = + (uint64_t)(uint32_t)0U }; + s[0U] = tmp; +} + +static inline Hacl_Streaming_Types_error_code +update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) +{ + Hacl_Streaming_MD_state_64 s = *p; + uint64_t total_len = s.total_len; + if ((uint64_t)len > (uint64_t)18446744073709551615U - total_len) { + return Hacl_Streaming_Types_MaximumLengthExceeded; + } + uint32_t sz; + if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len > (uint64_t)0U) { + sz = (uint32_t)128U; + } else { + sz = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); + } + if (len <= (uint32_t)128U - sz) { + Hacl_Streaming_MD_state_64 s1 = *p; + uint64_t *block_state1 = s1.block_state; + uint8_t *buf = s1.buf; + uint64_t total_len1 = s1.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)128U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); + } + uint8_t *buf2 = buf + sz1; + memcpy(buf2, data, len * sizeof(uint8_t)); + uint64_t total_len2 = total_len1 + (uint64_t)len; + *p = ((Hacl_Streaming_MD_state_64){ .block_state = block_state1, + .buf = buf, + .total_len = total_len2 }); + } else if (sz == (uint32_t)0U) { + Hacl_Streaming_MD_state_64 s1 = *p; + uint64_t *block_state1 = s1.block_state; + uint8_t *buf = s1.buf; + uint64_t total_len1 = s1.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)128U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); + } + if (!(sz1 == (uint32_t)0U)) { + Hacl_SHA2_Scalar32_sha512_update_nblocks( + (uint32_t)128U, buf, block_state1); + } + uint32_t ite; + if ((uint64_t)len % (uint64_t)(uint32_t)128U == (uint64_t)0U && + (uint64_t)len > (uint64_t)0U) { + ite = (uint32_t)128U; + } else { + ite = (uint32_t)((uint64_t)len % + (uint64_t)(uint32_t)128U); + } + uint32_t n_blocks = (len - ite) / (uint32_t)128U; + uint32_t data1_len = n_blocks * (uint32_t)128U; + uint32_t data2_len = len - data1_len; + uint8_t *data1 = data; + uint8_t *data2 = data + data1_len; + Hacl_SHA2_Scalar32_sha512_update_nblocks( + data1_len / (uint32_t)128U * (uint32_t)128U, data1, + block_state1); + uint8_t *dst = buf; + memcpy(dst, data2, data2_len * sizeof(uint8_t)); + *p = ((Hacl_Streaming_MD_state_64){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)len }); + } else { + uint32_t diff = (uint32_t)128U - sz; + uint8_t *data1 = data; + uint8_t *data2 = data + diff; + Hacl_Streaming_MD_state_64 s1 = *p; + uint64_t *block_state10 = s1.block_state; + uint8_t *buf0 = s1.buf; + uint64_t total_len10 = s1.total_len; + uint32_t sz10; + if (total_len10 % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len10 > (uint64_t)0U) { + sz10 = (uint32_t)128U; + } else { + sz10 = (uint32_t)(total_len10 % + (uint64_t)(uint32_t)128U); + } + uint8_t *buf2 = buf0 + sz10; + memcpy(buf2, data1, diff * sizeof(uint8_t)); + uint64_t total_len2 = total_len10 + (uint64_t)diff; + *p = ((Hacl_Streaming_MD_state_64){ .block_state = + block_state10, + .buf = buf0, + .total_len = total_len2 }); + Hacl_Streaming_MD_state_64 s10 = *p; + uint64_t *block_state1 = s10.block_state; + uint8_t *buf = s10.buf; + uint64_t total_len1 = s10.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)128U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); + } + if (!(sz1 == (uint32_t)0U)) { + Hacl_SHA2_Scalar32_sha512_update_nblocks( + (uint32_t)128U, buf, block_state1); + } + uint32_t ite; + if ((uint64_t)(len - diff) % (uint64_t)(uint32_t)128U == + (uint64_t)0U && + (uint64_t)(len - diff) > (uint64_t)0U) { + ite = (uint32_t)128U; + } else { + ite = (uint32_t)((uint64_t)(len - diff) % + (uint64_t)(uint32_t)128U); + } + uint32_t n_blocks = (len - diff - ite) / (uint32_t)128U; + uint32_t data1_len = n_blocks * (uint32_t)128U; + uint32_t data2_len = len - diff - data1_len; + uint8_t *data11 = data2; + uint8_t *data21 = data2 + data1_len; + Hacl_SHA2_Scalar32_sha512_update_nblocks( + data1_len / (uint32_t)128U * (uint32_t)128U, data11, + block_state1); + uint8_t *dst = buf; + memcpy(dst, data21, data2_len * sizeof(uint8_t)); + *p = ((Hacl_Streaming_MD_state_64){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)(len - diff) }); + } + return Hacl_Streaming_Types_Success; +} + +/** +Feed an arbitrary amount of data into the hash. This function returns 0 for +success, or 1 if the combined length of all of the data passed to `update_512` +(since the last call to `init_512`) exceeds 2^125-1 bytes. + +This function is identical to the update function for SHA2_384. +*/ +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_512(Hacl_Streaming_MD_state_64 *p, uint8_t *input, + uint32_t input_len) +{ + return update_384_512(p, input, input_len); +} + +/** +Write the resulting hash into `dst`, an array of 64 bytes. The state remains +valid after a call to `finish_512`, meaning the user may feed more data into +the hash via `update_512`. (The finish_512 function operates on an internal copy +of the state and therefore does not invalidate the client-held state `p`.) +*/ +void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) +{ + Hacl_Streaming_MD_state_64 scrut = *p; + uint64_t *block_state = scrut.block_state; + uint8_t *buf_ = scrut.buf; + uint64_t total_len = scrut.total_len; + uint32_t r; + if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len > (uint64_t)0U) { + r = (uint32_t)128U; + } else { + r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); + } + uint8_t *buf_1 = buf_; + uint64_t tmp_block_state[8U] = { 0U }; + memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof(uint64_t)); + uint32_t ite; + if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U) { + ite = (uint32_t)128U; + } else { + ite = r % (uint32_t)128U; + } + uint8_t *buf_last = buf_1 + r - ite; + uint8_t *buf_multi = buf_1; + Hacl_SHA2_Scalar32_sha512_update_nblocks((uint32_t)0U, buf_multi, + tmp_block_state); + uint64_t prev_len_last = total_len - (uint64_t)r; + Hacl_SHA2_Scalar32_sha512_update_last( + FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last), + FStar_UInt128_uint64_to_uint128((uint64_t)r)), + r, buf_last, tmp_block_state); + Hacl_SHA2_Scalar32_sha512_finish(tmp_block_state, dst); +} + +void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s) +{ + Hacl_Streaming_MD_state_64 scrut = *s; + uint8_t *buf = scrut.buf; + uint64_t *block_state = scrut.block_state; + Hacl_SHA2_Scalar32_sha384_init(block_state); + Hacl_Streaming_MD_state_64 tmp = { .block_state = block_state, + .buf = buf, + .total_len = + (uint64_t)(uint32_t)0U }; + s[0U] = tmp; +} + +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_384(Hacl_Streaming_MD_state_64 *p, uint8_t *input, + uint32_t input_len) +{ + return update_384_512(p, input, input_len); +} + +/** +Write the resulting hash into `dst`, an array of 48 bytes. The state remains +valid after a call to `finish_384`, meaning the user may feed more data into +the hash via `update_384`. +*/ +void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) +{ + Hacl_Streaming_MD_state_64 scrut = *p; + uint64_t *block_state = scrut.block_state; + uint8_t *buf_ = scrut.buf; + uint64_t total_len = scrut.total_len; + uint32_t r; + if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len > (uint64_t)0U) { + r = (uint32_t)128U; + } else { + r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); + } + uint8_t *buf_1 = buf_; + uint64_t tmp_block_state[8U] = { 0U }; + memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof(uint64_t)); + uint32_t ite; + if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U) { + ite = (uint32_t)128U; + } else { + ite = r % (uint32_t)128U; + } + uint8_t *buf_last = buf_1 + r - ite; + uint8_t *buf_multi = buf_1; + Hacl_SHA2_Scalar32_sha384_update_nblocks((uint32_t)0U, buf_multi, + tmp_block_state); + uint64_t prev_len_last = total_len - (uint64_t)r; + Hacl_SHA2_Scalar32_sha384_update_last( + FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last), + FStar_UInt128_uint64_to_uint128((uint64_t)r)), + r, buf_last, tmp_block_state); + Hacl_SHA2_Scalar32_sha384_finish(tmp_block_state, dst); +} diff --git a/crypto/sha2-hacl.c b/crypto/sha2-hacl.c new file mode 100644 index 0000000000000..51565911b167e --- /dev/null +++ b/crypto/sha2-hacl.c @@ -0,0 +1,187 @@ +/* + * GPLv2 or MIT License + * + * Copyright (c) 2023 Cryspen + * + */ + +#include +#include + +#include "./hacl_hash.h" +#include "./hacl_lib.h" + +int hacl_sha256_update(struct shash_desc *desc, const u8 *data, + unsigned int len) +{ + struct sha256_state *sctx = shash_desc_ctx(desc); + Hacl_Streaming_MD_state_32 st; + st.block_state = sctx->state; + st.buf = sctx->buf; + st.total_len = sctx->count; + Hacl_Streaming_SHA2_update_256(&st, (u8 *)data, len); + sctx->count = st.total_len; + return 0; +} +EXPORT_SYMBOL(hacl_sha256_update); + +static int hacl_sha256_final(struct shash_desc *desc, u8 *out) +{ + struct sha256_state *sctx = shash_desc_ctx(desc); + Hacl_Streaming_MD_state_32 st; + st.block_state = sctx->state; + st.buf = sctx->buf; + st.total_len = sctx->count; + if (crypto_shash_digestsize(desc->tfm) == SHA224_DIGEST_SIZE) + Hacl_Streaming_SHA2_finish_224(&st, out); + else + Hacl_Streaming_SHA2_finish_256(&st, out); + return 0; +} + +int hacl_sha256_finup(struct shash_desc *desc, const u8 *data, unsigned int len, + u8 *hash) +{ + struct sha256_state *sctx = shash_desc_ctx(desc); + Hacl_Streaming_MD_state_32 st; + st.block_state = sctx->state; + st.buf = sctx->buf; + st.total_len = sctx->count; + Hacl_Streaming_SHA2_update_256(&st, (u8 *)data, len); + if (crypto_shash_digestsize(desc->tfm) == SHA224_DIGEST_SIZE) + Hacl_Streaming_SHA2_finish_224(&st, hash); + else + Hacl_Streaming_SHA2_finish_256(&st, hash); + return 0; +} +EXPORT_SYMBOL(hacl_sha256_finup); + +int hacl_sha512_update(struct shash_desc *desc, const u8 *data, + unsigned int len) +{ + struct sha512_state *sctx = shash_desc_ctx(desc); + Hacl_Streaming_MD_state_64 st; + st.block_state = sctx->state; + st.buf = sctx->buf; + st.total_len = sctx->count[0]; + Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); + sctx->count[0] = st.total_len; + return 0; +} +EXPORT_SYMBOL(hacl_sha512_update); + +static int hacl_sha512_final(struct shash_desc *desc, u8 *hash) +{ + struct sha512_state *sctx = shash_desc_ctx(desc); + Hacl_Streaming_MD_state_64 st; + st.block_state = sctx->state; + st.buf = sctx->buf; + st.total_len = sctx->count[0]; + if (crypto_shash_digestsize(desc->tfm) == SHA384_DIGEST_SIZE) + Hacl_Streaming_SHA2_finish_384(&st, hash); + else + Hacl_Streaming_SHA2_finish_512(&st, hash); + return 0; +} + +int hacl_sha512_finup(struct shash_desc *desc, const u8 *data, unsigned int len, + u8 *hash) +{ + struct sha512_state *sctx = shash_desc_ctx(desc); + Hacl_Streaming_MD_state_64 st; + st.block_state = sctx->state; + st.buf = sctx->buf; + st.total_len = sctx->count[0]; + Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); + if (crypto_shash_digestsize(desc->tfm) == SHA384_DIGEST_SIZE) + Hacl_Streaming_SHA2_finish_384(&st, hash); + else + Hacl_Streaming_SHA2_finish_512(&st, hash); + return 0; +} +EXPORT_SYMBOL(hacl_sha512_finup); + +static struct shash_alg sha2_hacl_algs[4] = { { + .digestsize = SHA256_DIGEST_SIZE, + .init = sha256_base_init, + .update = hacl_sha256_update, + .final = hacl_sha256_final, + .finup = hacl_sha256_finup, + .descsize = sizeof(struct sha256_state), + .base = { + .cra_name = "sha256", + .cra_driver_name = "sha256-hacl", + .cra_priority = 100, + .cra_blocksize = SHA256_BLOCK_SIZE, + .cra_module = THIS_MODULE, + } + }, { + .digestsize = SHA224_DIGEST_SIZE, + .init = sha224_base_init, + .update = hacl_sha256_update, + .final = hacl_sha256_final, + .finup = hacl_sha256_finup, + .descsize = sizeof(struct sha256_state), + .base = { + .cra_name = "sha224", + .cra_driver_name = "sha224-hacl", + .cra_priority = 100, + .cra_blocksize = SHA224_BLOCK_SIZE, + .cra_module = THIS_MODULE, + } + }, { + .digestsize = SHA384_DIGEST_SIZE, + .init = sha384_base_init, + .update = hacl_sha512_update, + .final = hacl_sha512_final, + .finup = hacl_sha512_finup, + .descsize = sizeof(struct sha512_state), + .base = { + .cra_name = "sha384", + .cra_driver_name = "sha384-hacl", + .cra_priority = 100, + .cra_blocksize = SHA384_BLOCK_SIZE, + .cra_module = THIS_MODULE, + } + }, { + .digestsize = SHA512_DIGEST_SIZE, + .init = sha512_base_init, + .update = hacl_sha512_update, + .final = hacl_sha512_final, + .finup = hacl_sha512_finup, + .descsize = sizeof(struct sha512_state), + .base = { + .cra_name = "sha512", + .cra_driver_name = "sha512-hacl", + .cra_priority = 100, + .cra_blocksize = SHA512_BLOCK_SIZE, + .cra_module = THIS_MODULE, + } + } +}; + +static int __init sha2_hacl_mod_init(void) +{ + return crypto_register_shashes(sha2_hacl_algs, + ARRAY_SIZE(sha2_hacl_algs)); +} + +static void __exit sha2_hacl_mod_fini(void) +{ + crypto_unregister_shashes(sha2_hacl_algs, ARRAY_SIZE(sha2_hacl_algs)); +} + +subsys_initcall(sha2_hacl_mod_init); +module_exit(sha2_hacl_mod_fini); + +MODULE_LICENSE("GPLv2 or MIT"); +MODULE_DESCRIPTION("Formally Verified SHA-2 Secure Hash Algorithm from HACL*"); + +MODULE_ALIAS_CRYPTO("sha224"); +MODULE_ALIAS_CRYPTO("sha224-hacl"); +MODULE_ALIAS_CRYPTO("sha256"); +MODULE_ALIAS_CRYPTO("sha256-hacl"); +MODULE_ALIAS_CRYPTO("sha384"); +MODULE_ALIAS_CRYPTO("sha384-hacl"); +MODULE_ALIAS_CRYPTO("sha512"); +MODULE_ALIAS_CRYPTO("sha512-hacl"); From eda684b7aa7b7af286eb9108640d287398bc3947 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Thu, 5 Oct 2023 14:55:16 +0200 Subject: [PATCH 03/18] Add HACL SHA2 to Makefile and config --- crypto/Kconfig | 6 ++++++ crypto/Makefile | 1 + 2 files changed, 7 insertions(+) diff --git a/crypto/Kconfig b/crypto/Kconfig index 650b1b3620d81..e35350102a433 100644 --- a/crypto/Kconfig +++ b/crypto/Kconfig @@ -1026,6 +1026,12 @@ config CRYPTO_SHA256 This is required for IPsec AH (XFRM_AH) and IPsec ESP (XFRM_ESP). Used by the btrfs filesystem, Ceph, NFS, and SMB. +config CRYPTO_SHA2_HACL + tristate "SHA-224 and SHA-256 and SHA-384 and SHA-512" + select CRYPTO_HASH + help + SHA-2 secure hash algorithms (FIPS 180, ISO/IEC 10118-3) from HACL* + config CRYPTO_SHA512 tristate "SHA-384 and SHA-512" select CRYPTO_HASH diff --git a/crypto/Makefile b/crypto/Makefile index 953a7e105e58c..2c88f3c8ce4db 100644 --- a/crypto/Makefile +++ b/crypto/Makefile @@ -77,6 +77,7 @@ obj-$(CONFIG_CRYPTO_MD5) += md5.o obj-$(CONFIG_CRYPTO_RMD160) += rmd160.o obj-$(CONFIG_CRYPTO_SHA1) += sha1_generic.o obj-$(CONFIG_CRYPTO_SHA256) += sha256_generic.o +obj-$(CONFIG_CRYPTO_SHA2_HACL) += sha2-hacl-generated.o sha2-hacl.o obj-$(CONFIG_CRYPTO_SHA512) += sha512_generic.o obj-$(CONFIG_CRYPTO_SHA3) += sha3_generic.o obj-$(CONFIG_CRYPTO_SM3) += sm3.o From ad8e84e3c62a72aa99063d85e7b1f1b6db67c03a Mon Sep 17 00:00:00 2001 From: Karthik Bhargavan Date: Fri, 13 Oct 2023 11:25:56 +0200 Subject: [PATCH 04/18] addressed review comments --- crypto/hacl_hash.h | 201 +++-------------------------------- crypto/sha2-hacl-generated.c | 100 ++++++++--------- crypto/sha2-hacl.c | 12 +-- 3 files changed, 73 insertions(+), 240 deletions(-) diff --git a/crypto/hacl_hash.h b/crypto/hacl_hash.h index 38901e36dbe8c..32c4f33d7a809 100644 --- a/crypto/hacl_hash.h +++ b/crypto/hacl_hash.h @@ -9,51 +9,24 @@ #include "./hacl_lib.h" -#define Spec_Hash_Definitions_SHA2_224 0 -#define Spec_Hash_Definitions_SHA2_256 1 -#define Spec_Hash_Definitions_SHA2_384 2 -#define Spec_Hash_Definitions_SHA2_512 3 -#define Spec_Hash_Definitions_SHA1 4 -#define Spec_Hash_Definitions_MD5 5 -#define Spec_Hash_Definitions_Blake2S 6 -#define Spec_Hash_Definitions_Blake2B 7 -#define Spec_Hash_Definitions_SHA3_256 8 -#define Spec_Hash_Definitions_SHA3_224 9 -#define Spec_Hash_Definitions_SHA3_384 10 -#define Spec_Hash_Definitions_SHA3_512 11 -#define Spec_Hash_Definitions_Shake128 12 -#define Spec_Hash_Definitions_Shake256 13 - -typedef uint8_t Spec_Hash_Definitions_hash_alg; - #define Hacl_Streaming_Types_Success 0 #define Hacl_Streaming_Types_InvalidAlgorithm 1 #define Hacl_Streaming_Types_InvalidLength 2 #define Hacl_Streaming_Types_MaximumLengthExceeded 3 -uint32_t Hacl_Hash_Definitions_word_len(Spec_Hash_Definitions_hash_alg a); - -uint32_t Hacl_Hash_Definitions_block_len(Spec_Hash_Definitions_hash_alg a); - -uint32_t Hacl_Hash_Definitions_hash_word_len(Spec_Hash_Definitions_hash_alg a); - -uint32_t Hacl_Hash_Definitions_hash_len(Spec_Hash_Definitions_hash_alg a); - -typedef uint8_t *Hacl_Hash_Definitions_hash_t; - typedef uint8_t Hacl_Streaming_Types_error_code; -typedef struct Hacl_Streaming_MD_state_32_s { +struct Hacl_Streaming_MD_state_32_s { uint32_t *block_state; uint8_t *buf; uint64_t total_len; -} Hacl_Streaming_MD_state_32; +}; -typedef struct Hacl_Streaming_MD_state_64_s { +struct Hacl_Streaming_MD_state_64_s { uint64_t *block_state; uint8_t *buf; uint64_t total_len; -} Hacl_Streaming_MD_state_64; +}; static const uint32_t Hacl_Impl_SHA2_Generic_h224[8U] = { (uint32_t)0xc1059ed8U, (uint32_t)0x367cd507U, (uint32_t)0x3070dd17U, @@ -149,72 +122,10 @@ static const uint64_t Hacl_Impl_SHA2_Generic_k384_512[80U] = { (uint64_t)0x5fcb6fab3ad6faecU, (uint64_t)0x6c44198c4a475817U }; -void Hacl_SHA2_Scalar32_sha256_init(uint32_t *hash); - -void Hacl_SHA2_Scalar32_sha256_update_nblocks(uint32_t len, uint8_t *b, - uint32_t *st); - -void Hacl_SHA2_Scalar32_sha256_update_last(uint64_t totlen, uint32_t len, - uint8_t *b, uint32_t *hash); - -void Hacl_SHA2_Scalar32_sha256_finish(uint32_t *st, uint8_t *h); - -void Hacl_SHA2_Scalar32_sha224_init(uint32_t *hash); - -void Hacl_SHA2_Scalar32_sha224_update_last(uint64_t totlen, uint32_t len, - uint8_t *b, uint32_t *st); - -void Hacl_SHA2_Scalar32_sha224_finish(uint32_t *st, uint8_t *h); - -void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash); - -void Hacl_SHA2_Scalar32_sha512_update_nblocks(uint32_t len, uint8_t *b, - uint64_t *st); - -void Hacl_SHA2_Scalar32_sha512_update_last(FStar_UInt128_uint128 totlen, - uint32_t len, uint8_t *b, - uint64_t *hash); - -void Hacl_SHA2_Scalar32_sha512_finish(uint64_t *st, uint8_t *h); - -void Hacl_SHA2_Scalar32_sha384_init(uint64_t *hash); - -void Hacl_SHA2_Scalar32_sha384_update_nblocks(uint32_t len, uint8_t *b, - uint64_t *st); - -void Hacl_SHA2_Scalar32_sha384_update_last(FStar_UInt128_uint128 totlen, - uint32_t len, uint8_t *b, - uint64_t *st); - -void Hacl_SHA2_Scalar32_sha384_finish(uint64_t *st, uint8_t *h); - -typedef Hacl_Streaming_MD_state_32 Hacl_Streaming_SHA2_state_sha2_224; - -typedef Hacl_Streaming_MD_state_32 Hacl_Streaming_SHA2_state_sha2_256; - -typedef Hacl_Streaming_MD_state_64 Hacl_Streaming_SHA2_state_sha2_384; - -typedef Hacl_Streaming_MD_state_64 Hacl_Streaming_SHA2_state_sha2_512; - -/** -Allocate initial state for the SHA2_256 hash. The state is to be freed by -calling `free_256`. -*/ -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_256(void); - -/** -Copies the state passed as argument into a newly allocated state (deep copy). -The state is to be freed by calling `free_256`. Cloning the state this way is -useful, for instance, if your control-flow diverges and you need to feed -more (different) data into the hash in each branch. -*/ -Hacl_Streaming_MD_state_32 * -Hacl_Streaming_SHA2_copy_256(Hacl_Streaming_MD_state_32 *s0); - /** Reset an existing state to the initial hash state with empty data. */ -void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s); +void Hacl_Streaming_SHA2_init_256(struct Hacl_Streaming_MD_state_32_s *s); /** Feed an arbitrary amount of data into the hash. This function returns 0 for @@ -224,7 +135,7 @@ success, or 1 if the combined length of all of the data passed to `update_256` This function is identical to the update function for SHA2_224. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_256(Hacl_Streaming_MD_state_32 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len); /** @@ -233,28 +144,19 @@ valid after a call to `finish_256`, meaning the user may feed more data into the hash via `update_256`. (The finish_256 function operates on an internal copy of the state and therefore does not invalidate the client-held state `p`.) */ -void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, +void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst); -/** -Free a state allocated with `create_in_256`. - -This function is identical to the free function for SHA2_224. -*/ -void Hacl_Streaming_SHA2_free_256(Hacl_Streaming_MD_state_32 *s); - /** Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. */ void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, uint8_t *dst); -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_224(void); - -void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s); +void Hacl_Streaming_SHA2_init_224(struct Hacl_Streaming_MD_state_32_s *s); Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_224(Hacl_Streaming_MD_state_32 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len); /** @@ -262,29 +164,16 @@ Write the resulting hash into `dst`, an array of 28 bytes. The state remains valid after a call to `finish_224`, meaning the user may feed more data into the hash via `update_224`. */ -void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, +void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst); -void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_MD_state_32 *p); - /** Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. */ void Hacl_Streaming_SHA2_hash_224(uint8_t *input, uint32_t input_len, uint8_t *dst); -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_512(void); - -/** -Copies the state passed as argument into a newly allocated state (deep copy). -The state is to be freed by calling `free_512`. Cloning the state this way is -useful, for instance, if your control-flow diverges and you need to feed -more (different) data into the hash in each branch. -*/ -Hacl_Streaming_MD_state_64 * -Hacl_Streaming_SHA2_copy_512(Hacl_Streaming_MD_state_64 *s0); - -void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s); +void Hacl_Streaming_SHA2_init_512(struct Hacl_Streaming_MD_state_64_s *s); /** Feed an arbitrary amount of data into the hash. This function returns 0 for @@ -294,7 +183,7 @@ success, or 1 if the combined length of all of the data passed to `update_512` This function is identical to the update function for SHA2_384. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_512(Hacl_Streaming_MD_state_64 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len); /** @@ -303,28 +192,19 @@ valid after a call to `finish_512`, meaning the user may feed more data into the hash via `update_512`. (The finish_512 function operates on an internal copy of the state and therefore does not invalidate the client-held state `p`.) */ -void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, +void Hacl_Streaming_SHA2_finish_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst); -/** -Free a state allocated with `create_in_512`. - -This function is identical to the free function for SHA2_384. -*/ -void Hacl_Streaming_SHA2_free_512(Hacl_Streaming_MD_state_64 *s); - /** Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes. */ void Hacl_Streaming_SHA2_hash_512(uint8_t *input, uint32_t input_len, uint8_t *dst); -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_384(void); - -void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s); +void Hacl_Streaming_SHA2_init_384(struct Hacl_Streaming_MD_state_64_s *s); Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_384(Hacl_Streaming_MD_state_64 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len); /** @@ -332,61 +212,12 @@ Write the resulting hash into `dst`, an array of 48 bytes. The state remains valid after a call to `finish_384`, meaning the user may feed more data into the hash via `update_384`. */ -void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, +void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst); - -void Hacl_Streaming_SHA2_free_384(Hacl_Streaming_MD_state_64 *p); - /** Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. */ void Hacl_Streaming_SHA2_hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst); -typedef struct Hacl_Impl_SHA2_Types_uint8_2p_s { - uint8_t *fst; - uint8_t *snd; -} Hacl_Impl_SHA2_Types_uint8_2p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_3p_s { - uint8_t *fst; - Hacl_Impl_SHA2_Types_uint8_2p snd; -} Hacl_Impl_SHA2_Types_uint8_3p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_4p_s { - uint8_t *fst; - Hacl_Impl_SHA2_Types_uint8_3p snd; -} Hacl_Impl_SHA2_Types_uint8_4p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_5p_s { - uint8_t *fst; - Hacl_Impl_SHA2_Types_uint8_4p snd; -} Hacl_Impl_SHA2_Types_uint8_5p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_6p_s { - uint8_t *fst; - Hacl_Impl_SHA2_Types_uint8_5p snd; -} Hacl_Impl_SHA2_Types_uint8_6p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_7p_s { - uint8_t *fst; - Hacl_Impl_SHA2_Types_uint8_6p snd; -} Hacl_Impl_SHA2_Types_uint8_7p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_8p_s { - uint8_t *fst; - Hacl_Impl_SHA2_Types_uint8_7p snd; -} Hacl_Impl_SHA2_Types_uint8_8p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_2x4p_s { - Hacl_Impl_SHA2_Types_uint8_4p fst; - Hacl_Impl_SHA2_Types_uint8_4p snd; -} Hacl_Impl_SHA2_Types_uint8_2x4p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_2x8p_s { - Hacl_Impl_SHA2_Types_uint8_8p fst; - Hacl_Impl_SHA2_Types_uint8_8p snd; -} Hacl_Impl_SHA2_Types_uint8_2x8p; - -#define __Hacl_Hash_H_DEFINED #endif // CRYPTO_HACL_HASH_H_ diff --git a/crypto/sha2-hacl-generated.c b/crypto/sha2-hacl-generated.c index 9a5e081915b74..ca0b6de5736fc 100644 --- a/crypto/sha2-hacl-generated.c +++ b/crypto/sha2-hacl-generated.c @@ -1,4 +1,5 @@ -/* GPLv2 or MIT License +/* + * GPLv2 or MIT License * * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation * Copyright (c) 2022-2023 HACL* Contributors @@ -16,7 +17,7 @@ void Hacl_SHA2_Scalar32_sha256_init(uint32_t *hash) os[i] = x;); } -static inline void sha256_update_(uint8_t *b, uint32_t *hash) +static inline void hacl_sha256_update(uint8_t *b, uint32_t *hash) { uint32_t hash_old[8U] = { 0U }; uint32_t ws[16U] = { 0U }; @@ -117,7 +118,7 @@ void Hacl_SHA2_Scalar32_sha256_update_nblocks(uint32_t len, uint8_t *b, for (uint32_t i = (uint32_t)0U; i < blocks; i++) { uint8_t *b0 = b; uint8_t *mb = b0 + i * (uint32_t)64U; - sha256_update_(mb, st); + hacl_sha256_update(mb, st); } } @@ -148,9 +149,9 @@ void Hacl_SHA2_Scalar32_sha256_update_last(uint64_t totlen, uint32_t len, uint8_t *lb1 = l1; uint8_t *last0 = lb0; uint8_t *last1 = lb1; - sha256_update_(last0, hash); + hacl_sha256_update(last0, hash); if (blocks > (uint32_t)1U) { - sha256_update_(last1, hash); + hacl_sha256_update(last1, hash); return; } } @@ -193,13 +194,14 @@ void Hacl_SHA2_Scalar32_sha224_finish(uint32_t *st, uint8_t *h) /** Reset an existing state to the initial hash state with empty data. */ -void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s) + +void Hacl_Streaming_SHA2_init_256(struct Hacl_Streaming_MD_state_32_s *s) { - Hacl_Streaming_MD_state_32 scrut = *s; + struct Hacl_Streaming_MD_state_32_s scrut = *s; uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha256_init(block_state); - Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, + struct Hacl_Streaming_MD_state_32_s tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -207,9 +209,9 @@ void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s) } static inline Hacl_Streaming_Types_error_code -update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) +update_224_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *data, uint32_t len) { - Hacl_Streaming_MD_state_32 s = *p; + struct Hacl_Streaming_MD_state_32_s s = *p; uint64_t total_len = s.total_len; if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len) { return Hacl_Streaming_Types_MaximumLengthExceeded; @@ -222,7 +224,7 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) sz = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); } if (len <= (uint32_t)64U - sz) { - Hacl_Streaming_MD_state_32 s1 = *p; + struct Hacl_Streaming_MD_state_32_s s1 = *p; uint32_t *block_state1 = s1.block_state; uint8_t *buf = s1.buf; uint64_t total_len1 = s1.total_len; @@ -236,11 +238,11 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) uint8_t *buf2 = buf + sz1; memcpy(buf2, data, len * sizeof(uint8_t)); uint64_t total_len2 = total_len1 + (uint64_t)len; - *p = ((Hacl_Streaming_MD_state_32){ .block_state = block_state1, + *p = ((struct Hacl_Streaming_MD_state_32_s){ .block_state = block_state1, .buf = buf, .total_len = total_len2 }); } else if (sz == (uint32_t)0U) { - Hacl_Streaming_MD_state_32 s1 = *p; + struct Hacl_Streaming_MD_state_32_s s1 = *p; uint32_t *block_state1 = s1.block_state; uint8_t *buf = s1.buf; uint64_t total_len1 = s1.total_len; @@ -273,7 +275,7 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) block_state1); uint8_t *dst = buf; memcpy(dst, data2, data2_len * sizeof(uint8_t)); - *p = ((Hacl_Streaming_MD_state_32){ + *p = ((struct Hacl_Streaming_MD_state_32_s){ .block_state = block_state1, .buf = buf, .total_len = total_len1 + (uint64_t)len }); @@ -281,7 +283,7 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) uint32_t diff = (uint32_t)64U - sz; uint8_t *data1 = data; uint8_t *data2 = data + diff; - Hacl_Streaming_MD_state_32 s1 = *p; + struct Hacl_Streaming_MD_state_32_s s1 = *p; uint32_t *block_state10 = s1.block_state; uint8_t *buf0 = s1.buf; uint64_t total_len10 = s1.total_len; @@ -296,11 +298,11 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) uint8_t *buf2 = buf0 + sz10; memcpy(buf2, data1, diff * sizeof(uint8_t)); uint64_t total_len2 = total_len10 + (uint64_t)diff; - *p = ((Hacl_Streaming_MD_state_32){ .block_state = + *p = ((struct Hacl_Streaming_MD_state_32_s){ .block_state = block_state10, .buf = buf0, .total_len = total_len2 }); - Hacl_Streaming_MD_state_32 s10 = *p; + struct Hacl_Streaming_MD_state_32_s s10 = *p; uint32_t *block_state1 = s10.block_state; uint8_t *buf = s10.buf; uint64_t total_len1 = s10.total_len; @@ -334,7 +336,7 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) block_state1); uint8_t *dst = buf; memcpy(dst, data21, data2_len * sizeof(uint8_t)); - *p = ((Hacl_Streaming_MD_state_32){ + *p = ((struct Hacl_Streaming_MD_state_32_s){ .block_state = block_state1, .buf = buf, .total_len = total_len1 + (uint64_t)(len - diff) }); @@ -350,7 +352,7 @@ success, or 1 if the combined length of all of the data passed to `update_256` This function is identical to the update function for SHA2_224. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_256(Hacl_Streaming_MD_state_32 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len) { return update_224_256(p, input, input_len); @@ -362,9 +364,9 @@ valid after a call to `finish_256`, meaning the user may feed more data into the hash via `update_256`. (The finish_256 function operates on an internal copy of the state and therefore does not invalidate the client-held state `p`.) */ -void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst) { - Hacl_Streaming_MD_state_32 scrut = *p; + struct Hacl_Streaming_MD_state_32_s scrut = *p; uint32_t *block_state = scrut.block_state; uint8_t *buf_ = scrut.buf; uint64_t total_len = scrut.total_len; @@ -414,13 +416,13 @@ void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, Hacl_SHA2_Scalar32_sha256_finish(st, rb); } -void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s) +void Hacl_Streaming_SHA2_init_224(struct Hacl_Streaming_MD_state_32_s *s) { - Hacl_Streaming_MD_state_32 scrut = *s; + struct Hacl_Streaming_MD_state_32_s scrut = *s; uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha224_init(block_state); - Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, + struct Hacl_Streaming_MD_state_32_s tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -428,7 +430,7 @@ void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s) } Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_224(Hacl_Streaming_MD_state_32 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len) { return update_224_256(p, input, input_len); @@ -439,9 +441,9 @@ Write the resulting hash into `dst`, an array of 28 bytes. The state remains valid after a call to `finish_224`, meaning the user may feed more data into the hash via `update_224`. */ -void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst) { - Hacl_Streaming_MD_state_32 scrut = *p; + struct Hacl_Streaming_MD_state_32_s scrut = *p; uint32_t *block_state = scrut.block_state; uint8_t *buf_ = scrut.buf; uint64_t total_len = scrut.total_len; @@ -676,13 +678,13 @@ void Hacl_SHA2_Scalar32_sha384_finish(uint64_t *st, uint8_t *h) memcpy(h, hbuf, (uint32_t)48U * sizeof(uint8_t)); } -void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s) +void Hacl_Streaming_SHA2_init_512(struct Hacl_Streaming_MD_state_64_s *s) { - Hacl_Streaming_MD_state_64 scrut = *s; + struct Hacl_Streaming_MD_state_64_s scrut = *s; uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha512_init(block_state); - Hacl_Streaming_MD_state_64 tmp = { .block_state = block_state, + struct Hacl_Streaming_MD_state_64_s tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -690,9 +692,9 @@ void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s) } static inline Hacl_Streaming_Types_error_code -update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) +update_384_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *data, uint32_t len) { - Hacl_Streaming_MD_state_64 s = *p; + struct Hacl_Streaming_MD_state_64_s s = *p; uint64_t total_len = s.total_len; if ((uint64_t)len > (uint64_t)18446744073709551615U - total_len) { return Hacl_Streaming_Types_MaximumLengthExceeded; @@ -705,7 +707,7 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) sz = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); } if (len <= (uint32_t)128U - sz) { - Hacl_Streaming_MD_state_64 s1 = *p; + struct Hacl_Streaming_MD_state_64_s s1 = *p; uint64_t *block_state1 = s1.block_state; uint8_t *buf = s1.buf; uint64_t total_len1 = s1.total_len; @@ -719,11 +721,11 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) uint8_t *buf2 = buf + sz1; memcpy(buf2, data, len * sizeof(uint8_t)); uint64_t total_len2 = total_len1 + (uint64_t)len; - *p = ((Hacl_Streaming_MD_state_64){ .block_state = block_state1, + *p = ((struct Hacl_Streaming_MD_state_64_s){ .block_state = block_state1, .buf = buf, .total_len = total_len2 }); } else if (sz == (uint32_t)0U) { - Hacl_Streaming_MD_state_64 s1 = *p; + struct Hacl_Streaming_MD_state_64_s s1 = *p; uint64_t *block_state1 = s1.block_state; uint8_t *buf = s1.buf; uint64_t total_len1 = s1.total_len; @@ -756,7 +758,7 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) block_state1); uint8_t *dst = buf; memcpy(dst, data2, data2_len * sizeof(uint8_t)); - *p = ((Hacl_Streaming_MD_state_64){ + *p = ((struct Hacl_Streaming_MD_state_64_s){ .block_state = block_state1, .buf = buf, .total_len = total_len1 + (uint64_t)len }); @@ -764,7 +766,7 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) uint32_t diff = (uint32_t)128U - sz; uint8_t *data1 = data; uint8_t *data2 = data + diff; - Hacl_Streaming_MD_state_64 s1 = *p; + struct Hacl_Streaming_MD_state_64_s s1 = *p; uint64_t *block_state10 = s1.block_state; uint8_t *buf0 = s1.buf; uint64_t total_len10 = s1.total_len; @@ -779,11 +781,11 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) uint8_t *buf2 = buf0 + sz10; memcpy(buf2, data1, diff * sizeof(uint8_t)); uint64_t total_len2 = total_len10 + (uint64_t)diff; - *p = ((Hacl_Streaming_MD_state_64){ .block_state = + *p = ((struct Hacl_Streaming_MD_state_64_s){ .block_state = block_state10, .buf = buf0, .total_len = total_len2 }); - Hacl_Streaming_MD_state_64 s10 = *p; + struct Hacl_Streaming_MD_state_64_s s10 = *p; uint64_t *block_state1 = s10.block_state; uint8_t *buf = s10.buf; uint64_t total_len1 = s10.total_len; @@ -817,7 +819,7 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) block_state1); uint8_t *dst = buf; memcpy(dst, data21, data2_len * sizeof(uint8_t)); - *p = ((Hacl_Streaming_MD_state_64){ + *p = ((struct Hacl_Streaming_MD_state_64_s){ .block_state = block_state1, .buf = buf, .total_len = total_len1 + (uint64_t)(len - diff) }); @@ -833,7 +835,7 @@ success, or 1 if the combined length of all of the data passed to `update_512` This function is identical to the update function for SHA2_384. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_512(Hacl_Streaming_MD_state_64 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len) { return update_384_512(p, input, input_len); @@ -845,9 +847,9 @@ valid after a call to `finish_512`, meaning the user may feed more data into the hash via `update_512`. (The finish_512 function operates on an internal copy of the state and therefore does not invalidate the client-held state `p`.) */ -void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst) { - Hacl_Streaming_MD_state_64 scrut = *p; + struct Hacl_Streaming_MD_state_64_s scrut = *p; uint64_t *block_state = scrut.block_state; uint8_t *buf_ = scrut.buf; uint64_t total_len = scrut.total_len; @@ -879,13 +881,13 @@ void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) Hacl_SHA2_Scalar32_sha512_finish(tmp_block_state, dst); } -void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s) +void Hacl_Streaming_SHA2_init_384(struct Hacl_Streaming_MD_state_64_s *s) { - Hacl_Streaming_MD_state_64 scrut = *s; + struct Hacl_Streaming_MD_state_64_s scrut = *s; uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha384_init(block_state); - Hacl_Streaming_MD_state_64 tmp = { .block_state = block_state, + struct Hacl_Streaming_MD_state_64_s tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -893,7 +895,7 @@ void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s) } Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_384(Hacl_Streaming_MD_state_64 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len) { return update_384_512(p, input, input_len); @@ -904,9 +906,9 @@ Write the resulting hash into `dst`, an array of 48 bytes. The state remains valid after a call to `finish_384`, meaning the user may feed more data into the hash via `update_384`. */ -void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst) { - Hacl_Streaming_MD_state_64 scrut = *p; + struct Hacl_Streaming_MD_state_64_s scrut = *p; uint64_t *block_state = scrut.block_state; uint8_t *buf_ = scrut.buf; uint64_t total_len = scrut.total_len; diff --git a/crypto/sha2-hacl.c b/crypto/sha2-hacl.c index 51565911b167e..89e4ec2e2c457 100644 --- a/crypto/sha2-hacl.c +++ b/crypto/sha2-hacl.c @@ -15,7 +15,7 @@ int hacl_sha256_update(struct shash_desc *desc, const u8 *data, unsigned int len) { struct sha256_state *sctx = shash_desc_ctx(desc); - Hacl_Streaming_MD_state_32 st; + struct Hacl_Streaming_MD_state_32_s st; st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count; @@ -28,7 +28,7 @@ EXPORT_SYMBOL(hacl_sha256_update); static int hacl_sha256_final(struct shash_desc *desc, u8 *out) { struct sha256_state *sctx = shash_desc_ctx(desc); - Hacl_Streaming_MD_state_32 st; + struct Hacl_Streaming_MD_state_32_s st; st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count; @@ -43,7 +43,7 @@ int hacl_sha256_finup(struct shash_desc *desc, const u8 *data, unsigned int len, u8 *hash) { struct sha256_state *sctx = shash_desc_ctx(desc); - Hacl_Streaming_MD_state_32 st; + struct Hacl_Streaming_MD_state_32_s st; st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count; @@ -60,7 +60,7 @@ int hacl_sha512_update(struct shash_desc *desc, const u8 *data, unsigned int len) { struct sha512_state *sctx = shash_desc_ctx(desc); - Hacl_Streaming_MD_state_64 st; + struct Hacl_Streaming_MD_state_64_s st; st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count[0]; @@ -73,7 +73,7 @@ EXPORT_SYMBOL(hacl_sha512_update); static int hacl_sha512_final(struct shash_desc *desc, u8 *hash) { struct sha512_state *sctx = shash_desc_ctx(desc); - Hacl_Streaming_MD_state_64 st; + struct Hacl_Streaming_MD_state_64_s st; st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count[0]; @@ -88,7 +88,7 @@ int hacl_sha512_finup(struct shash_desc *desc, const u8 *data, unsigned int len, u8 *hash) { struct sha512_state *sctx = shash_desc_ctx(desc); - Hacl_Streaming_MD_state_64 st; + struct Hacl_Streaming_MD_state_64_s st; st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count[0]; From 585ad7d4e280114b5df50bb9e5625a93599d1cf3 Mon Sep 17 00:00:00 2001 From: Karthik Bhargavan Date: Fri, 13 Oct 2023 11:34:21 +0200 Subject: [PATCH 05/18] propagating errors --- crypto/sha2-hacl.c | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/crypto/sha2-hacl.c b/crypto/sha2-hacl.c index 89e4ec2e2c457..efc9e09b1f1b9 100644 --- a/crypto/sha2-hacl.c +++ b/crypto/sha2-hacl.c @@ -19,9 +19,9 @@ int hacl_sha256_update(struct shash_desc *desc, const u8 *data, st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count; - Hacl_Streaming_SHA2_update_256(&st, (u8 *)data, len); + uint8_t res = Hacl_Streaming_SHA2_update_256(&st, (u8 *)data, len); sctx->count = st.total_len; - return 0; + return res; } EXPORT_SYMBOL(hacl_sha256_update); @@ -64,9 +64,9 @@ int hacl_sha512_update(struct shash_desc *desc, const u8 *data, st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count[0]; - Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); + uint8_t res = Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); sctx->count[0] = st.total_len; - return 0; + return res; } EXPORT_SYMBOL(hacl_sha512_update); @@ -92,12 +92,15 @@ int hacl_sha512_finup(struct shash_desc *desc, const u8 *data, unsigned int len, st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count[0]; - Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); - if (crypto_shash_digestsize(desc->tfm) == SHA384_DIGEST_SIZE) - Hacl_Streaming_SHA2_finish_384(&st, hash); - else - Hacl_Streaming_SHA2_finish_512(&st, hash); - return 0; + uint8_t res = Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); + if (res == 0) { + if (crypto_shash_digestsize(desc->tfm) == SHA384_DIGEST_SIZE) + Hacl_Streaming_SHA2_finish_384(&st, hash); + else + Hacl_Streaming_SHA2_finish_512(&st, hash); + return 0; + } else + return res; } EXPORT_SYMBOL(hacl_sha512_finup); From b0e03392ce0ac298fe22ebe18b9454a7e404d7f4 Mon Sep 17 00:00:00 2001 From: armfazh Date: Mon, 16 Oct 2023 16:42:06 -0700 Subject: [PATCH 06/18] Formatting files according to clang-format. --- crypto/hacl_hash.h | 20 +++---- crypto/hacl_lib.h | 2 +- crypto/sha2-hacl-generated.c | 106 +++++++++++++++++++---------------- crypto/sha2-hacl.c | 21 +++---- 4 files changed, 81 insertions(+), 68 deletions(-) diff --git a/crypto/hacl_hash.h b/crypto/hacl_hash.h index 32c4f33d7a809..a9524994e9023 100644 --- a/crypto/hacl_hash.h +++ b/crypto/hacl_hash.h @@ -7,7 +7,7 @@ #ifndef CRYPTO_HACL_HASH_H_ #define CRYPTO_HACL_HASH_H_ -#include "./hacl_lib.h" +#include "hacl_lib.h" #define Hacl_Streaming_Types_Success 0 #define Hacl_Streaming_Types_InvalidAlgorithm 1 @@ -135,8 +135,8 @@ success, or 1 if the combined length of all of the data passed to `update_256` This function is identical to the update function for SHA2_224. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, - uint32_t input_len); +Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, + uint8_t *input, uint32_t input_len); /** Write the resulting hash into `dst`, an array of 32 bytes. The state remains @@ -156,8 +156,8 @@ void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, void Hacl_Streaming_SHA2_init_224(struct Hacl_Streaming_MD_state_32_s *s); Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, - uint32_t input_len); +Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, + uint8_t *input, uint32_t input_len); /** Write the resulting hash into `dst`, an array of 28 bytes. The state remains @@ -183,8 +183,8 @@ success, or 1 if the combined length of all of the data passed to `update_512` This function is identical to the update function for SHA2_384. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, - uint32_t input_len); +Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, + uint8_t *input, uint32_t input_len); /** Write the resulting hash into `dst`, an array of 64 bytes. The state remains @@ -204,8 +204,8 @@ void Hacl_Streaming_SHA2_hash_512(uint8_t *input, uint32_t input_len, void Hacl_Streaming_SHA2_init_384(struct Hacl_Streaming_MD_state_64_s *s); Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, - uint32_t input_len); +Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, + uint8_t *input, uint32_t input_len); /** Write the resulting hash into `dst`, an array of 48 bytes. The state remains @@ -220,4 +220,4 @@ Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. void Hacl_Streaming_SHA2_hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst); -#endif // CRYPTO_HACL_HASH_H_ +#endif // CRYPTO_HACL_HASH_H_ diff --git a/crypto/hacl_lib.h b/crypto/hacl_lib.h index 44c8038ed124d..b6e3e015294d3 100644 --- a/crypto/hacl_lib.h +++ b/crypto/hacl_lib.h @@ -228,4 +228,4 @@ static inline void store128_be(u8 *buf, u128 x) #define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) #endif -#endif // CRYPTO_HACL_LIB_H_" +#endif // CRYPTO_HACL_LIB_H_ diff --git a/crypto/sha2-hacl-generated.c b/crypto/sha2-hacl-generated.c index ca0b6de5736fc..9f3bfa4824219 100644 --- a/crypto/sha2-hacl-generated.c +++ b/crypto/sha2-hacl-generated.c @@ -1,4 +1,4 @@ -/* +/* * GPLv2 or MIT License * * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation @@ -6,8 +6,8 @@ * */ -#include "./hacl_hash.h" -#include "./hacl_lib.h" +#include "hacl_hash.h" +#include "hacl_lib.h" void Hacl_SHA2_Scalar32_sha256_init(uint32_t *hash) { @@ -201,15 +201,17 @@ void Hacl_Streaming_SHA2_init_256(struct Hacl_Streaming_MD_state_32_s *s) uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha256_init(block_state); - struct Hacl_Streaming_MD_state_32_s tmp = { .block_state = block_state, - .buf = buf, - .total_len = - (uint64_t)(uint32_t)0U }; + struct Hacl_Streaming_MD_state_32_s tmp = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; s[0U] = tmp; } static inline Hacl_Streaming_Types_error_code -update_224_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *data, uint32_t len) +update_224_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *data, + uint32_t len) { struct Hacl_Streaming_MD_state_32_s s = *p; uint64_t total_len = s.total_len; @@ -238,9 +240,10 @@ update_224_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *data, uint32_t l uint8_t *buf2 = buf + sz1; memcpy(buf2, data, len * sizeof(uint8_t)); uint64_t total_len2 = total_len1 + (uint64_t)len; - *p = ((struct Hacl_Streaming_MD_state_32_s){ .block_state = block_state1, - .buf = buf, - .total_len = total_len2 }); + *p = ((struct Hacl_Streaming_MD_state_32_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len2 }); } else if (sz == (uint32_t)0U) { struct Hacl_Streaming_MD_state_32_s s1 = *p; uint32_t *block_state1 = s1.block_state; @@ -298,10 +301,10 @@ update_224_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *data, uint32_t l uint8_t *buf2 = buf0 + sz10; memcpy(buf2, data1, diff * sizeof(uint8_t)); uint64_t total_len2 = total_len10 + (uint64_t)diff; - *p = ((struct Hacl_Streaming_MD_state_32_s){ .block_state = - block_state10, - .buf = buf0, - .total_len = total_len2 }); + *p = ((struct Hacl_Streaming_MD_state_32_s){ + .block_state = block_state10, + .buf = buf0, + .total_len = total_len2 }); struct Hacl_Streaming_MD_state_32_s s10 = *p; uint32_t *block_state1 = s10.block_state; uint8_t *buf = s10.buf; @@ -352,8 +355,8 @@ success, or 1 if the combined length of all of the data passed to `update_256` This function is identical to the update function for SHA2_224. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, - uint32_t input_len) +Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, + uint8_t *input, uint32_t input_len) { return update_224_256(p, input, input_len); } @@ -364,7 +367,8 @@ valid after a call to `finish_256`, meaning the user may feed more data into the hash via `update_256`. (The finish_256 function operates on an internal copy of the state and therefore does not invalidate the client-held state `p`.) */ -void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, + uint8_t *dst) { struct Hacl_Streaming_MD_state_32_s scrut = *p; uint32_t *block_state = scrut.block_state; @@ -422,16 +426,17 @@ void Hacl_Streaming_SHA2_init_224(struct Hacl_Streaming_MD_state_32_s *s) uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha224_init(block_state); - struct Hacl_Streaming_MD_state_32_s tmp = { .block_state = block_state, - .buf = buf, - .total_len = - (uint64_t)(uint32_t)0U }; + struct Hacl_Streaming_MD_state_32_s tmp = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; s[0U] = tmp; } Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, - uint32_t input_len) +Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, + uint8_t *input, uint32_t input_len) { return update_224_256(p, input, input_len); } @@ -441,7 +446,8 @@ Write the resulting hash into `dst`, an array of 28 bytes. The state remains valid after a call to `finish_224`, meaning the user may feed more data into the hash via `update_224`. */ -void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, + uint8_t *dst) { struct Hacl_Streaming_MD_state_32_s scrut = *p; uint32_t *block_state = scrut.block_state; @@ -684,15 +690,17 @@ void Hacl_Streaming_SHA2_init_512(struct Hacl_Streaming_MD_state_64_s *s) uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha512_init(block_state); - struct Hacl_Streaming_MD_state_64_s tmp = { .block_state = block_state, - .buf = buf, - .total_len = - (uint64_t)(uint32_t)0U }; + struct Hacl_Streaming_MD_state_64_s tmp = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; s[0U] = tmp; } static inline Hacl_Streaming_Types_error_code -update_384_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *data, uint32_t len) +update_384_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *data, + uint32_t len) { struct Hacl_Streaming_MD_state_64_s s = *p; uint64_t total_len = s.total_len; @@ -721,9 +729,10 @@ update_384_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *data, uint32_t l uint8_t *buf2 = buf + sz1; memcpy(buf2, data, len * sizeof(uint8_t)); uint64_t total_len2 = total_len1 + (uint64_t)len; - *p = ((struct Hacl_Streaming_MD_state_64_s){ .block_state = block_state1, - .buf = buf, - .total_len = total_len2 }); + *p = ((struct Hacl_Streaming_MD_state_64_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len2 }); } else if (sz == (uint32_t)0U) { struct Hacl_Streaming_MD_state_64_s s1 = *p; uint64_t *block_state1 = s1.block_state; @@ -781,10 +790,10 @@ update_384_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *data, uint32_t l uint8_t *buf2 = buf0 + sz10; memcpy(buf2, data1, diff * sizeof(uint8_t)); uint64_t total_len2 = total_len10 + (uint64_t)diff; - *p = ((struct Hacl_Streaming_MD_state_64_s){ .block_state = - block_state10, - .buf = buf0, - .total_len = total_len2 }); + *p = ((struct Hacl_Streaming_MD_state_64_s){ + .block_state = block_state10, + .buf = buf0, + .total_len = total_len2 }); struct Hacl_Streaming_MD_state_64_s s10 = *p; uint64_t *block_state1 = s10.block_state; uint8_t *buf = s10.buf; @@ -835,8 +844,8 @@ success, or 1 if the combined length of all of the data passed to `update_512` This function is identical to the update function for SHA2_384. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, - uint32_t input_len) +Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, + uint8_t *input, uint32_t input_len) { return update_384_512(p, input, input_len); } @@ -847,7 +856,8 @@ valid after a call to `finish_512`, meaning the user may feed more data into the hash via `update_512`. (The finish_512 function operates on an internal copy of the state and therefore does not invalidate the client-held state `p`.) */ -void Hacl_Streaming_SHA2_finish_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_512(struct Hacl_Streaming_MD_state_64_s *p, + uint8_t *dst) { struct Hacl_Streaming_MD_state_64_s scrut = *p; uint64_t *block_state = scrut.block_state; @@ -887,16 +897,17 @@ void Hacl_Streaming_SHA2_init_384(struct Hacl_Streaming_MD_state_64_s *s) uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha384_init(block_state); - struct Hacl_Streaming_MD_state_64_s tmp = { .block_state = block_state, - .buf = buf, - .total_len = - (uint64_t)(uint32_t)0U }; + struct Hacl_Streaming_MD_state_64_s tmp = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; s[0U] = tmp; } Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, - uint32_t input_len) +Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, + uint8_t *input, uint32_t input_len) { return update_384_512(p, input, input_len); } @@ -906,7 +917,8 @@ Write the resulting hash into `dst`, an array of 48 bytes. The state remains valid after a call to `finish_384`, meaning the user may feed more data into the hash via `update_384`. */ -void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, + uint8_t *dst) { struct Hacl_Streaming_MD_state_64_s scrut = *p; uint64_t *block_state = scrut.block_state; diff --git a/crypto/sha2-hacl.c b/crypto/sha2-hacl.c index efc9e09b1f1b9..6400fbce0ae0b 100644 --- a/crypto/sha2-hacl.c +++ b/crypto/sha2-hacl.c @@ -8,8 +8,8 @@ #include #include -#include "./hacl_hash.h" -#include "./hacl_lib.h" +#include "hacl_hash.h" +#include "hacl_lib.h" int hacl_sha256_update(struct shash_desc *desc, const u8 *data, unsigned int len) @@ -93,14 +93,15 @@ int hacl_sha512_finup(struct shash_desc *desc, const u8 *data, unsigned int len, st.buf = sctx->buf; st.total_len = sctx->count[0]; uint8_t res = Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); - if (res == 0) { - if (crypto_shash_digestsize(desc->tfm) == SHA384_DIGEST_SIZE) - Hacl_Streaming_SHA2_finish_384(&st, hash); - else - Hacl_Streaming_SHA2_finish_512(&st, hash); - return 0; - } else - return res; + if (res == 0) { + if (crypto_shash_digestsize(desc->tfm) == SHA384_DIGEST_SIZE) + Hacl_Streaming_SHA2_finish_384(&st, hash); + else + Hacl_Streaming_SHA2_finish_512(&st, hash); + return 0; + } else { + return res; + } } EXPORT_SYMBOL(hacl_sha512_finup); From 0a59a731f54310b87f850fe9071ff5081279e6f4 Mon Sep 17 00:00:00 2001 From: armfazh Date: Mon, 16 Oct 2023 16:47:21 -0700 Subject: [PATCH 07/18] Updating comment style. --- crypto/hacl_hash.h | 104 ++++++++++++++++++----------------- crypto/hacl_lib.h | 6 +- crypto/sha2-hacl-generated.c | 10 ++-- 3 files changed, 62 insertions(+), 58 deletions(-) diff --git a/crypto/hacl_hash.h b/crypto/hacl_hash.h index a9524994e9023..1e10e54dfd6c2 100644 --- a/crypto/hacl_hash.h +++ b/crypto/hacl_hash.h @@ -122,34 +122,35 @@ static const uint64_t Hacl_Impl_SHA2_Generic_k384_512[80U] = { (uint64_t)0x5fcb6fab3ad6faecU, (uint64_t)0x6c44198c4a475817U }; -/** -Reset an existing state to the initial hash state with empty data. -*/ +/* + * Reset an existing state to the initial hash state with empty data. + */ void Hacl_Streaming_SHA2_init_256(struct Hacl_Streaming_MD_state_32_s *s); -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_256` -(since the last call to `init_256`) exceeds 2^61-1 bytes. - -This function is identical to the update function for SHA2_224. -*/ +/* + * Feed an arbitrary amount of data into the hash. This function returns 0 for + * success, or 1 if the combined length of all of the data passed to + * `update_256` (since the last call to `init_256`) exceeds 2^61-1 bytes. + * + * This function is identical to the update function for SHA2_224. + */ Hacl_Streaming_Types_error_code Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len); -/** -Write the resulting hash into `dst`, an array of 32 bytes. The state remains -valid after a call to `finish_256`, meaning the user may feed more data into -the hash via `update_256`. (The finish_256 function operates on an internal copy -of the state and therefore does not invalidate the client-held state `p`.) -*/ +/* + * Write the resulting hash into `dst`, an array of 32 bytes. The state remains + * valid after a call to `finish_256`, meaning the user may feed more data into + * the hash via `update_256`. (The finish_256 function operates on an internal + * copy of the state and therefore does not invalidate the client-held state + * `p`.) + */ void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst); -/** -Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. -*/ +/* + * Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. + */ void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, uint8_t *dst); @@ -159,45 +160,46 @@ Hacl_Streaming_Types_error_code Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len); -/** -Write the resulting hash into `dst`, an array of 28 bytes. The state remains -valid after a call to `finish_224`, meaning the user may feed more data into -the hash via `update_224`. -*/ +/* + * Write the resulting hash into `dst`, an array of 28 bytes. The state remains + * valid after a call to `finish_224`, meaning the user may feed more data into + * the hash via `update_224`. + */ void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst); -/** -Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. -*/ +/* + * Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. + */ void Hacl_Streaming_SHA2_hash_224(uint8_t *input, uint32_t input_len, uint8_t *dst); void Hacl_Streaming_SHA2_init_512(struct Hacl_Streaming_MD_state_64_s *s); -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_512` -(since the last call to `init_512`) exceeds 2^125-1 bytes. - -This function is identical to the update function for SHA2_384. -*/ +/* + * Feed an arbitrary amount of data into the hash. This function returns 0 for + * success, or 1 if the combined length of all of the data passed to + * `update_512` (since the last call to `init_512`) exceeds 2^125-1 bytes. + * + * This function is identical to the update function for SHA2_384. + */ Hacl_Streaming_Types_error_code Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len); -/** -Write the resulting hash into `dst`, an array of 64 bytes. The state remains -valid after a call to `finish_512`, meaning the user may feed more data into -the hash via `update_512`. (The finish_512 function operates on an internal copy -of the state and therefore does not invalidate the client-held state `p`.) -*/ +/* + * Write the resulting hash into `dst`, an array of 64 bytes. The state remains + * valid after a call to `finish_512`, meaning the user may feed more data into + * the hash via `update_512`. (The finish_512 function operates on an internal + * copy of the state and therefore does not invalidate the client-held state + * `p`.) + */ void Hacl_Streaming_SHA2_finish_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst); -/** -Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes. -*/ +/* + * Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes. + */ void Hacl_Streaming_SHA2_hash_512(uint8_t *input, uint32_t input_len, uint8_t *dst); @@ -207,16 +209,16 @@ Hacl_Streaming_Types_error_code Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len); -/** -Write the resulting hash into `dst`, an array of 48 bytes. The state remains -valid after a call to `finish_384`, meaning the user may feed more data into -the hash via `update_384`. -*/ +/* + * Write the resulting hash into `dst`, an array of 48 bytes. The state remains + * valid after a call to `finish_384`, meaning the user may feed more data into + * the hash via `update_384`. + */ void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst); -/** -Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. -*/ +/* + * Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. + */ void Hacl_Streaming_SHA2_hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst); diff --git a/crypto/hacl_lib.h b/crypto/hacl_lib.h index b6e3e015294d3..7ecb4db961767 100644 --- a/crypto/hacl_lib.h +++ b/crypto/hacl_lib.h @@ -30,8 +30,10 @@ static inline u128 FStar_UInt128_uint64_to_uint128(u64 x) return ((u128)x); } -/* Loads and stores. These avoid undefined behavior due to unaligned memory - * accesses, via memcpy. */ +/* + * Loads and stores. These avoid undefined behavior due to unaligned memory + * accesses, via memcpy. + */ #define load32_be(b) (get_unaligned_be32(b)) #define store32_be(b, i) put_unaligned_be32(i, b); diff --git a/crypto/sha2-hacl-generated.c b/crypto/sha2-hacl-generated.c index 9f3bfa4824219..a90e1cdc24a9f 100644 --- a/crypto/sha2-hacl-generated.c +++ b/crypto/sha2-hacl-generated.c @@ -912,11 +912,11 @@ Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, return update_384_512(p, input, input_len); } -/** -Write the resulting hash into `dst`, an array of 48 bytes. The state remains -valid after a call to `finish_384`, meaning the user may feed more data into -the hash via `update_384`. -*/ +/* + * Write the resulting hash into `dst`, an array of 48 bytes. The state remains + * valid after a call to `finish_384`, meaning the user may feed more data into + * the hash via `update_384`. + */ void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst) { From 0bf813846dce7780365e17ae5bff5b3e84f4307f Mon Sep 17 00:00:00 2001 From: armfazh Date: Mon, 16 Oct 2023 16:47:46 -0700 Subject: [PATCH 08/18] Adding CRYPTO_SHA2_HACL module. --- zeta/test-artifacts/config-um | 6 ++++++ zeta/test-artifacts/test-script.sh | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/zeta/test-artifacts/config-um b/zeta/test-artifacts/config-um index 06d98e23e21b5..b7c9b183457c6 100644 --- a/zeta/test-artifacts/config-um +++ b/zeta/test-artifacts/config-um @@ -1403,6 +1403,12 @@ CONFIG_CRYPTO_AUTHENC=y CONFIG_CRYPTO_TEST=m # end of Crypto core or helper +# +# HACL implementation +# +CONFIG_CRYPTO_SHA2_HACL=y +# end of HACL implementation + # # Public-key cryptography # diff --git a/zeta/test-artifacts/test-script.sh b/zeta/test-artifacts/test-script.sh index 1ff9b2df6fe9d..3a7b53c6db47d 100755 --- a/zeta/test-artifacts/test-script.sh +++ b/zeta/test-artifacts/test-script.sh @@ -1,5 +1,11 @@ #!/bin/busybox sh +echo "tcrypt: starting CRYPTO_SHA2_HACL" +modprobe tcrypt mode=300 alg=sha224-hacl sec=2 +modprobe tcrypt mode=300 alg=sha256-hacl sec=2 +modprobe tcrypt mode=300 alg=sha384-hacl sec=2 +modprobe tcrypt mode=300 alg=sha512-hacl sec=2 + echo "tcrypt: starting SHA2 (256) test" echo "tcrypt: testing sha256 generic implementation" modprobe tcrypt mode=300 alg=sha256-generic sec=2 From c2998c783091322b8787390932af4168844e5187 Mon Sep 17 00:00:00 2001 From: armfazh Date: Fri, 1 Dec 2023 20:21:00 -0800 Subject: [PATCH 09/18] Set correct version identifier. --- crypto/hacl_hash.h | 1 + crypto/hacl_lib.h | 1 + crypto/sha2-hacl-generated.c | 6 ++++-- crypto/sha2-hacl.c | 6 +++--- 4 files changed, 9 insertions(+), 5 deletions(-) diff --git a/crypto/hacl_hash.h b/crypto/hacl_hash.h index 1e10e54dfd6c2..80d8dd4ef2249 100644 --- a/crypto/hacl_hash.h +++ b/crypto/hacl_hash.h @@ -1,3 +1,4 @@ +/* SPDX-License-Identifier: GPL-2.0 OR MIT */ /* * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation * Copyright (c) 2022-2023 HACL* Contributors diff --git a/crypto/hacl_lib.h b/crypto/hacl_lib.h index 7ecb4db961767..12a9a3c2fcac4 100644 --- a/crypto/hacl_lib.h +++ b/crypto/hacl_lib.h @@ -1,3 +1,4 @@ +/* SPDX-License-Identifier: GPL-2.0 OR MIT */ /* * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation * Copyright (c) 2022-2023 HACL* Contributors diff --git a/crypto/sha2-hacl-generated.c b/crypto/sha2-hacl-generated.c index a90e1cdc24a9f..2084b2a19dd62 100644 --- a/crypto/sha2-hacl-generated.c +++ b/crypto/sha2-hacl-generated.c @@ -1,9 +1,9 @@ +// SPDX-License-Identifier: GPL-2.0 OR MIT /* - * GPLv2 or MIT License - * * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation * Copyright (c) 2022-2023 HACL* Contributors * + * This is a formally-verified implementation of SHA-2 produced by HACL*. */ #include "hacl_hash.h" @@ -951,3 +951,5 @@ void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, r, buf_last, tmp_block_state); Hacl_SHA2_Scalar32_sha384_finish(tmp_block_state, dst); } + +MODULE_LICENSE("Dual MIT/GPL"); diff --git a/crypto/sha2-hacl.c b/crypto/sha2-hacl.c index 6400fbce0ae0b..d5339c93949e3 100644 --- a/crypto/sha2-hacl.c +++ b/crypto/sha2-hacl.c @@ -1,8 +1,8 @@ +// SPDX-License-Identifier: GPL-2.0 OR MIT /* - * GPLv2 or MIT License - * * Copyright (c) 2023 Cryspen * + * This is a formally-verified implementation of SHA-2 produced by HACL*. */ #include @@ -178,7 +178,7 @@ static void __exit sha2_hacl_mod_fini(void) subsys_initcall(sha2_hacl_mod_init); module_exit(sha2_hacl_mod_fini); -MODULE_LICENSE("GPLv2 or MIT"); +MODULE_LICENSE("Dual MIT/GPL"); MODULE_DESCRIPTION("Formally Verified SHA-2 Secure Hash Algorithm from HACL*"); MODULE_ALIAS_CRYPTO("sha224"); From 37a16ff66085c4023038b6f21f8066d157e8436c Mon Sep 17 00:00:00 2001 From: armfazh Date: Fri, 1 Dec 2023 20:21:21 -0800 Subject: [PATCH 10/18] Compiles single module from multiple files. --- crypto/Kconfig | 11 ++++++++++- crypto/Makefile | 4 +++- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/crypto/Kconfig b/crypto/Kconfig index e35350102a433..d4fd42bc33da8 100644 --- a/crypto/Kconfig +++ b/crypto/Kconfig @@ -1027,11 +1027,20 @@ config CRYPTO_SHA256 Used by the btrfs filesystem, Ceph, NFS, and SMB. config CRYPTO_SHA2_HACL - tristate "SHA-224 and SHA-256 and SHA-384 and SHA-512" + tristate "SHA-2 (HACL*)" select CRYPTO_HASH help SHA-2 secure hash algorithms (FIPS 180, ISO/IEC 10118-3) from HACL* + This is a formally-verified implementation of SHA-2 ported + from the HACL* project. + + This module provides the following algorithms: + - SHA-224 + - SHA-256 + - SHA-384 + - SHA-512 + config CRYPTO_SHA512 tristate "SHA-384 and SHA-512" select CRYPTO_HASH diff --git a/crypto/Makefile b/crypto/Makefile index 2c88f3c8ce4db..d2706951763eb 100644 --- a/crypto/Makefile +++ b/crypto/Makefile @@ -77,7 +77,9 @@ obj-$(CONFIG_CRYPTO_MD5) += md5.o obj-$(CONFIG_CRYPTO_RMD160) += rmd160.o obj-$(CONFIG_CRYPTO_SHA1) += sha1_generic.o obj-$(CONFIG_CRYPTO_SHA256) += sha256_generic.o -obj-$(CONFIG_CRYPTO_SHA2_HACL) += sha2-hacl-generated.o sha2-hacl.o +sha2_hacl-y := sha2-hacl-generated.o +sha2_hacl-y += sha2-hacl.o +obj-$(CONFIG_CRYPTO_SHA2_HACL) += sha2_hacl.o obj-$(CONFIG_CRYPTO_SHA512) += sha512_generic.o obj-$(CONFIG_CRYPTO_SHA3) += sha3_generic.o obj-$(CONFIG_CRYPTO_SM3) += sm3.o From b1d172374779510b68d2eb05a297e23e01b4ab52 Mon Sep 17 00:00:00 2001 From: armfazh Date: Tue, 5 Dec 2023 10:48:36 -0800 Subject: [PATCH 11/18] Loading module manually, so we check whether it loads ok. --- zeta/test-artifacts/config-um | 2 +- zeta/test-artifacts/test-script.sh | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/zeta/test-artifacts/config-um b/zeta/test-artifacts/config-um index b7c9b183457c6..cd8025db42d49 100644 --- a/zeta/test-artifacts/config-um +++ b/zeta/test-artifacts/config-um @@ -1406,7 +1406,7 @@ CONFIG_CRYPTO_TEST=m # # HACL implementation # -CONFIG_CRYPTO_SHA2_HACL=y +CONFIG_CRYPTO_SHA2_HACL=m # end of HACL implementation # diff --git a/zeta/test-artifacts/test-script.sh b/zeta/test-artifacts/test-script.sh index 3a7b53c6db47d..f4777ebbdb3db 100755 --- a/zeta/test-artifacts/test-script.sh +++ b/zeta/test-artifacts/test-script.sh @@ -1,6 +1,7 @@ #!/bin/busybox sh echo "tcrypt: starting CRYPTO_SHA2_HACL" +modprobe sha2-hacl modprobe tcrypt mode=300 alg=sha224-hacl sec=2 modprobe tcrypt mode=300 alg=sha256-hacl sec=2 modprobe tcrypt mode=300 alg=sha384-hacl sec=2 From 376f49921e8e2c89196016b68ec813a4fa3e1cf1 Mon Sep 17 00:00:00 2001 From: armfazh Date: Tue, 5 Dec 2023 15:06:38 -0800 Subject: [PATCH 12/18] Fixing format of documentation strings for SHA2. --- crypto/sha2-hacl-generated.c | 82 ++++++++++++++++++------------------ 1 file changed, 42 insertions(+), 40 deletions(-) diff --git a/crypto/sha2-hacl-generated.c b/crypto/sha2-hacl-generated.c index 2084b2a19dd62..29a7136ed1b6f 100644 --- a/crypto/sha2-hacl-generated.c +++ b/crypto/sha2-hacl-generated.c @@ -191,9 +191,9 @@ void Hacl_SHA2_Scalar32_sha224_finish(uint32_t *st, uint8_t *h) memcpy(h, hbuf, (uint32_t)28U * sizeof(uint8_t)); } -/** -Reset an existing state to the initial hash state with empty data. -*/ +/* + * Reset an existing state to the initial hash state with empty data. + */ void Hacl_Streaming_SHA2_init_256(struct Hacl_Streaming_MD_state_32_s *s) { @@ -347,13 +347,13 @@ update_224_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *data, return Hacl_Streaming_Types_Success; } -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_256` -(since the last call to `init_256`) exceeds 2^61-1 bytes. - -This function is identical to the update function for SHA2_224. -*/ +/* + * Feed an arbitrary amount of data into the hash. This function returns 0 for + * success, or 1 if the combined length of all of the data passed to + * `update_256` (since the last call to `init_256`) exceeds 2^61-1 bytes. + * + * This function is identical to the update function for SHA2_224. + */ Hacl_Streaming_Types_error_code Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len) @@ -361,12 +361,13 @@ Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, return update_224_256(p, input, input_len); } -/** -Write the resulting hash into `dst`, an array of 32 bytes. The state remains -valid after a call to `finish_256`, meaning the user may feed more data into -the hash via `update_256`. (The finish_256 function operates on an internal copy -of the state and therefore does not invalidate the client-held state `p`.) -*/ +/* + * Write the resulting hash into `dst`, an array of 32 bytes. The state remains + * valid after a call to `finish_256`, meaning the user may feed more data into + * the hash via `update_256`. (The finish_256 function operates on an internal + * copy of the state and therefore does not invalidate the client-held state + * `p`.) + */ void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst) { @@ -400,9 +401,9 @@ void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, Hacl_SHA2_Scalar32_sha256_finish(tmp_block_state, dst); } -/** -Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. -*/ +/* + * Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. + */ void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, uint8_t *dst) { @@ -441,11 +442,11 @@ Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, return update_224_256(p, input, input_len); } -/** -Write the resulting hash into `dst`, an array of 28 bytes. The state remains -valid after a call to `finish_224`, meaning the user may feed more data into -the hash via `update_224`. -*/ +/* + * Write the resulting hash into `dst`, an array of 28 bytes. The state remains + * valid after a call to `finish_224`, meaning the user may feed more data into + * the hash via `update_224`. + */ void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst) { @@ -478,9 +479,9 @@ void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, Hacl_SHA2_Scalar32_sha224_finish(tmp_block_state, dst); } -/** -Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. -*/ +/* + * Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. + */ void Hacl_Streaming_SHA2_hash_224(uint8_t *input, uint32_t input_len, uint8_t *dst) { @@ -836,13 +837,13 @@ update_384_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *data, return Hacl_Streaming_Types_Success; } -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_512` -(since the last call to `init_512`) exceeds 2^125-1 bytes. - -This function is identical to the update function for SHA2_384. -*/ +/* + * Feed an arbitrary amount of data into the hash. This function returns 0 for + * success, or 1 if the combined length of all of the data passed to + * `update_512` (since the last call to `init_512`) exceeds 2^125-1 bytes. + * + * This function is identical to the update function for SHA2_384. + */ Hacl_Streaming_Types_error_code Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len) @@ -850,12 +851,13 @@ Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, return update_384_512(p, input, input_len); } -/** -Write the resulting hash into `dst`, an array of 64 bytes. The state remains -valid after a call to `finish_512`, meaning the user may feed more data into -the hash via `update_512`. (The finish_512 function operates on an internal copy -of the state and therefore does not invalidate the client-held state `p`.) -*/ +/* + * Write the resulting hash into `dst`, an array of 64 bytes. The state remains + * valid after a call to `finish_512`, meaning the user may feed more data into + * the hash via `update_512`. (The finish_512 function operates on an internal + * copy of the state and therefore does not invalidate the client-held state + * `p`.) + */ void Hacl_Streaming_SHA2_finish_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst) { From 8b4a455ccffba92e1395ede6a87e8354ca42cbf7 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Tue, 24 Oct 2023 16:32:13 +0200 Subject: [PATCH 13/18] hacl sha3 --- crypto/Kconfig | 6 + crypto/Makefile | 1 + crypto/hacl_hash.h | 42 +++ crypto/hacl_lib.h | 9 + crypto/sha3-hacl-generated.c | 581 +++++++++++++++++++++++++++++++++++ crypto/sha3-hacl.c | 149 +++++++++ 6 files changed, 788 insertions(+) create mode 100644 crypto/sha3-hacl-generated.c create mode 100644 crypto/sha3-hacl.c diff --git a/crypto/Kconfig b/crypto/Kconfig index d4fd42bc33da8..add9f42e305bb 100644 --- a/crypto/Kconfig +++ b/crypto/Kconfig @@ -1053,6 +1053,12 @@ config CRYPTO_SHA3 help SHA-3 secure hash algorithms (FIPS 202, ISO/IEC 10118-3) +config CRYPTO_SHA3_HACL + tristate "SHA-3" + select CRYPTO_HASH + help + SHA-3 secure hash algorithms (FIPS 202, ISO/IEC 10118-3) from HACL* + config CRYPTO_SM3 tristate diff --git a/crypto/Makefile b/crypto/Makefile index d2706951763eb..dabf78769e8f1 100644 --- a/crypto/Makefile +++ b/crypto/Makefile @@ -82,6 +82,7 @@ sha2_hacl-y += sha2-hacl.o obj-$(CONFIG_CRYPTO_SHA2_HACL) += sha2_hacl.o obj-$(CONFIG_CRYPTO_SHA512) += sha512_generic.o obj-$(CONFIG_CRYPTO_SHA3) += sha3_generic.o +obj-$(CONFIG_CRYPTO_SHA3_HACL) += sha3-hacl-generated.o sha3-hacl.o obj-$(CONFIG_CRYPTO_SM3) += sm3.o obj-$(CONFIG_CRYPTO_SM3_GENERIC) += sm3_generic.o obj-$(CONFIG_CRYPTO_STREEBOG) += streebog_generic.o diff --git a/crypto/hacl_hash.h b/crypto/hacl_hash.h index 80d8dd4ef2249..2de978ea7b945 100644 --- a/crypto/hacl_hash.h +++ b/crypto/hacl_hash.h @@ -10,6 +10,15 @@ #include "hacl_lib.h" +#define Spec_Hash_Definitions_SHA3_256 8 +#define Spec_Hash_Definitions_SHA3_224 9 +#define Spec_Hash_Definitions_SHA3_384 10 +#define Spec_Hash_Definitions_SHA3_512 11 +#define Spec_Hash_Definitions_Shake128 12 +#define Spec_Hash_Definitions_Shake256 13 + +typedef uint8_t Spec_Hash_Definitions_hash_alg; + #define Hacl_Streaming_Types_Success 0 #define Hacl_Streaming_Types_InvalidAlgorithm 1 #define Hacl_Streaming_Types_InvalidLength 2 @@ -223,4 +232,37 @@ void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, void Hacl_Streaming_SHA2_hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst); +struct Hacl_Streaming_Keccak_hash_buf_s { + Spec_Hash_Definitions_hash_alg fst; + uint64_t *snd; +}; + +struct Hacl_Streaming_Keccak_state_s { + struct Hacl_Streaming_Keccak_hash_buf_s block_state; + uint8_t *buf; + uint64_t total_len; +}; + +Hacl_Streaming_Types_error_code +Hacl_Streaming_Keccak_update(struct Hacl_Streaming_Keccak_state_s *p, + uint8_t *data, uint32_t len); + +Hacl_Streaming_Types_error_code +Hacl_Streaming_Keccak_finish(struct Hacl_Streaming_Keccak_state_s *p, + uint8_t *out); + +void Hacl_SHA3_shake128_hacl(uint32_t inputByteLen, uint8_t *input, + uint32_t outputByteLen, uint8_t *output); + +void Hacl_SHA3_shake256_hacl(uint32_t inputByteLen, uint8_t *input, + uint32_t outputByteLen, uint8_t *output); + +void Hacl_SHA3_sha3_224(uint32_t inputByteLen, uint8_t *input, uint8_t *output); + +void Hacl_SHA3_sha3_256(uint32_t inputByteLen, uint8_t *input, uint8_t *output); + +void Hacl_SHA3_sha3_384(uint32_t inputByteLen, uint8_t *input, uint8_t *output); + +void Hacl_SHA3_sha3_512(uint32_t inputByteLen, uint8_t *input, uint8_t *output); + #endif // CRYPTO_HACL_HASH_H_ diff --git a/crypto/hacl_lib.h b/crypto/hacl_lib.h index 12a9a3c2fcac4..04b5b1487b64f 100644 --- a/crypto/hacl_lib.h +++ b/crypto/hacl_lib.h @@ -41,6 +41,11 @@ static inline u128 FStar_UInt128_uint64_to_uint128(u64 x) #define load64_be(b) (get_unaligned_be64(b)) #define store64_be(b, i) put_unaligned_be64(i, b); +#define load32_le(b) (get_unaligned_le32(b)) +#define store32_le(b, i) put_unaligned_le32(i, b); +#define load64_le(b) (get_unaligned_le64(b)) +#define store64_le(b, i) put_unaligned_le64(i, b); + static inline void store128_be(u8 *buf, u128 x) { store64_be(buf, (u64)(x >> 64)); @@ -231,4 +236,8 @@ static inline void store128_be(u8 *buf, u128 x) #define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) #endif +#ifndef KRML_HOST_IGNORE +#define KRML_HOST_IGNORE(x) (void)(x) +#endif + #endif // CRYPTO_HACL_LIB_H_ diff --git a/crypto/sha3-hacl-generated.c b/crypto/sha3-hacl-generated.c new file mode 100644 index 0000000000000..53d624ccb166d --- /dev/null +++ b/crypto/sha3-hacl-generated.c @@ -0,0 +1,581 @@ +/* GPLv2 or MIT License + * + * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation + * Copyright (c) 2022-2023 HACL* Contributors + * + */ + +#include "hacl_hash.h" +#include "hacl_lib.h" + +static uint32_t block_len(Spec_Hash_Definitions_hash_alg a) +{ + switch (a) { + case Spec_Hash_Definitions_SHA3_224: { + return (uint32_t)144U; + } + case Spec_Hash_Definitions_SHA3_256: { + return (uint32_t)136U; + } + case Spec_Hash_Definitions_SHA3_384: { + return (uint32_t)104U; + } + case Spec_Hash_Definitions_SHA3_512: { + return (uint32_t)72U; + } + case Spec_Hash_Definitions_Shake128: { + return (uint32_t)168U; + } + case Spec_Hash_Definitions_Shake256: { + return (uint32_t)136U; + } + default: { + return (uint32_t)144U; + } + } +} + +static uint32_t hash_len(Spec_Hash_Definitions_hash_alg a) +{ + switch (a) { + case Spec_Hash_Definitions_SHA3_224: { + return (uint32_t)28U; + } + case Spec_Hash_Definitions_SHA3_256: { + return (uint32_t)32U; + } + case Spec_Hash_Definitions_SHA3_384: { + return (uint32_t)48U; + } + case Spec_Hash_Definitions_SHA3_512: { + return (uint32_t)64U; + } + default: { + return (uint32_t)64U; + } + } +} + +static void Hacl_Impl_SHA3_loadState(uint32_t rateInBytes, uint8_t *input, + uint64_t *s) +{ + uint8_t block[200U] = { 0U }; + memcpy(block, input, rateInBytes * sizeof(uint8_t)); + for (uint32_t i = (uint32_t)0U; i < (uint32_t)25U; i++) { + uint64_t u = load64_le(block + i * (uint32_t)8U); + uint64_t x = u; + s[i] = s[i] ^ x; + } +} + +static void storeState(uint32_t rateInBytes, uint64_t *s, uint8_t *res) +{ + uint8_t block[200U] = { 0U }; + for (uint32_t i = (uint32_t)0U; i < (uint32_t)25U; i++) { + uint64_t sj = s[i]; + store64_le(block + i * (uint32_t)8U, sj); + } + memcpy(res, block, rateInBytes * sizeof(uint8_t)); +} + +static const uint32_t keccak_rotc[24U] = { + (uint32_t)1U, (uint32_t)3U, (uint32_t)6U, (uint32_t)10U, + (uint32_t)15U, (uint32_t)21U, (uint32_t)28U, (uint32_t)36U, + (uint32_t)45U, (uint32_t)55U, (uint32_t)2U, (uint32_t)14U, + (uint32_t)27U, (uint32_t)41U, (uint32_t)56U, (uint32_t)8U, + (uint32_t)25U, (uint32_t)43U, (uint32_t)62U, (uint32_t)18U, + (uint32_t)39U, (uint32_t)61U, (uint32_t)20U, (uint32_t)44U +}; + +static const uint32_t keccak_piln[24U] = { + (uint32_t)10U, (uint32_t)7U, (uint32_t)11U, (uint32_t)17U, + (uint32_t)18U, (uint32_t)3U, (uint32_t)5U, (uint32_t)16U, + (uint32_t)8U, (uint32_t)21U, (uint32_t)24U, (uint32_t)4U, + (uint32_t)15U, (uint32_t)23U, (uint32_t)19U, (uint32_t)13U, + (uint32_t)12U, (uint32_t)2U, (uint32_t)20U, (uint32_t)14U, + (uint32_t)22U, (uint32_t)9U, (uint32_t)6U, (uint32_t)1U +}; + +static const uint64_t keccak_rndc[24U] = { + (uint64_t)0x0000000000000001U, (uint64_t)0x0000000000008082U, + (uint64_t)0x800000000000808aU, (uint64_t)0x8000000080008000U, + (uint64_t)0x000000000000808bU, (uint64_t)0x0000000080000001U, + (uint64_t)0x8000000080008081U, (uint64_t)0x8000000000008009U, + (uint64_t)0x000000000000008aU, (uint64_t)0x0000000000000088U, + (uint64_t)0x0000000080008009U, (uint64_t)0x000000008000000aU, + (uint64_t)0x000000008000808bU, (uint64_t)0x800000000000008bU, + (uint64_t)0x8000000000008089U, (uint64_t)0x8000000000008003U, + (uint64_t)0x8000000000008002U, (uint64_t)0x8000000000000080U, + (uint64_t)0x000000000000800aU, (uint64_t)0x800000008000000aU, + (uint64_t)0x8000000080008081U, (uint64_t)0x8000000000008080U, + (uint64_t)0x0000000080000001U, (uint64_t)0x8000000080008008U +}; + +static void Hacl_Impl_SHA3_state_permute(uint64_t *s) +{ + for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)24U; i0++) { + uint64_t _C[5U] = { 0U }; + KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, + _C[i] = s[i + (uint32_t)0U] ^ + (s[i + (uint32_t)5U] ^ + (s[i + (uint32_t)10U] ^ + (s[i + (uint32_t)15U] ^ + s[i + (uint32_t)20U])));); + KRML_MAYBE_FOR5( + i1, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, + uint64_t uu____0 = + _C[(i1 + (uint32_t)1U) % (uint32_t)5U]; + uint64_t _D = _C[(i1 + (uint32_t)4U) % (uint32_t)5U] ^ + (uu____0 << (uint32_t)1U | + uu____0 >> (uint32_t)63U); + KRML_MAYBE_FOR5( + i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, + s[i1 + (uint32_t)5U * i] = + s[i1 + (uint32_t)5U * i] ^ _D;);); + uint64_t x = s[1U]; + uint64_t curr = x; + for (uint32_t i = (uint32_t)0U; i < (uint32_t)24U; i++) { + uint32_t _Y = keccak_piln[i]; + uint32_t r = keccak_rotc[i]; + uint64_t temp = s[_Y]; + uint64_t uu____1 = curr; + s[_Y] = uu____1 << r | uu____1 >> ((uint32_t)64U - r); + curr = temp; + } + KRML_MAYBE_FOR5( + i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, + uint64_t v0 = s[(uint32_t)0U + (uint32_t)5U * i] ^ + (~s[(uint32_t)1U + (uint32_t)5U * i] & + s[(uint32_t)2U + (uint32_t)5U * i]); + uint64_t v1 = s[(uint32_t)1U + (uint32_t)5U * i] ^ + (~s[(uint32_t)2U + (uint32_t)5U * i] & + s[(uint32_t)3U + (uint32_t)5U * i]); + uint64_t v2 = s[(uint32_t)2U + (uint32_t)5U * i] ^ + (~s[(uint32_t)3U + (uint32_t)5U * i] & + s[(uint32_t)4U + (uint32_t)5U * i]); + uint64_t v3 = s[(uint32_t)3U + (uint32_t)5U * i] ^ + (~s[(uint32_t)4U + (uint32_t)5U * i] & + s[(uint32_t)0U + (uint32_t)5U * i]); + uint64_t v4 = s[(uint32_t)4U + (uint32_t)5U * i] ^ + (~s[(uint32_t)0U + (uint32_t)5U * i] & + s[(uint32_t)1U + (uint32_t)5U * i]); + s[(uint32_t)0U + (uint32_t)5U * i] = v0; + s[(uint32_t)1U + (uint32_t)5U * i] = v1; + s[(uint32_t)2U + (uint32_t)5U * i] = v2; + s[(uint32_t)3U + (uint32_t)5U * i] = v3; + s[(uint32_t)4U + (uint32_t)5U * i] = v4;); + uint64_t c = keccak_rndc[i0]; + s[0U] = s[0U] ^ c; + } +} + +static void Hacl_Impl_SHA3_absorb_inner(uint32_t rateInBytes, uint8_t *block, + uint64_t *s) +{ + Hacl_Impl_SHA3_loadState(rateInBytes, block, s); + Hacl_Impl_SHA3_state_permute(s); +} + +static void absorb(uint64_t *s, uint32_t rateInBytes, uint32_t inputByteLen, + uint8_t *input, uint8_t delimitedSuffix) +{ + uint32_t n_blocks = inputByteLen / rateInBytes; + uint32_t rem = inputByteLen % rateInBytes; + for (uint32_t i = (uint32_t)0U; i < n_blocks; i++) { + uint8_t *block = input + i * rateInBytes; + Hacl_Impl_SHA3_absorb_inner(rateInBytes, block, s); + } + uint8_t *last = input + n_blocks * rateInBytes; + uint8_t lastBlock_[200U] = { 0U }; + uint8_t *lastBlock = lastBlock_; + memcpy(lastBlock, last, rem * sizeof(uint8_t)); + lastBlock[rem] = delimitedSuffix; + Hacl_Impl_SHA3_loadState(rateInBytes, lastBlock, s); + if (!((delimitedSuffix & (uint8_t)0x80U) == (uint8_t)0U) && + rem == rateInBytes - (uint32_t)1U) { + Hacl_Impl_SHA3_state_permute(s); + } + uint8_t nextBlock_[200U] = { 0U }; + uint8_t *nextBlock = nextBlock_; + nextBlock[rateInBytes - (uint32_t)1U] = (uint8_t)0x80U; + Hacl_Impl_SHA3_loadState(rateInBytes, nextBlock, s); + Hacl_Impl_SHA3_state_permute(s); +} + +static void Hacl_Hash_SHA3_update_multi_sha3(Spec_Hash_Definitions_hash_alg a, + uint64_t *s, uint8_t *blocks, + uint32_t n_blocks) +{ + for (uint32_t i = (uint32_t)0U; i < n_blocks; i++) { + uint8_t *block = blocks + i * block_len(a); + Hacl_Impl_SHA3_absorb_inner(block_len(a), block, s); + } +} + +static void Hacl_Hash_SHA3_update_last_sha3(Spec_Hash_Definitions_hash_alg a, + uint64_t *s, uint8_t *input, + uint32_t input_len) +{ + uint8_t suffix; + if (a == Spec_Hash_Definitions_Shake128 || + a == Spec_Hash_Definitions_Shake256) { + suffix = (uint8_t)0x1fU; + } else { + suffix = (uint8_t)0x06U; + } + uint32_t len = block_len(a); + if (input_len == len) { + Hacl_Impl_SHA3_absorb_inner(len, input, s); + uint8_t *uu____0 = input + input_len; + uint8_t lastBlock_[200U] = { 0U }; + uint8_t *lastBlock = lastBlock_; + memcpy(lastBlock, uu____0, (uint32_t)0U * sizeof(uint8_t)); + lastBlock[0U] = suffix; + Hacl_Impl_SHA3_loadState(len, lastBlock, s); + if (!((suffix & (uint8_t)0x80U) == (uint8_t)0U) && + (uint32_t)0U == len - (uint32_t)1U) { + Hacl_Impl_SHA3_state_permute(s); + } + uint8_t nextBlock_[200U] = { 0U }; + uint8_t *nextBlock = nextBlock_; + nextBlock[len - (uint32_t)1U] = (uint8_t)0x80U; + Hacl_Impl_SHA3_loadState(len, nextBlock, s); + Hacl_Impl_SHA3_state_permute(s); + return; + } + uint8_t lastBlock_[200U] = { 0U }; + uint8_t *lastBlock = lastBlock_; + memcpy(lastBlock, input, input_len * sizeof(uint8_t)); + lastBlock[input_len] = suffix; + Hacl_Impl_SHA3_loadState(len, lastBlock, s); + if (!((suffix & (uint8_t)0x80U) == (uint8_t)0U) && + input_len == len - (uint32_t)1U) { + Hacl_Impl_SHA3_state_permute(s); + } + uint8_t nextBlock_[200U] = { 0U }; + uint8_t *nextBlock = nextBlock_; + nextBlock[len - (uint32_t)1U] = (uint8_t)0x80U; + Hacl_Impl_SHA3_loadState(len, nextBlock, s); + Hacl_Impl_SHA3_state_permute(s); +} + +typedef struct hash_buf2_s { + struct Hacl_Streaming_Keccak_hash_buf_s fst; + struct Hacl_Streaming_Keccak_hash_buf_s snd; +} hash_buf2; + +static Spec_Hash_Definitions_hash_alg +Hacl_Streaming_Keccak_get_alg(struct Hacl_Streaming_Keccak_state_s *s) +{ + struct Hacl_Streaming_Keccak_state_s scrut = *s; + struct Hacl_Streaming_Keccak_hash_buf_s block_state = scrut.block_state; + return block_state.fst; +} + +void Hacl_Streaming_Keccak_reset(struct Hacl_Streaming_Keccak_state_s *s) +{ + struct Hacl_Streaming_Keccak_state_s scrut = *s; + uint8_t *buf = scrut.buf; + struct Hacl_Streaming_Keccak_hash_buf_s block_state = scrut.block_state; + Spec_Hash_Definitions_hash_alg i = block_state.fst; + KRML_HOST_IGNORE(i); + uint64_t *s1 = block_state.snd; + memset(s1, 0U, (uint32_t)25U * sizeof(uint64_t)); + struct Hacl_Streaming_Keccak_state_s tmp = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; + s[0U] = tmp; +} + +Hacl_Streaming_Types_error_code +Hacl_Streaming_Keccak_update(struct Hacl_Streaming_Keccak_state_s *p, + uint8_t *data, uint32_t len) +{ + struct Hacl_Streaming_Keccak_state_s s = *p; + struct Hacl_Streaming_Keccak_hash_buf_s block_state = s.block_state; + uint64_t total_len = s.total_len; + Spec_Hash_Definitions_hash_alg i = block_state.fst; + if ((uint64_t)len > (uint64_t)0xFFFFFFFFFFFFFFFFU - total_len) { + return Hacl_Streaming_Types_MaximumLengthExceeded; + } + uint32_t sz; + if (total_len % (uint64_t)block_len(i) == (uint64_t)0U && + total_len > (uint64_t)0U) { + sz = block_len(i); + } else { + sz = (uint32_t)(total_len % (uint64_t)block_len(i)); + } + if (len <= block_len(i) - sz) { + struct Hacl_Streaming_Keccak_state_s s1 = *p; + struct Hacl_Streaming_Keccak_hash_buf_s block_state1 = + s1.block_state; + uint8_t *buf = s1.buf; + uint64_t total_len1 = s1.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)block_len(i) == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = block_len(i); + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)block_len(i)); + } + uint8_t *buf2 = buf + sz1; + memcpy(buf2, data, len * sizeof(uint8_t)); + uint64_t total_len2 = total_len1 + (uint64_t)len; + *p = ((struct Hacl_Streaming_Keccak_state_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len2 }); + } else if (sz == (uint32_t)0U) { + struct Hacl_Streaming_Keccak_state_s s1 = *p; + struct Hacl_Streaming_Keccak_hash_buf_s block_state1 = + s1.block_state; + uint8_t *buf = s1.buf; + uint64_t total_len1 = s1.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)block_len(i) == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = block_len(i); + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)block_len(i)); + } + if (!(sz1 == (uint32_t)0U)) { + Spec_Hash_Definitions_hash_alg a1 = block_state1.fst; + uint64_t *s2 = block_state1.snd; + Hacl_Hash_SHA3_update_multi_sha3( + a1, s2, buf, block_len(i) / block_len(a1)); + } + uint32_t ite; + if ((uint64_t)len % (uint64_t)block_len(i) == (uint64_t)0U && + (uint64_t)len > (uint64_t)0U) { + ite = block_len(i); + } else { + ite = (uint32_t)((uint64_t)len % + (uint64_t)block_len(i)); + } + uint32_t n_blocks = (len - ite) / block_len(i); + uint32_t data1_len = n_blocks * block_len(i); + uint32_t data2_len = len - data1_len; + uint8_t *data1 = data; + uint8_t *data2 = data + data1_len; + Spec_Hash_Definitions_hash_alg a1 = block_state1.fst; + uint64_t *s2 = block_state1.snd; + Hacl_Hash_SHA3_update_multi_sha3(a1, s2, data1, + data1_len / block_len(a1)); + uint8_t *dst = buf; + memcpy(dst, data2, data2_len * sizeof(uint8_t)); + *p = ((struct Hacl_Streaming_Keccak_state_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)len }); + } else { + uint32_t diff = block_len(i) - sz; + uint8_t *data1 = data; + uint8_t *data2 = data + diff; + struct Hacl_Streaming_Keccak_state_s s1 = *p; + struct Hacl_Streaming_Keccak_hash_buf_s block_state10 = + s1.block_state; + uint8_t *buf0 = s1.buf; + uint64_t total_len10 = s1.total_len; + uint32_t sz10; + if (total_len10 % (uint64_t)block_len(i) == (uint64_t)0U && + total_len10 > (uint64_t)0U) { + sz10 = block_len(i); + } else { + sz10 = (uint32_t)(total_len10 % (uint64_t)block_len(i)); + } + uint8_t *buf2 = buf0 + sz10; + memcpy(buf2, data1, diff * sizeof(uint8_t)); + uint64_t total_len2 = total_len10 + (uint64_t)diff; + *p = ((struct Hacl_Streaming_Keccak_state_s){ + .block_state = block_state10, + .buf = buf0, + .total_len = total_len2 }); + struct Hacl_Streaming_Keccak_state_s s10 = *p; + struct Hacl_Streaming_Keccak_hash_buf_s block_state1 = + s10.block_state; + uint8_t *buf = s10.buf; + uint64_t total_len1 = s10.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)block_len(i) == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = block_len(i); + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)block_len(i)); + } + if (!(sz1 == (uint32_t)0U)) { + Spec_Hash_Definitions_hash_alg a1 = block_state1.fst; + uint64_t *s2 = block_state1.snd; + Hacl_Hash_SHA3_update_multi_sha3( + a1, s2, buf, block_len(i) / block_len(a1)); + } + uint32_t ite; + if ((uint64_t)(len - diff) % (uint64_t)block_len(i) == + (uint64_t)0U && + (uint64_t)(len - diff) > (uint64_t)0U) { + ite = block_len(i); + } else { + ite = (uint32_t)((uint64_t)(len - diff) % + (uint64_t)block_len(i)); + } + uint32_t n_blocks = (len - diff - ite) / block_len(i); + uint32_t data1_len = n_blocks * block_len(i); + uint32_t data2_len = len - diff - data1_len; + uint8_t *data11 = data2; + uint8_t *data21 = data2 + data1_len; + Spec_Hash_Definitions_hash_alg a1 = block_state1.fst; + uint64_t *s2 = block_state1.snd; + Hacl_Hash_SHA3_update_multi_sha3(a1, s2, data11, + data1_len / block_len(a1)); + uint8_t *dst = buf; + memcpy(dst, data21, data2_len * sizeof(uint8_t)); + *p = ((struct Hacl_Streaming_Keccak_state_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)(len - diff) }); + } + return Hacl_Streaming_Types_Success; +} + +static void Hacl_Impl_SHA3_squeeze(uint64_t *s, uint32_t rateInBytes, + uint32_t outputByteLen, uint8_t *output) +{ + uint32_t outBlocks = outputByteLen / rateInBytes; + uint32_t remOut = outputByteLen % rateInBytes; + uint8_t *last = output + outputByteLen - remOut; + uint8_t *blocks = output; + for (uint32_t i = (uint32_t)0U; i < outBlocks; i++) { + storeState(rateInBytes, s, blocks + i * rateInBytes); + Hacl_Impl_SHA3_state_permute(s); + } + storeState(remOut, s, last); +} + +static void finish_(Spec_Hash_Definitions_hash_alg a, + struct Hacl_Streaming_Keccak_state_s *p, uint8_t *dst, + uint32_t l) +{ + struct Hacl_Streaming_Keccak_state_s scrut0 = *p; + struct Hacl_Streaming_Keccak_hash_buf_s block_state = + scrut0.block_state; + uint8_t *buf_ = scrut0.buf; + uint64_t total_len = scrut0.total_len; + uint32_t r; + if (total_len % (uint64_t)block_len(a) == (uint64_t)0U && + total_len > (uint64_t)0U) { + r = block_len(a); + } else { + r = (uint32_t)(total_len % (uint64_t)block_len(a)); + } + uint8_t *buf_1 = buf_; + uint64_t buf[25U] = { 0U }; + struct Hacl_Streaming_Keccak_hash_buf_s tmp_block_state = { + .fst = a, .snd = buf + }; + hash_buf2 scrut = { .fst = block_state, .snd = tmp_block_state }; + uint64_t *s_dst = scrut.snd.snd; + uint64_t *s_src = scrut.fst.snd; + memcpy(s_dst, s_src, (uint32_t)25U * sizeof(uint64_t)); + uint32_t ite; + if (r % block_len(a) == (uint32_t)0U && r > (uint32_t)0U) { + ite = block_len(a); + } else { + ite = r % block_len(a); + } + uint8_t *buf_last = buf_1 + r - ite; + uint8_t *buf_multi = buf_1; + Spec_Hash_Definitions_hash_alg a1 = tmp_block_state.fst; + uint64_t *s0 = tmp_block_state.snd; + Hacl_Hash_SHA3_update_multi_sha3(a1, s0, buf_multi, + (uint32_t)0U / block_len(a1)); + Spec_Hash_Definitions_hash_alg a10 = tmp_block_state.fst; + uint64_t *s1 = tmp_block_state.snd; + Hacl_Hash_SHA3_update_last_sha3(a10, s1, buf_last, r); + Spec_Hash_Definitions_hash_alg a11 = tmp_block_state.fst; + uint64_t *s = tmp_block_state.snd; + if (a11 == Spec_Hash_Definitions_Shake128 || + a11 == Spec_Hash_Definitions_Shake256) { + Hacl_Impl_SHA3_squeeze(s, block_len(a11), l, dst); + return; + } + Hacl_Impl_SHA3_squeeze(s, block_len(a11), hash_len(a11), dst); +} + +Hacl_Streaming_Types_error_code +Hacl_Streaming_Keccak_finish(struct Hacl_Streaming_Keccak_state_s *s, + uint8_t *dst) +{ + Spec_Hash_Definitions_hash_alg a1 = Hacl_Streaming_Keccak_get_alg(s); + if (a1 == Spec_Hash_Definitions_Shake128 || + a1 == Spec_Hash_Definitions_Shake256) { + return Hacl_Streaming_Types_InvalidAlgorithm; + } + finish_(a1, s, dst, hash_len(a1)); + return Hacl_Streaming_Types_Success; +} + +Hacl_Streaming_Types_error_code +Hacl_Streaming_Keccak_squeeze(struct Hacl_Streaming_Keccak_state_s *s, + uint8_t *dst, uint32_t l) +{ + Spec_Hash_Definitions_hash_alg a1 = Hacl_Streaming_Keccak_get_alg(s); + if (!(a1 == Spec_Hash_Definitions_Shake128 || + a1 == Spec_Hash_Definitions_Shake256)) { + return Hacl_Streaming_Types_InvalidAlgorithm; + } + if (l == (uint32_t)0U) { + return Hacl_Streaming_Types_InvalidLength; + } + finish_(a1, s, dst, l); + return Hacl_Streaming_Types_Success; +} + +static void Hacl_Impl_SHA3_keccak(uint32_t rate, uint32_t capacity, + uint32_t inputByteLen, uint8_t *input, + uint8_t delimitedSuffix, + uint32_t outputByteLen, uint8_t *output) +{ + uint32_t rateInBytes = rate / (uint32_t)8U; + uint64_t s[25U] = { 0U }; + absorb(s, rateInBytes, inputByteLen, input, delimitedSuffix); + Hacl_Impl_SHA3_squeeze(s, rateInBytes, outputByteLen, output); +} + +void Hacl_SHA3_shake128_hacl(uint32_t inputByteLen, uint8_t *input, + uint32_t outputByteLen, uint8_t *output) +{ + Hacl_Impl_SHA3_keccak((uint32_t)1344U, (uint32_t)256U, inputByteLen, + input, (uint8_t)0x1FU, outputByteLen, output); +} + +void Hacl_SHA3_shake256_hacl(uint32_t inputByteLen, uint8_t *input, + uint32_t outputByteLen, uint8_t *output) +{ + Hacl_Impl_SHA3_keccak((uint32_t)1088U, (uint32_t)512U, inputByteLen, + input, (uint8_t)0x1FU, outputByteLen, output); +} + +void Hacl_SHA3_sha3_224(uint32_t inputByteLen, uint8_t *input, uint8_t *output) +{ + Hacl_Impl_SHA3_keccak((uint32_t)1152U, (uint32_t)448U, inputByteLen, + input, (uint8_t)0x06U, (uint32_t)28U, output); +} + +void Hacl_SHA3_sha3_256(uint32_t inputByteLen, uint8_t *input, uint8_t *output) +{ + Hacl_Impl_SHA3_keccak((uint32_t)1088U, (uint32_t)512U, inputByteLen, + input, (uint8_t)0x06U, (uint32_t)32U, output); +} + +void Hacl_SHA3_sha3_384(uint32_t inputByteLen, uint8_t *input, uint8_t *output) +{ + Hacl_Impl_SHA3_keccak((uint32_t)832U, (uint32_t)768U, inputByteLen, + input, (uint8_t)0x06U, (uint32_t)48U, output); +} + +void Hacl_SHA3_sha3_512(uint32_t inputByteLen, uint8_t *input, uint8_t *output) +{ + Hacl_Impl_SHA3_keccak((uint32_t)576U, (uint32_t)1024U, inputByteLen, + input, (uint8_t)0x06U, (uint32_t)64U, output); +} diff --git a/crypto/sha3-hacl.c b/crypto/sha3-hacl.c new file mode 100644 index 0000000000000..70957a40166d6 --- /dev/null +++ b/crypto/sha3-hacl.c @@ -0,0 +1,149 @@ +/* GPLv2 or MIT License + * + * Copyright (c) 2023 Cryspen + * + */ + +#include + +#include "hacl_hash.h" +#include "hacl_lib.h" + +int hacl_sha3_init(struct shash_desc *desc) +{ + struct sha3_state *sctx = shash_desc_ctx(desc); + unsigned int digest_size = crypto_shash_digestsize(desc->tfm); + sctx->rsiz = 200 - 2 * digest_size; + sctx->rsizw = sctx->rsiz / 8; + sctx->partial = 0; + memset(sctx->st, 0, sizeof(sctx->st)); + return 0; +} +EXPORT_SYMBOL(hacl_sha3_init); + +Spec_Hash_Definitions_hash_alg hacl_sha3_alg(unsigned int rsiz) +{ + switch (rsiz) { + case 144: { + return Spec_Hash_Definitions_SHA3_224; + } + case 136: { + return Spec_Hash_Definitions_SHA3_256; + } + case 104: { + return Spec_Hash_Definitions_SHA3_384; + } + case 72: { + return Spec_Hash_Definitions_SHA3_512; + } + default: { + return Spec_Hash_Definitions_SHA3_256; + } + } +} + +int hacl_sha3_update(struct shash_desc *desc, const u8 *data, unsigned int len) +{ + struct sha3_state *sctx = shash_desc_ctx(desc); + struct Hacl_Streaming_Keccak_state_s st; + st.block_state.fst = hacl_sha3_alg(sctx->rsiz); + st.block_state.snd = sctx->st; + st.buf = sctx->buf; + st.total_len = 0; + uint8_t ret = Hacl_Streaming_Keccak_update(&st, (uint8_t *)data, len); + if (ret > 0) { + return -1; + } else { + return 0; + } +} +EXPORT_SYMBOL(hacl_sha3_update); + +int hacl_sha3_final(struct shash_desc *desc, u8 *out) +{ + struct sha3_state *sctx = shash_desc_ctx(desc); + struct Hacl_Streaming_Keccak_state_s st; + st.block_state.fst = hacl_sha3_alg(sctx->rsiz); + st.block_state.snd = sctx->st; + st.buf = sctx->buf; + st.total_len = 0; + uint8_t ret = Hacl_Streaming_Keccak_finish(&st, out); + if (ret > 0) { + return -1; + } else { + return 0; + } +} +EXPORT_SYMBOL(hacl_sha3_final); + +static struct shash_alg algs[] = { + { + .digestsize = SHA3_224_DIGEST_SIZE, + .init = hacl_sha3_init, + .update = hacl_sha3_update, + .final = hacl_sha3_final, + .descsize = sizeof(struct sha3_state), + .base.cra_name = "sha3-224", + .base.cra_driver_name = "sha3-224-hacl", + .base.cra_blocksize = SHA3_224_BLOCK_SIZE, + .base.cra_module = THIS_MODULE, + }, + { + .digestsize = SHA3_256_DIGEST_SIZE, + .init = hacl_sha3_init, + .update = hacl_sha3_update, + .final = hacl_sha3_final, + .descsize = sizeof(struct sha3_state), + .base.cra_name = "sha3-256", + .base.cra_driver_name = "sha3-256-hacl", + .base.cra_blocksize = SHA3_256_BLOCK_SIZE, + .base.cra_module = THIS_MODULE, + }, + { + .digestsize = SHA3_384_DIGEST_SIZE, + .init = hacl_sha3_init, + .update = hacl_sha3_update, + .final = hacl_sha3_final, + .descsize = sizeof(struct sha3_state), + .base.cra_name = "sha3-384", + .base.cra_driver_name = "sha3-384-hacl", + .base.cra_blocksize = SHA3_384_BLOCK_SIZE, + .base.cra_module = THIS_MODULE, + }, + { + .digestsize = SHA3_512_DIGEST_SIZE, + .init = hacl_sha3_init, + .update = hacl_sha3_update, + .final = hacl_sha3_final, + .descsize = sizeof(struct sha3_state), + .base.cra_name = "sha3-512", + .base.cra_driver_name = "sha3-512-hacl", + .base.cra_blocksize = SHA3_512_BLOCK_SIZE, + .base.cra_module = THIS_MODULE, + } +}; + +static int __init sha3_hacl_mod_init(void) +{ + return crypto_register_shashes(algs, ARRAY_SIZE(algs)); +} + +static void __exit sha3_hacl_mod_fini(void) +{ + crypto_unregister_shashes(algs, ARRAY_SIZE(algs)); +} + +subsys_initcall(sha3_hacl_mod_init); +module_exit(sha3_hacl_mod_fini); + +MODULE_LICENSE("GPLv2 or MIT"); +MODULE_DESCRIPTION("Formally Verified SHA-3 Secure Hash Algorithm from HACL*"); + +MODULE_ALIAS_CRYPTO("sha3-224"); +MODULE_ALIAS_CRYPTO("sha3-224-hacl"); +MODULE_ALIAS_CRYPTO("sha3-256"); +MODULE_ALIAS_CRYPTO("sha3-256-hacl"); +MODULE_ALIAS_CRYPTO("sha3-384"); +MODULE_ALIAS_CRYPTO("sha3-384-hacl"); +MODULE_ALIAS_CRYPTO("sha3-512"); +MODULE_ALIAS_CRYPTO("sha3-512-hacl"); From 09be30b9db413a08946cc8dba71aea6980944288 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Tue, 24 Oct 2023 17:18:30 +0200 Subject: [PATCH 14/18] run ci --- .github/workflows/crypto-test-harness.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/crypto-test-harness.yml b/.github/workflows/crypto-test-harness.yml index 19e1791e838c8..67fc1a643eec1 100644 --- a/.github/workflows/crypto-test-harness.yml +++ b/.github/workflows/crypto-test-harness.yml @@ -3,7 +3,6 @@ name: Linux on: pull_request: - branches: ["cf-zeta"] workflow_dispatch: jobs: From 81fc44ece1ef5ef69ca1433149f4f812717d515e Mon Sep 17 00:00:00 2001 From: armfazh Date: Tue, 5 Dec 2023 15:30:26 -0800 Subject: [PATCH 15/18] Fixing license and compilation of module for SHA3. --- crypto/Kconfig | 11 ++++++++++- crypto/Makefile | 4 +++- crypto/sha3-hacl-generated.c | 13 ++++++++----- crypto/sha3-hacl.c | 7 ++++--- include/crypto/sha3.h | 4 ++++ 5 files changed, 29 insertions(+), 10 deletions(-) diff --git a/crypto/Kconfig b/crypto/Kconfig index add9f42e305bb..8b6b633c70353 100644 --- a/crypto/Kconfig +++ b/crypto/Kconfig @@ -1054,11 +1054,20 @@ config CRYPTO_SHA3 SHA-3 secure hash algorithms (FIPS 202, ISO/IEC 10118-3) config CRYPTO_SHA3_HACL - tristate "SHA-3" + tristate "SHA-3 (HACL*)" select CRYPTO_HASH help SHA-3 secure hash algorithms (FIPS 202, ISO/IEC 10118-3) from HACL* + This is a formally-verified implementation of SHA-3 ported + from the HACL* project. + + This module provides the following algorithms: + - SHA3-224 + - SHA3-256 + - SHA3-384 + - SHA3-512 + config CRYPTO_SM3 tristate diff --git a/crypto/Makefile b/crypto/Makefile index dabf78769e8f1..82a379ca222d1 100644 --- a/crypto/Makefile +++ b/crypto/Makefile @@ -82,7 +82,9 @@ sha2_hacl-y += sha2-hacl.o obj-$(CONFIG_CRYPTO_SHA2_HACL) += sha2_hacl.o obj-$(CONFIG_CRYPTO_SHA512) += sha512_generic.o obj-$(CONFIG_CRYPTO_SHA3) += sha3_generic.o -obj-$(CONFIG_CRYPTO_SHA3_HACL) += sha3-hacl-generated.o sha3-hacl.o +sha3_hacl-y := sha3-hacl-generated.o +sha3_hacl-y += sha3-hacl.o +obj-$(CONFIG_CRYPTO_SHA3_HACL) += sha3_hacl.o obj-$(CONFIG_CRYPTO_SM3) += sm3.o obj-$(CONFIG_CRYPTO_SM3_GENERIC) += sm3_generic.o obj-$(CONFIG_CRYPTO_STREEBOG) += streebog_generic.o diff --git a/crypto/sha3-hacl-generated.c b/crypto/sha3-hacl-generated.c index 53d624ccb166d..c021d5b73dad2 100644 --- a/crypto/sha3-hacl-generated.c +++ b/crypto/sha3-hacl-generated.c @@ -1,8 +1,9 @@ -/* GPLv2 or MIT License - * +// SPDX-License-Identifier: GPL-2.0 OR MIT +/* * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation * Copyright (c) 2022-2023 HACL* Contributors * + * This is a formally-verified implementation of SHA-3 produced by HACL*. */ #include "hacl_hash.h" @@ -259,10 +260,10 @@ static void Hacl_Hash_SHA3_update_last_sha3(Spec_Hash_Definitions_hash_alg a, Hacl_Impl_SHA3_state_permute(s); } -typedef struct hash_buf2_s { +struct hash_buf2 { struct Hacl_Streaming_Keccak_hash_buf_s fst; struct Hacl_Streaming_Keccak_hash_buf_s snd; -} hash_buf2; +}; static Spec_Hash_Definitions_hash_alg Hacl_Streaming_Keccak_get_alg(struct Hacl_Streaming_Keccak_state_s *s) @@ -473,7 +474,7 @@ static void finish_(Spec_Hash_Definitions_hash_alg a, struct Hacl_Streaming_Keccak_hash_buf_s tmp_block_state = { .fst = a, .snd = buf }; - hash_buf2 scrut = { .fst = block_state, .snd = tmp_block_state }; + struct hash_buf2 scrut = { .fst = block_state, .snd = tmp_block_state }; uint64_t *s_dst = scrut.snd.snd; uint64_t *s_src = scrut.fst.snd; memcpy(s_dst, s_src, (uint32_t)25U * sizeof(uint64_t)); @@ -579,3 +580,5 @@ void Hacl_SHA3_sha3_512(uint32_t inputByteLen, uint8_t *input, uint8_t *output) Hacl_Impl_SHA3_keccak((uint32_t)576U, (uint32_t)1024U, inputByteLen, input, (uint8_t)0x06U, (uint32_t)64U, output); } + +MODULE_LICENSE("Dual MIT/GPL"); diff --git a/crypto/sha3-hacl.c b/crypto/sha3-hacl.c index 70957a40166d6..04ad8fd3c9ad0 100644 --- a/crypto/sha3-hacl.c +++ b/crypto/sha3-hacl.c @@ -1,7 +1,8 @@ -/* GPLv2 or MIT License - * +// SPDX-License-Identifier: GPL-2.0 OR MIT +/* * Copyright (c) 2023 Cryspen * + * This is a formally-verified implementation of SHA-3 produced by HACL*. */ #include @@ -136,7 +137,7 @@ static void __exit sha3_hacl_mod_fini(void) subsys_initcall(sha3_hacl_mod_init); module_exit(sha3_hacl_mod_fini); -MODULE_LICENSE("GPLv2 or MIT"); +MODULE_LICENSE("Dual MIT/GPL"); MODULE_DESCRIPTION("Formally Verified SHA-3 Secure Hash Algorithm from HACL*"); MODULE_ALIAS_CRYPTO("sha3-224"); diff --git a/include/crypto/sha3.h b/include/crypto/sha3.h index 080f60c2e6b16..f92e15b2e8e98 100644 --- a/include/crypto/sha3.h +++ b/include/crypto/sha3.h @@ -5,6 +5,8 @@ #ifndef __CRYPTO_SHA3_H__ #define __CRYPTO_SHA3_H__ +#include + #define SHA3_224_DIGEST_SIZE (224 / 8) #define SHA3_224_BLOCK_SIZE (200 - 2 * SHA3_224_DIGEST_SIZE) @@ -26,6 +28,8 @@ struct sha3_state { u8 buf[SHA3_224_BLOCK_SIZE]; }; +struct shash_desc; + int crypto_sha3_init(struct shash_desc *desc); int crypto_sha3_update(struct shash_desc *desc, const u8 *data, unsigned int len); From f04cd5221a58e0849df5d3f257fbc6b12dc20ab9 Mon Sep 17 00:00:00 2001 From: armfazh Date: Mon, 11 Dec 2023 17:08:08 -0800 Subject: [PATCH 16/18] Run SHA3 in CI. --- zeta/test-artifacts/config-um | 1 + zeta/test-artifacts/test-script.sh | 7 +++++++ 2 files changed, 8 insertions(+) diff --git a/zeta/test-artifacts/config-um b/zeta/test-artifacts/config-um index cd8025db42d49..a7acf4ac81674 100644 --- a/zeta/test-artifacts/config-um +++ b/zeta/test-artifacts/config-um @@ -1407,6 +1407,7 @@ CONFIG_CRYPTO_TEST=m # HACL implementation # CONFIG_CRYPTO_SHA2_HACL=m +CONFIG_CRYPTO_SHA3_HACL=m # end of HACL implementation # diff --git a/zeta/test-artifacts/test-script.sh b/zeta/test-artifacts/test-script.sh index f4777ebbdb3db..efaebdf331491 100755 --- a/zeta/test-artifacts/test-script.sh +++ b/zeta/test-artifacts/test-script.sh @@ -7,6 +7,13 @@ modprobe tcrypt mode=300 alg=sha256-hacl sec=2 modprobe tcrypt mode=300 alg=sha384-hacl sec=2 modprobe tcrypt mode=300 alg=sha512-hacl sec=2 +echo "tcrypt: starting CRYPTO_SHA3_HACL" +modprobe sha3-hacl +modprobe tcrypt mode=300 alg=sha3-224-hacl sec=2 +modprobe tcrypt mode=300 alg=sha3-256-hacl sec=2 +modprobe tcrypt mode=300 alg=sha3-384-hacl sec=2 +modprobe tcrypt mode=300 alg=sha3-512-hacl sec=2 + echo "tcrypt: starting SHA2 (256) test" echo "tcrypt: testing sha256 generic implementation" modprobe tcrypt mode=300 alg=sha256-generic sec=2 From 7db50bfc92d7e81788265e28b96584cd13fc7a71 Mon Sep 17 00:00:00 2001 From: armfazh Date: Mon, 11 Dec 2023 17:08:32 -0800 Subject: [PATCH 17/18] [BUG]: SHA3 is has an identified bug for 1 byte update. Using the interface Init-Update-Final with hacl produces a wrong hash value, which is equal to calling Init-Final (no Update). Reproducer: $ echo -n "" | openssl dgst -sha3-224 -r $ echo -n "a" | openssl dgst -sha3-224 -r --- crypto/sha3-hacl.c | 47 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/crypto/sha3-hacl.c b/crypto/sha3-hacl.c index 04ad8fd3c9ad0..028f0a885b4f0 100644 --- a/crypto/sha3-hacl.c +++ b/crypto/sha3-hacl.c @@ -124,8 +124,55 @@ static struct shash_alg algs[] = { } }; +static int test_hash(char *hash_alg_name, const unsigned char *data, + unsigned int datalen, unsigned char *digest, + unsigned int digestlen) +{ + struct crypto_shash *alg; + struct shash_desc *sdesc; + char out[300]; + int size; + int ret; + alg = crypto_alloc_shash(hash_alg_name, 0, CRYPTO_ALG_ASYNC); + if (IS_ERR(alg)) { + pr_info("can't alloc alg %s\n", hash_alg_name); + return PTR_ERR(alg); + } + size = sizeof(struct shash_desc) + crypto_shash_descsize(alg); + sdesc = kmalloc(size, GFP_KERNEL); + if (IS_ERR(sdesc)) { + pr_info("can't alloc sdesc\n"); + return PTR_ERR(sdesc); + } + sdesc->tfm = alg; + hacl_sha3_init(sdesc); + hacl_sha3_update(sdesc, data, datalen); + hacl_sha3_final(sdesc, digest); + pr_err("Name: %s\n", hash_alg_name); + memset(out, 0, ARRAY_SIZE(out)); + for (int i = 0; i < digestlen; i++) + snprintf(out, ARRAY_SIZE(out), "%s%02x", out, digest[i]); + pr_err("hacl: %s\n", out); + ret = crypto_shash_digest(sdesc, data, datalen, digest); + memset(out, 0, ARRAY_SIZE(out)); + for (int i = 0; i < digestlen; i++) + snprintf(out, ARRAY_SIZE(out), "%s%02x", out, digest[i]); + pr_err("generic: %s\n", out); + kfree(sdesc); + crypto_free_shash(alg); + return ret; +} + static int __init sha3_hacl_mod_init(void) { + unsigned char data[1]; + unsigned char out[SHA3_512_DIGEST_SIZE]; + data[0] = 'a'; + int datalen = ARRAY_SIZE(data); + test_hash("sha3-224", data, datalen, out, SHA3_224_DIGEST_SIZE); + test_hash("sha3-256", data, datalen, out, SHA3_256_DIGEST_SIZE); + test_hash("sha3-384", data, datalen, out, SHA3_384_DIGEST_SIZE); + test_hash("sha3-512", data, datalen, out, SHA3_512_DIGEST_SIZE); return crypto_register_shashes(algs, ARRAY_SIZE(algs)); } From 1a94da20763bfe14f9299abc041096df60357c7f Mon Sep 17 00:00:00 2001 From: Karthik Bhargavan Date: Fri, 15 Dec 2023 11:33:18 +0100 Subject: [PATCH 18/18] update-finish partial buffer length fixed --- crypto/sha3-hacl.c | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/crypto/sha3-hacl.c b/crypto/sha3-hacl.c index 028f0a885b4f0..29ce2631b82ac 100644 --- a/crypto/sha3-hacl.c +++ b/crypto/sha3-hacl.c @@ -50,11 +50,12 @@ int hacl_sha3_update(struct shash_desc *desc, const u8 *data, unsigned int len) st.block_state.fst = hacl_sha3_alg(sctx->rsiz); st.block_state.snd = sctx->st; st.buf = sctx->buf; - st.total_len = 0; + st.total_len = sctx->partial; uint8_t ret = Hacl_Streaming_Keccak_update(&st, (uint8_t *)data, len); if (ret > 0) { return -1; } else { + sctx->partial = st.total_len ; return 0; } } @@ -67,7 +68,7 @@ int hacl_sha3_final(struct shash_desc *desc, u8 *out) st.block_state.fst = hacl_sha3_alg(sctx->rsiz); st.block_state.snd = sctx->st; st.buf = sctx->buf; - st.total_len = 0; + st.total_len = sctx->partial; uint8_t ret = Hacl_Streaming_Keccak_finish(&st, out); if (ret > 0) { return -1;