gh-99108: Replace SHA3 implementation HACL* version (#103597)

Replaces our built-in SHA3 implementation with a verified one from the HACL* project.

This implementation is used when OpenSSL does not provide SHA3 or is not present.

3.11 shiped with a very slow tiny sha3 implementation to get off of the <=3.10 reference implementation that wound up having serious bugs. This brings us back to a reasonably performing built-in implementation consistent with what we've just replaced our other guaranteed available standard hash algorithms with: code from the HACL* project.

---------

Co-authored-by: Gregory P. Smith <greg@krypto.org>
This commit is contained in:
Jonathan Protzenko 2023-05-07 20:50:04 -07:00 committed by GitHub
parent 01cc9c1ff7
commit 15665d896b
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
21 changed files with 1204 additions and 434 deletions

View file

@ -19,6 +19,28 @@
# define inline __inline__
#endif
/******************************************************************************/
/* Macros that KaRaMeL will generate. */
/******************************************************************************/
/* For "bare" targets that do not have a C stdlib, the user might want to use
* [-add-early-include '"mydefinitions.h"'] and override these. */
#ifndef KRML_HOST_PRINTF
# define KRML_HOST_PRINTF printf
#endif
#if ( \
(defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) && \
(!(defined KRML_HOST_EPRINTF)))
# define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
#elif !(defined KRML_HOST_EPRINTF) && defined(_MSC_VER)
# define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
#endif
#ifndef KRML_HOST_EXIT
# define KRML_HOST_EXIT exit
#endif
#ifndef KRML_HOST_MALLOC
# define KRML_HOST_MALLOC malloc
#endif
@ -35,6 +57,28 @@
# define KRML_HOST_IGNORE(x) (void)(x)
#endif
/* In FStar.Buffer.fst, the size of arrays is uint32_t, but it's a number of
* *elements*. Do an ugly, run-time check (some of which KaRaMeL can eliminate).
*/
#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ > 4))
# define _KRML_CHECK_SIZE_PRAGMA \
_Pragma("GCC diagnostic ignored \"-Wtype-limits\"")
#else
# define _KRML_CHECK_SIZE_PRAGMA
#endif
#define KRML_CHECK_SIZE(size_elt, sz) \
do { \
_KRML_CHECK_SIZE_PRAGMA \
if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) { \
KRML_HOST_PRINTF( \
"Maximum allocatable size exceeded, aborting before overflow at " \
"%s:%d\n", \
__FILE__, __LINE__); \
KRML_HOST_EXIT(253); \
} \
} while (0)
/* Macros for prettier unrolling of loops */
#define KRML_LOOP1(i, n, x) { \
x \

View file

@ -77,7 +77,7 @@
# define le64toh(x) (x)
/* ... for Windows (GCC-like, e.g. mingw or clang) */
#elif (defined(_WIN32) || defined(_WIN64)) && \
#elif (defined(_WIN32) || defined(_WIN64) || defined(__EMSCRIPTEN__)) && \
(defined(__GNUC__) || defined(__clang__))
# define htobe16(x) __builtin_bswap16(x)
@ -96,7 +96,8 @@
# define le64toh(x) (x)
/* ... generic big-endian fallback code */
#elif defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
/* ... AIX doesn't have __BYTE_ORDER__ (with XLC compiler) & is always big-endian */
#elif (defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__) || defined(_AIX)
/* byte swapping code inspired by:
* https://github.com/rweather/arduinolibs/blob/master/libraries/Crypto/utility/EndianUtil.h