gh-99108: Import SHA2-384/512 from HACL* (#101707)

Replace the builtin hashlib implementations of SHA2-384 and SHA2-512
originally from LibTomCrypt with formally verified, side-channel resistant
code from the [HACL*](https://github.com/hacl-star/hacl-star/) project.
The builtins remain a fallback only used when OpenSSL does not provide them.
This commit is contained in:
Jonathan Protzenko 2023-02-14 01:25:16 -08:00 committed by GitHub
parent 8be8101bca
commit e5da9ab2c8
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
16 changed files with 1259 additions and 434 deletions

View file

@ -22,7 +22,7 @@ fi
# Update this when updating to a new version after verifying that the changes
# the update brings in are good.
expected_hacl_star_rev=94aabbb4cf71347d3779a8db486c761403c6d036
expected_hacl_star_rev=4751fc2b11639f651718abf8522fcc36902ca67c
hacl_dir="$(realpath "$1")"
cd "$(dirname "$0")"
@ -54,6 +54,8 @@ include_files=(
declare -a lib_files
lib_files=(
krmllib/dist/minimal/FStar_UInt_8_16_32_64.h
krmllib/dist/minimal/fstar_uint128_struct_endianness.h
krmllib/dist/minimal/FStar_UInt128_Verified.h
)
# C files for the algorithms themselves: current directory
@ -82,10 +84,27 @@ fi
readarray -t all_files < <(find . -name '*.h' -or -name '*.c')
# types.h is a simple wrapper that defines the uint128 type then proceeds to
# include FStar_UInt_8_16_32_64.h; we jump the types.h step since our current
# selection of algorithms does not necessitate the use of uint128
$sed -i 's!#include.*types.h"!#include "krml/FStar_UInt_8_16_32_64.h"!g' "${all_files[@]}"
# types.h originally contains a complex series of if-defs and auxiliary type
# definitions; here, we just need a proper uint128 type in scope
# is a simple wrapper that defines the uint128 type
cat > include/krml/types.h <<EOF
#pragma once
#include <inttypes.h>
typedef struct FStar_UInt128_uint128_s {
uint64_t low;
uint64_t high;
} FStar_UInt128_uint128, uint128_t;
#define KRML_VERIFIED_UINT128
#include "krml/lowstar_endianness.h"
#include "krml/fstar_uint128_struct_endianness.h"
#include "krml/FStar_UInt128_Verified.h"
EOF
# Adjust the include path to reflect the local directory structure
$sed -i 's!#include.*types.h"!#include "krml/types.h"!g' "${all_files[@]}"
$sed -i 's!#include.*compat.h"!!g' "${all_files[@]}"
# FStar_UInt_8_16_32_64 contains definitions useful in the general case, but not
@ -103,22 +122,6 @@ $sed -i 's!#include.*Hacl_Krmllib.h"!!g' "${all_files[@]}"
# included in $dist_files).
$sed -i 's!#include.*internal/Hacl_Streaming_SHA2.h"!#include "Hacl_Streaming_SHA2.h"!g' "${all_files[@]}"
# The SHA2 file contains all variants of SHA2. We strip 384 and 512 for the time
# being, to be included later.
# This regexp matches a separator (two new lines), followed by:
#
# <non-empty-line>*
# ... 384 or 512 ... {
# <indented-line>*
# }
#
# The first non-empty lines are the comment block. The second ... may spill over
# the next following lines if the arguments are printed in one-per-line mode.
$sed -i -z 's/\n\n\([^\n]\+\n\)*[^\n]*\(384\|512\)[^{]*{\n\?\( [^\n]*\n\)*}//g' Hacl_Streaming_SHA2.c
# Same thing with function prototypes
$sed -i -z 's/\n\n\([^\n]\+\n\)*[^\n]*\(384\|512\)[^;]*;//g' Hacl_Streaming_SHA2.h
# Use globally unique names for the Hacl_ C APIs to avoid linkage conflicts.
$sed -i -z 's!#include <string.h>\n!#include <string.h>\n#include "python_hacl_namespaces.h"\n!' Hacl_Streaming_SHA2.h