diff --git a/Lib/test/test_hashlib.py b/Lib/test/test_hashlib.py index 450dc4933f4..9c92b4e9c28 100644 --- a/Lib/test/test_hashlib.py +++ b/Lib/test/test_hashlib.py @@ -22,6 +22,7 @@ from test import support from test.support import _4G, bigmemtest from test.support.import_helper import import_fresh_module from test.support import os_helper +from test.support import requires_resource from test.support import threading_helper from test.support import warnings_helper from http.client import HTTPException @@ -354,6 +355,15 @@ class HashLibTestCase(unittest.TestCase): self.assertEqual(m1.digest(*args), m4_copy.digest(*args)) self.assertEqual(m4.digest(*args), m4_digest) + @requires_resource('cpu') + def test_sha256_update_over_4gb(self): + zero_1mb = b"\0" * 1024 * 1024 + h = hashlib.sha256() + for i in range(0, 4096): + h.update(zero_1mb) + h.update(b"hello world") + self.assertEqual(h.hexdigest(), "a5364f7a52ebe2e25f1838a4ca715a893b6fd7a23f2a0d9e9762120da8b1bf53") + def check(self, name, data, hexdigest, shake=False, **kwargs): length = len(hexdigest)//2 hexdigest = hexdigest.lower() diff --git a/Makefile.pre.in b/Makefile.pre.in index f2f9371e8ac..3641c4eeebe 100644 --- a/Makefile.pre.in +++ b/Makefile.pre.in @@ -2612,7 +2612,7 @@ MODULE__HASHLIB_DEPS=$(srcdir)/Modules/hashlib.h MODULE__IO_DEPS=$(srcdir)/Modules/_io/_iomodule.h MODULE__MD5_DEPS=$(srcdir)/Modules/hashlib.h MODULE__SHA1_DEPS=$(srcdir)/Modules/hashlib.h -MODULE__SHA256_DEPS=$(srcdir)/Modules/hashlib.h +MODULE__SHA256_DEPS=$(srcdir)/Modules/hashlib.h $(srcdir)/Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h $(srcdir)/Modules/_hacl/include/krml/lowstar_endianness.h $(srcdir)/Modules/_hacl/include/krml/internal/target.h $(srcdir)/Modules/_hacl/Hacl_Streaming_SHA2.h MODULE__SHA3_DEPS=$(srcdir)/Modules/_sha3/sha3.c $(srcdir)/Modules/_sha3/sha3.h $(srcdir)/Modules/hashlib.h MODULE__SHA512_DEPS=$(srcdir)/Modules/hashlib.h MODULE__SOCKET_DEPS=$(srcdir)/Modules/socketmodule.h $(srcdir)/Modules/addrinfo.h $(srcdir)/Modules/getaddrinfo.c $(srcdir)/Modules/getnameinfo.c diff --git a/Misc/NEWS.d/next/Security/2022-11-08-12-06-52.gh-issue-99108.4Wrsuh.rst b/Misc/NEWS.d/next/Security/2022-11-08-12-06-52.gh-issue-99108.4Wrsuh.rst new file mode 100644 index 00000000000..64acc09c482 --- /dev/null +++ b/Misc/NEWS.d/next/Security/2022-11-08-12-06-52.gh-issue-99108.4Wrsuh.rst @@ -0,0 +1,4 @@ +Replace the builtin :mod:`hashlib` implementations of SHA2-224 and SHA2-256 +originally from LibTomCrypt with formally verified, side-channel resistant +code from the `HACL* `_ project. The +builtins remain a fallback only used when OpenSSL does not provide them. diff --git a/Modules/Setup.stdlib.in b/Modules/Setup.stdlib.in index 3fd591c70d4..f72783810f9 100644 --- a/Modules/Setup.stdlib.in +++ b/Modules/Setup.stdlib.in @@ -79,7 +79,7 @@ # hashing builtins, can be disabled with --without-builtin-hashlib-hashes @MODULE__MD5_TRUE@_md5 md5module.c @MODULE__SHA1_TRUE@_sha1 sha1module.c -@MODULE__SHA256_TRUE@_sha256 sha256module.c +@MODULE__SHA256_TRUE@_sha256 sha256module.c _hacl/Hacl_Streaming_SHA2.c @MODULE__SHA512_TRUE@_sha512 sha512module.c @MODULE__SHA3_TRUE@_sha3 _sha3/sha3module.c @MODULE__BLAKE2_TRUE@_blake2 _blake2/blake2module.c _blake2/blake2b_impl.c _blake2/blake2s_impl.c diff --git a/Modules/_hacl/Hacl_Streaming_SHA2.c b/Modules/_hacl/Hacl_Streaming_SHA2.c new file mode 100644 index 00000000000..84566571792 --- /dev/null +++ b/Modules/_hacl/Hacl_Streaming_SHA2.c @@ -0,0 +1,682 @@ +/* MIT License + * + * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation + * Copyright (c) 2022-2023 HACL* Contributors + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + */ + + +#include "Hacl_Streaming_SHA2.h" + +#include "internal/Hacl_SHA2_Generic.h" + + +static inline void 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_update0(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;); +} + +static inline void 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_update0(mb, st); + } +} + +static inline void +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_update0(last0, hash); + if (blocks > (uint32_t)1U) + { + sha256_update0(last1, hash); + return; + } +} + +static inline void 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)); +} + +static inline void 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) +{ + sha256_update_nblocks(len, b, st); +} + +static void sha224_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *st) +{ + sha256_update_last(totlen, len, b, st); +} + +static inline void 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)); +} + +/** +Allocate initial state for the SHA2_256 hash. The state is to be freed by +calling `free_256`. +*/ +Hacl_Streaming_SHA2_state_sha2_224 *Hacl_Streaming_SHA2_create_in_256(void) +{ + uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t)); + uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t)); + Hacl_Streaming_SHA2_state_sha2_224 + s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; + Hacl_Streaming_SHA2_state_sha2_224 + *p = + (Hacl_Streaming_SHA2_state_sha2_224 *)KRML_HOST_MALLOC(sizeof ( + Hacl_Streaming_SHA2_state_sha2_224 + )); + p[0U] = s; + sha256_init(block_state); + return p; +} + +/** +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_SHA2_state_sha2_224 +*Hacl_Streaming_SHA2_copy_256(Hacl_Streaming_SHA2_state_sha2_224 *s0) +{ + Hacl_Streaming_SHA2_state_sha2_224 scrut = *s0; + uint32_t *block_state0 = scrut.block_state; + uint8_t *buf0 = scrut.buf; + uint64_t total_len0 = scrut.total_len; + uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t)); + memcpy(buf, buf0, (uint32_t)64U * sizeof (uint8_t)); + uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t)); + memcpy(block_state, block_state0, (uint32_t)8U * sizeof (uint32_t)); + Hacl_Streaming_SHA2_state_sha2_224 + s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; + Hacl_Streaming_SHA2_state_sha2_224 + *p = + (Hacl_Streaming_SHA2_state_sha2_224 *)KRML_HOST_MALLOC(sizeof ( + Hacl_Streaming_SHA2_state_sha2_224 + )); + p[0U] = s; + return p; +} + +/** +Reset an existing state to the initial hash state with empty data. +*/ +void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_SHA2_state_sha2_224 *s) +{ + Hacl_Streaming_SHA2_state_sha2_224 scrut = *s; + uint8_t *buf = scrut.buf; + uint32_t *block_state = scrut.block_state; + sha256_init(block_state); + Hacl_Streaming_SHA2_state_sha2_224 + tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; + s[0U] = tmp; +} + +static inline uint32_t +update_224_256(Hacl_Streaming_SHA2_state_sha2_224 *p, uint8_t *data, uint32_t len) +{ + Hacl_Streaming_SHA2_state_sha2_224 s = *p; + uint64_t total_len = s.total_len; + if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len) + { + return (uint32_t)1U; + } + 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_SHA2_state_sha2_224 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_SHA2_state_sha2_224){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len2 + } + ); + } + else if (sz == (uint32_t)0U) + { + Hacl_Streaming_SHA2_state_sha2_224 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)) + { + 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; + sha256_update_nblocks(data1_len, data1, block_state1); + uint8_t *dst = buf; + memcpy(dst, data2, data2_len * sizeof (uint8_t)); + *p + = + ( + (Hacl_Streaming_SHA2_state_sha2_224){ + .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_SHA2_state_sha2_224 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_SHA2_state_sha2_224){ + .block_state = block_state10, + .buf = buf0, + .total_len = total_len2 + } + ); + Hacl_Streaming_SHA2_state_sha2_224 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)) + { + 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; + sha256_update_nblocks(data1_len, data11, block_state1); + uint8_t *dst = buf; + memcpy(dst, data21, data2_len * sizeof (uint8_t)); + *p + = + ( + (Hacl_Streaming_SHA2_state_sha2_224){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)(len - diff) + } + ); + } + return (uint32_t)0U; +} + +/** +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. +*/ +uint32_t +Hacl_Streaming_SHA2_update_256( + Hacl_Streaming_SHA2_state_sha2_224 *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_SHA2_state_sha2_224 *p, uint8_t *dst) +{ + Hacl_Streaming_SHA2_state_sha2_224 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; + sha256_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state); + uint64_t prev_len_last = total_len - (uint64_t)r; + sha256_update_last(prev_len_last + (uint64_t)r, r, buf_last, tmp_block_state); + sha256_finish(tmp_block_state, 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_SHA2_state_sha2_224 *s) +{ + Hacl_Streaming_SHA2_state_sha2_224 scrut = *s; + uint8_t *buf = scrut.buf; + uint32_t *block_state = scrut.block_state; + KRML_HOST_FREE(block_state); + KRML_HOST_FREE(buf); + KRML_HOST_FREE(s); +} + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. +*/ +void Hacl_Streaming_SHA2_sha256(uint8_t *input, uint32_t input_len, uint8_t *dst) +{ + uint8_t *ib = input; + uint8_t *rb = dst; + uint32_t st[8U] = { 0U }; + sha256_init(st); + uint32_t rem = input_len % (uint32_t)64U; + uint64_t len_ = (uint64_t)input_len; + 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; + sha256_update_last(len_, rem, lb, st); + sha256_finish(st, rb); +} + +Hacl_Streaming_SHA2_state_sha2_224 *Hacl_Streaming_SHA2_create_in_224(void) +{ + uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t)); + uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t)); + Hacl_Streaming_SHA2_state_sha2_224 + s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; + Hacl_Streaming_SHA2_state_sha2_224 + *p = + (Hacl_Streaming_SHA2_state_sha2_224 *)KRML_HOST_MALLOC(sizeof ( + Hacl_Streaming_SHA2_state_sha2_224 + )); + p[0U] = s; + sha224_init(block_state); + return p; +} + +void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_SHA2_state_sha2_224 *s) +{ + Hacl_Streaming_SHA2_state_sha2_224 scrut = *s; + uint8_t *buf = scrut.buf; + uint32_t *block_state = scrut.block_state; + sha224_init(block_state); + Hacl_Streaming_SHA2_state_sha2_224 + tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; + s[0U] = tmp; +} + +uint32_t +Hacl_Streaming_SHA2_update_224( + Hacl_Streaming_SHA2_state_sha2_224 *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_SHA2_state_sha2_224 *p, uint8_t *dst) +{ + Hacl_Streaming_SHA2_state_sha2_224 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; + sha224_update_last(prev_len_last + (uint64_t)r, r, buf_last, tmp_block_state); + sha224_finish(tmp_block_state, dst); +} + +void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_SHA2_state_sha2_224 *p) +{ + Hacl_Streaming_SHA2_free_256(p); +} + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. +*/ +void Hacl_Streaming_SHA2_sha224(uint8_t *input, uint32_t input_len, uint8_t *dst) +{ + uint8_t *ib = input; + uint8_t *rb = dst; + uint32_t st[8U] = { 0U }; + 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; + sha224_update_last(len_, rem, lb, st); + sha224_finish(st, rb); +} + diff --git a/Modules/_hacl/Hacl_Streaming_SHA2.h b/Modules/_hacl/Hacl_Streaming_SHA2.h new file mode 100644 index 00000000000..c83a835afe7 --- /dev/null +++ b/Modules/_hacl/Hacl_Streaming_SHA2.h @@ -0,0 +1,136 @@ +/* MIT License + * + * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation + * Copyright (c) 2022-2023 HACL* Contributors + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + */ + + +#ifndef __Hacl_Streaming_SHA2_H +#define __Hacl_Streaming_SHA2_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include +#include "python_hacl_namespaces.h" +#include "krml/FStar_UInt_8_16_32_64.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + + + + +typedef struct Hacl_Streaming_SHA2_state_sha2_224_s +{ + uint32_t *block_state; + uint8_t *buf; + uint64_t total_len; +} +Hacl_Streaming_SHA2_state_sha2_224; + +typedef Hacl_Streaming_SHA2_state_sha2_224 Hacl_Streaming_SHA2_state_sha2_256; + +/** +Allocate initial state for the SHA2_256 hash. The state is to be freed by +calling `free_256`. +*/ +Hacl_Streaming_SHA2_state_sha2_224 *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_SHA2_state_sha2_224 +*Hacl_Streaming_SHA2_copy_256(Hacl_Streaming_SHA2_state_sha2_224 *s0); + +/** +Reset an existing state to the initial hash state with empty data. +*/ +void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_SHA2_state_sha2_224 *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. +*/ +uint32_t +Hacl_Streaming_SHA2_update_256( + Hacl_Streaming_SHA2_state_sha2_224 *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_SHA2_state_sha2_224 *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_SHA2_state_sha2_224 *s); + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. +*/ +void Hacl_Streaming_SHA2_sha256(uint8_t *input, uint32_t input_len, uint8_t *dst); + +Hacl_Streaming_SHA2_state_sha2_224 *Hacl_Streaming_SHA2_create_in_224(void); + +void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_SHA2_state_sha2_224 *s); + +uint32_t +Hacl_Streaming_SHA2_update_224( + Hacl_Streaming_SHA2_state_sha2_224 *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_SHA2_state_sha2_224 *p, uint8_t *dst); + +void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_SHA2_state_sha2_224 *p); + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. +*/ +void Hacl_Streaming_SHA2_sha224(uint8_t *input, uint32_t input_len, uint8_t *dst); + +#if defined(__cplusplus) +} +#endif + +#define __Hacl_Streaming_SHA2_H_DEFINED +#endif diff --git a/Modules/_hacl/README.md b/Modules/_hacl/README.md new file mode 100644 index 00000000000..e6a156a54b3 --- /dev/null +++ b/Modules/_hacl/README.md @@ -0,0 +1,29 @@ +# Algorithm implementations used by the `hashlib` module. + +This code comes from the +[HACL\*](https://github.com/hacl-star/hacl-star/) project. + +HACL\* is a cryptographic library that has been formally verified for memory +safety, functional correctness, and secret independence. + +## Updating HACL* + +Use the `refresh.sh` script in this directory to pull in a new upstream code +version. The upstream git hash used for the most recent code pull is recorded +in the script. Modify the script as needed to bring in more if changes are +needed based on upstream code refactoring. + +Never manually edit HACL\* files. Always add transformation shell code to the +`refresh.sh` script to perform any necessary edits. If there are serious code +changes needed, work with the upstream repository. + +## Local files + +1. `./include/python_hacl_namespaces.h` +1. `./README.md` +1. `./refresh.sh` + +## ACKS + +* Jonathan Protzenko aka [@msprotz on Github](https://github.com/msprotz) +contributed our HACL\* based builtin code. diff --git a/Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h b/Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h new file mode 100644 index 00000000000..3e2e4b32b22 --- /dev/null +++ b/Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h @@ -0,0 +1,109 @@ +/* + Copyright (c) INRIA and Microsoft Corporation. All rights reserved. + Licensed under the Apache 2.0 License. +*/ + + +#ifndef __FStar_UInt_8_16_32_64_H +#define __FStar_UInt_8_16_32_64_H + + + + +#include +#include + +#include "krml/lowstar_endianness.h" +#include "krml/FStar_UInt_8_16_32_64.h" +#include "krml/internal/target.h" +static inline uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b) +{ + uint64_t x = a ^ b; + uint64_t minus_x = ~x + (uint64_t)1U; + uint64_t x_or_minus_x = x | minus_x; + uint64_t xnx = x_or_minus_x >> (uint32_t)63U; + return xnx - (uint64_t)1U; +} + +static inline uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b) +{ + uint64_t x = a; + uint64_t y = b; + uint64_t x_xor_y = x ^ y; + uint64_t x_sub_y = x - y; + uint64_t x_sub_y_xor_y = x_sub_y ^ y; + uint64_t q = x_xor_y | x_sub_y_xor_y; + uint64_t x_xor_q = x ^ q; + uint64_t x_xor_q_ = x_xor_q >> (uint32_t)63U; + return x_xor_q_ - (uint64_t)1U; +} + +static inline uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b) +{ + uint32_t x = a ^ b; + uint32_t minus_x = ~x + (uint32_t)1U; + uint32_t x_or_minus_x = x | minus_x; + uint32_t xnx = x_or_minus_x >> (uint32_t)31U; + return xnx - (uint32_t)1U; +} + +static inline uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b) +{ + uint32_t x = a; + uint32_t y = b; + uint32_t x_xor_y = x ^ y; + uint32_t x_sub_y = x - y; + uint32_t x_sub_y_xor_y = x_sub_y ^ y; + uint32_t q = x_xor_y | x_sub_y_xor_y; + uint32_t x_xor_q = x ^ q; + uint32_t x_xor_q_ = x_xor_q >> (uint32_t)31U; + return x_xor_q_ - (uint32_t)1U; +} + +static inline uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b) +{ + uint16_t x = a ^ b; + uint16_t minus_x = ~x + (uint16_t)1U; + uint16_t x_or_minus_x = x | minus_x; + uint16_t xnx = x_or_minus_x >> (uint32_t)15U; + return xnx - (uint16_t)1U; +} + +static inline uint16_t FStar_UInt16_gte_mask(uint16_t a, uint16_t b) +{ + uint16_t x = a; + uint16_t y = b; + uint16_t x_xor_y = x ^ y; + uint16_t x_sub_y = x - y; + uint16_t x_sub_y_xor_y = x_sub_y ^ y; + uint16_t q = x_xor_y | x_sub_y_xor_y; + uint16_t x_xor_q = x ^ q; + uint16_t x_xor_q_ = x_xor_q >> (uint32_t)15U; + return x_xor_q_ - (uint16_t)1U; +} + +static inline uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b) +{ + uint8_t x = a ^ b; + uint8_t minus_x = ~x + (uint8_t)1U; + uint8_t x_or_minus_x = x | minus_x; + uint8_t xnx = x_or_minus_x >> (uint32_t)7U; + return xnx - (uint8_t)1U; +} + +static inline uint8_t FStar_UInt8_gte_mask(uint8_t a, uint8_t b) +{ + uint8_t x = a; + uint8_t y = b; + uint8_t x_xor_y = x ^ y; + uint8_t x_sub_y = x - y; + uint8_t x_sub_y_xor_y = x_sub_y ^ y; + uint8_t q = x_xor_y | x_sub_y_xor_y; + uint8_t x_xor_q = x ^ q; + uint8_t x_xor_q_ = x_xor_q >> (uint32_t)7U; + return x_xor_q_ - (uint8_t)1U; +} + + +#define __FStar_UInt_8_16_32_64_H_DEFINED +#endif diff --git a/Modules/_hacl/include/krml/internal/target.h b/Modules/_hacl/include/krml/internal/target.h new file mode 100644 index 00000000000..9ef59859a55 --- /dev/null +++ b/Modules/_hacl/include/krml/internal/target.h @@ -0,0 +1,218 @@ +/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. + Licensed under the Apache 2.0 License. */ + +#ifndef __KRML_TARGET_H +#define __KRML_TARGET_H + +#include +#include +#include +#include +#include +#include +#include + +/* Since KaRaMeL emits the inline keyword unconditionally, we follow the + * guidelines at https://gcc.gnu.org/onlinedocs/gcc/Inline.html and make this + * __inline__ to ensure the code compiles with -std=c90 and earlier. */ +#ifdef __GNUC__ +# define inline __inline__ +#endif + +#ifndef KRML_HOST_MALLOC +# define KRML_HOST_MALLOC malloc +#endif + +#ifndef KRML_HOST_CALLOC +# define KRML_HOST_CALLOC calloc +#endif + +#ifndef KRML_HOST_FREE +# define KRML_HOST_FREE free +#endif + +/* 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) + +#ifndef KRML_UNROLL_MAX +#define KRML_UNROLL_MAX 16 +#endif + +/* 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 diff --git a/Modules/_hacl/include/krml/lowstar_endianness.h b/Modules/_hacl/include/krml/lowstar_endianness.h new file mode 100644 index 00000000000..32a7391e817 --- /dev/null +++ b/Modules/_hacl/include/krml/lowstar_endianness.h @@ -0,0 +1,230 @@ +/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. + Licensed under the Apache 2.0 License. */ + +#ifndef __LOWSTAR_ENDIANNESS_H +#define __LOWSTAR_ENDIANNESS_H + +#include +#include + +/******************************************************************************/ +/* Implementing C.fst (part 2: endian-ness macros) */ +/******************************************************************************/ + +/* ... for Linux */ +#if defined(__linux__) || defined(__CYGWIN__) || defined (__USE_SYSTEM_ENDIAN_H__) || defined(__GLIBC__) +# include + +/* ... for OSX */ +#elif defined(__APPLE__) +# include +# define htole64(x) OSSwapHostToLittleInt64(x) +# define le64toh(x) OSSwapLittleToHostInt64(x) +# define htobe64(x) OSSwapHostToBigInt64(x) +# define be64toh(x) OSSwapBigToHostInt64(x) + +# define htole16(x) OSSwapHostToLittleInt16(x) +# define le16toh(x) OSSwapLittleToHostInt16(x) +# define htobe16(x) OSSwapHostToBigInt16(x) +# define be16toh(x) OSSwapBigToHostInt16(x) + +# define htole32(x) OSSwapHostToLittleInt32(x) +# define le32toh(x) OSSwapLittleToHostInt32(x) +# define htobe32(x) OSSwapHostToBigInt32(x) +# define be32toh(x) OSSwapBigToHostInt32(x) + +/* ... for Solaris */ +#elif defined(__sun__) +# include +# define htole64(x) LE_64(x) +# define le64toh(x) LE_64(x) +# define htobe64(x) BE_64(x) +# define be64toh(x) BE_64(x) + +# define htole16(x) LE_16(x) +# define le16toh(x) LE_16(x) +# define htobe16(x) BE_16(x) +# define be16toh(x) BE_16(x) + +# define htole32(x) LE_32(x) +# define le32toh(x) LE_32(x) +# define htobe32(x) BE_32(x) +# define be32toh(x) BE_32(x) + +/* ... for the BSDs */ +#elif defined(__FreeBSD__) || defined(__NetBSD__) || defined(__DragonFly__) +# include +#elif defined(__OpenBSD__) +# include + +/* ... for Windows (MSVC)... not targeting XBOX 360! */ +#elif defined(_MSC_VER) + +# include +# define htobe16(x) _byteswap_ushort(x) +# define htole16(x) (x) +# define be16toh(x) _byteswap_ushort(x) +# define le16toh(x) (x) + +# define htobe32(x) _byteswap_ulong(x) +# define htole32(x) (x) +# define be32toh(x) _byteswap_ulong(x) +# define le32toh(x) (x) + +# define htobe64(x) _byteswap_uint64(x) +# define htole64(x) (x) +# define be64toh(x) _byteswap_uint64(x) +# define le64toh(x) (x) + +/* ... for Windows (GCC-like, e.g. mingw or clang) */ +#elif (defined(_WIN32) || defined(_WIN64)) && \ + (defined(__GNUC__) || defined(__clang__)) + +# define htobe16(x) __builtin_bswap16(x) +# define htole16(x) (x) +# define be16toh(x) __builtin_bswap16(x) +# define le16toh(x) (x) + +# define htobe32(x) __builtin_bswap32(x) +# define htole32(x) (x) +# define be32toh(x) __builtin_bswap32(x) +# define le32toh(x) (x) + +# define htobe64(x) __builtin_bswap64(x) +# define htole64(x) (x) +# define be64toh(x) __builtin_bswap64(x) +# define le64toh(x) (x) + +/* ... generic big-endian fallback code */ +#elif defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__ + +/* byte swapping code inspired by: + * https://github.com/rweather/arduinolibs/blob/master/libraries/Crypto/utility/EndianUtil.h + * */ + +# define htobe32(x) (x) +# define be32toh(x) (x) +# define htole32(x) \ + (__extension__({ \ + uint32_t _temp = (x); \ + ((_temp >> 24) & 0x000000FF) | ((_temp >> 8) & 0x0000FF00) | \ + ((_temp << 8) & 0x00FF0000) | ((_temp << 24) & 0xFF000000); \ + })) +# define le32toh(x) (htole32((x))) + +# define htobe64(x) (x) +# define be64toh(x) (x) +# define htole64(x) \ + (__extension__({ \ + uint64_t __temp = (x); \ + uint32_t __low = htobe32((uint32_t)__temp); \ + uint32_t __high = htobe32((uint32_t)(__temp >> 32)); \ + (((uint64_t)__low) << 32) | __high; \ + })) +# define le64toh(x) (htole64((x))) + +/* ... generic little-endian fallback code */ +#elif defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__ + +# define htole32(x) (x) +# define le32toh(x) (x) +# define htobe32(x) \ + (__extension__({ \ + uint32_t _temp = (x); \ + ((_temp >> 24) & 0x000000FF) | ((_temp >> 8) & 0x0000FF00) | \ + ((_temp << 8) & 0x00FF0000) | ((_temp << 24) & 0xFF000000); \ + })) +# define be32toh(x) (htobe32((x))) + +# define htole64(x) (x) +# define le64toh(x) (x) +# define htobe64(x) \ + (__extension__({ \ + uint64_t __temp = (x); \ + uint32_t __low = htobe32((uint32_t)__temp); \ + uint32_t __high = htobe32((uint32_t)(__temp >> 32)); \ + (((uint64_t)__low) << 32) | __high; \ + })) +# define be64toh(x) (htobe64((x))) + +/* ... couldn't determine endian-ness of the target platform */ +#else +# error "Please define __BYTE_ORDER__!" + +#endif /* defined(__linux__) || ... */ + +/* Loads and stores. These avoid undefined behavior due to unaligned memory + * accesses, via memcpy. */ + +inline static uint16_t load16(uint8_t *b) { + uint16_t x; + memcpy(&x, b, 2); + return x; +} + +inline static uint32_t load32(uint8_t *b) { + uint32_t x; + memcpy(&x, b, 4); + return x; +} + +inline static uint64_t load64(uint8_t *b) { + uint64_t x; + memcpy(&x, b, 8); + return x; +} + +inline static void store16(uint8_t *b, uint16_t i) { + memcpy(b, &i, 2); +} + +inline static void store32(uint8_t *b, uint32_t i) { + memcpy(b, &i, 4); +} + +inline static void store64(uint8_t *b, uint64_t i) { + memcpy(b, &i, 8); +} + +/* Legacy accessors so that this header can serve as an implementation of + * C.Endianness */ +#define load16_le(b) (le16toh(load16(b))) +#define store16_le(b, i) (store16(b, htole16(i))) +#define load16_be(b) (be16toh(load16(b))) +#define store16_be(b, i) (store16(b, htobe16(i))) + +#define load32_le(b) (le32toh(load32(b))) +#define store32_le(b, i) (store32(b, htole32(i))) +#define load32_be(b) (be32toh(load32(b))) +#define store32_be(b, i) (store32(b, htobe32(i))) + +#define load64_le(b) (le64toh(load64(b))) +#define store64_le(b, i) (store64(b, htole64(i))) +#define load64_be(b) (be64toh(load64(b))) +#define store64_be(b, i) (store64(b, htobe64(i))) + +/* Co-existence of LowStar.Endianness and FStar.Endianness generates name + * conflicts, because of course both insist on having no prefixes. Until a + * prefix is added, or until we truly retire FStar.Endianness, solve this issue + * in an elegant way. */ +#define load16_le0 load16_le +#define store16_le0 store16_le +#define load16_be0 load16_be +#define store16_be0 store16_be + +#define load32_le0 load32_le +#define store32_le0 store32_le +#define load32_be0 load32_be +#define store32_be0 store32_be + +#define load64_le0 load64_le +#define store64_le0 store64_le +#define load64_be0 load64_be +#define store64_be0 store64_be + +#define load128_le0 load128_le +#define store128_le0 store128_le +#define load128_be0 load128_be +#define store128_be0 store128_be + +#endif diff --git a/Modules/_hacl/include/python_hacl_namespaces.h b/Modules/_hacl/include/python_hacl_namespaces.h new file mode 100644 index 00000000000..af390459311 --- /dev/null +++ b/Modules/_hacl/include/python_hacl_namespaces.h @@ -0,0 +1,28 @@ +#ifndef _PYTHON_HACL_NAMESPACES_H +#define _PYTHON_HACL_NAMESPACES_H + +/* + * C's excuse for namespaces: Use globally unique names to avoid linkage + * conflicts with builds linking or dynamically loading other code potentially + * using HACL* libraries. + */ + +#define Hacl_Streaming_SHA2_state_sha2_224_s python_hashlib_Hacl_Streaming_SHA2_state_sha2_224_s +#define Hacl_Streaming_SHA2_state_sha2_224 python_hashlib_Hacl_Streaming_SHA2_state_sha2_224 +#define Hacl_Streaming_SHA2_state_sha2_256 python_hashlib_Hacl_Streaming_SHA2_state_sha2_256 +#define Hacl_Streaming_SHA2_create_in_256 python_hashlib_Hacl_Streaming_SHA2_create_in_256 +#define Hacl_Streaming_SHA2_create_in_224 python_hashlib_Hacl_Streaming_SHA2_create_in_224 +#define Hacl_Streaming_SHA2_copy_256 python_hashlib_Hacl_Streaming_SHA2_copy_256 +#define Hacl_Streaming_SHA2_copy_224 python_hashlib_Hacl_Streaming_SHA2_copy_224 +#define Hacl_Streaming_SHA2_init_256 python_hashlib_Hacl_Streaming_SHA2_init_256 +#define Hacl_Streaming_SHA2_init_224 python_hashlib_Hacl_Streaming_SHA2_init_224 +#define Hacl_Streaming_SHA2_update_256 python_hashlib_Hacl_Streaming_SHA2_update_256 +#define Hacl_Streaming_SHA2_update_224 python_hashlib_Hacl_Streaming_SHA2_update_224 +#define Hacl_Streaming_SHA2_finish_256 python_hashlib_Hacl_Streaming_SHA2_finish_256 +#define Hacl_Streaming_SHA2_finish_224 python_hashlib_Hacl_Streaming_SHA2_finish_224 +#define Hacl_Streaming_SHA2_free_256 python_hashlib_Hacl_Streaming_SHA2_free_256 +#define Hacl_Streaming_SHA2_free_224 python_hashlib_Hacl_Streaming_SHA2_free_224 +#define Hacl_Streaming_SHA2_sha256 python_hashlib_Hacl_Streaming_SHA2_sha256 +#define Hacl_Streaming_SHA2_sha224 python_hashlib_Hacl_Streaming_SHA2_sha224 + +#endif // _PYTHON_HACL_NAMESPACES_H diff --git a/Modules/_hacl/internal/Hacl_SHA2_Generic.h b/Modules/_hacl/internal/Hacl_SHA2_Generic.h new file mode 100644 index 00000000000..23f7cea1eb3 --- /dev/null +++ b/Modules/_hacl/internal/Hacl_SHA2_Generic.h @@ -0,0 +1,135 @@ +/* MIT License + * + * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation + * Copyright (c) 2022-2023 HACL* Contributors + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + */ + + +#ifndef __internal_Hacl_SHA2_Generic_H +#define __internal_Hacl_SHA2_Generic_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include +#include "krml/FStar_UInt_8_16_32_64.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + + + + +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 + }; + +#if defined(__cplusplus) +} +#endif + +#define __internal_Hacl_SHA2_Generic_H_DEFINED +#endif diff --git a/Modules/_hacl/refresh.sh b/Modules/_hacl/refresh.sh new file mode 100755 index 00000000000..594873862a2 --- /dev/null +++ b/Modules/_hacl/refresh.sh @@ -0,0 +1,132 @@ +#!/usr/bin/env bash +# +# Use this script to update the HACL generated hash algorithm implementation +# code from a local checkout of the upstream hacl-star repository. +# + +set -e +set -o pipefail + +if [[ "${BASH_VERSINFO[0]}" -lt 4 ]]; then + echo "A bash version >= 4 required. Got: $BASH_VERSION" >&2 + exit 1 +fi + +if [[ $1 == "" ]]; then + echo "Usage: $0 path-to-hacl-directory" + echo "" + echo " path-to-hacl-directory should be a local git checkout of a" + echo " https://github.com/hacl-star/hacl-star/ repo." + exit 1 +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 + +hacl_dir="$(realpath "$1")" +cd "$(dirname "$0")" +actual_rev=$(cd "$hacl_dir" && git rev-parse HEAD) + +if [[ "$actual_rev" != "$expected_hacl_star_rev" ]]; then + echo "WARNING: HACL* in '$hacl_dir' is at revision:" >&2 + echo " $actual_rev" >&2 + echo "but expected revision:" >&2 + echo " $expected_hacl_star_rev" >&2 + echo "Edit the expected rev if the changes pulled in are what you want." +fi + +# Step 1: copy files + +declare -a dist_files +dist_files=( + Hacl_Streaming_SHA2.h + internal/Hacl_SHA2_Generic.h + Hacl_Streaming_SHA2.c +) + +declare -a include_files +include_files=( + include/krml/lowstar_endianness.h + include/krml/internal/target.h +) + +declare -a lib_files +lib_files=( + krmllib/dist/minimal/FStar_UInt_8_16_32_64.h +) + +# C files for the algorithms themselves: current directory +(cd "$hacl_dir/dist/gcc-compatible" && tar cf - "${dist_files[@]}") | tar xf - + +# Support header files (e.g. endianness macros): stays in include/ +(cd "$hacl_dir/dist/karamel" && tar cf - "${include_files[@]}") | tar xf - + +# Special treatment: we don't bother with an extra directory and move krmllib +# files to the same include directory +for f in "${lib_files[@]}"; do + cp "$hacl_dir/dist/karamel/$f" include/krml/ +done + +# Step 2: some in-place modifications to keep things simple and minimal + +# This is basic, but refreshes of the vendored HACL code are infrequent, so +# let's not over-engineer this. +if [[ $(uname) == "Darwin" ]]; then + # You're already running with homebrew or macports to satisfy the + # bash>=4 requirement, so requiring GNU sed is entirely reasonable. + sed=gsed +else + sed=sed +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[@]}" +$sed -i 's!#include.*compat.h"!!g' "${all_files[@]}" + +# FStar_UInt_8_16_32_64 contains definitions useful in the general case, but not +# for us; trim! +$sed -i -z 's!\(extern\|typedef\)[^;]*;\n\n!!g' include/krml/FStar_UInt_8_16_32_64.h + +# This contains static inline prototypes that are defined in +# FStar_UInt_8_16_32_64; they are by default repeated for safety of separate +# compilation, but this is not necessary. +$sed -i 's!#include.*Hacl_Krmllib.h"!!g' "${all_files[@]}" + +# This header is useful for *other* algorithms that refer to SHA2, e.g. Ed25519 +# which needs to compute a digest of a message before signing it. Here, since no +# other algorithm builds upon SHA2, this internal header is useless (and is not +# 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: +# +# * +# ... 384 or 512 ... { +# * +# } +# +# 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 \n!#include \n#include "python_hacl_namespaces.h"\n!' Hacl_Streaming_SHA2.h + +# Finally, we remove a bunch of ifdefs from target.h that are, again, useful in +# the general case, but not exercised by the subset of HACL* that we vendor. +$sed -z -i 's!#ifndef KRML_\(HOST_PRINTF\|HOST_EXIT\|PRE_ALIGN\|POST_ALIGN\|ALIGNED_MALLOC\|ALIGNED_FREE\|HOST_TIME\)\n\(\n\|# [^\n]*\n\|[^#][^\n]*\n\)*#endif\n\n!!g' include/krml/internal/target.h +$sed -z -i 's!\n\n\([^#][^\n]*\n\)*#define KRML_\(EABORT\|EXIT\|CHECK_SIZE\)[^\n]*\(\n [^\n]*\)*!!g' include/krml/internal/target.h +$sed -z -i 's!\n\n\([^#][^\n]*\n\)*#if [^\n]*\n\( [^\n]*\n\)*#define KRML_\(EABORT\|EXIT\|CHECK_SIZE\)[^\n]*\(\n [^\n]*\)*!!g' include/krml/internal/target.h +$sed -z -i 's!\n\n\([^#][^\n]*\n\)*#if [^\n]*\n\( [^\n]*\n\)*# define _\?KRML_\(DEPRECATED\|CHECK_SIZE_PRAGMA\|HOST_EPRINTF\|HOST_SNPRINTF\)[^\n]*\n\([^#][^\n]*\n\|#el[^\n]*\n\|# [^\n]*\n\)*#endif!!g' include/krml/internal/target.h + +echo "Updated; verify all is okay using git diff and git status." diff --git a/Modules/sha256module.c b/Modules/sha256module.c index 17ee86683b7..630e4bf03bb 100644 --- a/Modules/sha256module.c +++ b/Modules/sha256module.c @@ -31,29 +31,33 @@ class SHA256Type "SHAobject *" "&PyType_Type" [clinic start generated code]*/ /*[clinic end generated code: output=da39a3ee5e6b4b0d input=71a39174d4f0a744]*/ -/* Some useful types */ -typedef unsigned char SHA_BYTE; -typedef uint32_t SHA_INT32; /* 32-bit integer */ - -/* The SHA block size and message digest sizes, in bytes */ +/* The SHA block size and maximum message digest sizes, in bytes */ #define SHA_BLOCKSIZE 64 -#define SHA_DIGESTSIZE 32 +#define SHA_DIGESTSIZE 32 -/* The structure for storing SHA info */ +/* The SHA2-224 and SHA2-256 implementations defer to the HACL* verified + * library. */ + +#include "_hacl/Hacl_Streaming_SHA2.h" typedef struct { - PyObject_HEAD - SHA_INT32 digest[8]; /* Message digest */ - SHA_INT32 count_lo, count_hi; /* 64-bit bit count */ - SHA_BYTE data[SHA_BLOCKSIZE]; /* SHA data buffer */ - int local; /* unprocessed amount in data */ - int digestsize; + PyObject_HEAD + // Even though one could conceivably perform run-type checks to tell apart a + // sha224_type from a sha256_type (and thus deduce the digest size), we must + // keep this field because it's exposed as a member field on the underlying + // python object. + // TODO: could we transform this into a getter and get rid of the redundant + // field? + int digestsize; + Hacl_Streaming_SHA2_state_sha2_256 *state; } SHAobject; #include "clinic/sha256module.c.h" +/* We shall use run-time type information in the remainder of this module to + * tell apart SHA2-224 and SHA2-256 */ typedef struct { PyTypeObject* sha224_type; PyTypeObject* sha256_type; @@ -67,321 +71,12 @@ _sha256_get_state(PyObject *module) return (_sha256_state *)state; } -/* When run on a little-endian CPU we need to perform byte reversal on an - array of longwords. */ - -#if PY_LITTLE_ENDIAN -static void longReverse(SHA_INT32 *buffer, int byteCount) -{ - byteCount /= sizeof(*buffer); - for (; byteCount--; buffer++) { - *buffer = _Py_bswap32(*buffer); - } -} -#endif - static void SHAcopy(SHAobject *src, SHAobject *dest) { - dest->local = src->local; dest->digestsize = src->digestsize; - dest->count_lo = src->count_lo; - dest->count_hi = src->count_hi; - memcpy(dest->digest, src->digest, sizeof(src->digest)); - memcpy(dest->data, src->data, sizeof(src->data)); + dest->state = Hacl_Streaming_SHA2_copy_256(src->state); } - -/* ------------------------------------------------------------------------ - * - * This code for the SHA-256 algorithm was noted as public domain. The - * original headers are pasted below. - * - * Several changes have been made to make it more compatible with the - * Python environment and desired interface. - * - */ - -/* LibTomCrypt, modular cryptographic library -- Tom St Denis - * - * LibTomCrypt is a library that provides various cryptographic - * algorithms in a highly modular and flexible manner. - * - * The library is free for all purposes without any express - * guarantee it works. - * - * Tom St Denis, tomstdenis@iahu.ca, https://www.libtom.net - */ - - -/* SHA256 by Tom St Denis */ - -/* Various logical functions */ -#define ROR(x, y)\ -( ((((unsigned long)(x)&0xFFFFFFFFUL)>>(unsigned long)((y)&31)) | \ -((unsigned long)(x)<<(unsigned long)(32-((y)&31)))) & 0xFFFFFFFFUL) -#define Ch(x,y,z) (z ^ (x & (y ^ z))) -#define Maj(x,y,z) (((x | y) & z) | (x & y)) -#define S(x, n) ROR((x),(n)) -#define R(x, n) (((x)&0xFFFFFFFFUL)>>(n)) -#define Sigma0(x) (S(x, 2) ^ S(x, 13) ^ S(x, 22)) -#define Sigma1(x) (S(x, 6) ^ S(x, 11) ^ S(x, 25)) -#define Gamma0(x) (S(x, 7) ^ S(x, 18) ^ R(x, 3)) -#define Gamma1(x) (S(x, 17) ^ S(x, 19) ^ R(x, 10)) - - -static void -sha_transform(SHAobject *sha_info) -{ - int i; - SHA_INT32 S[8], W[64], t0, t1; - - memcpy(W, sha_info->data, sizeof(sha_info->data)); -#if PY_LITTLE_ENDIAN - longReverse(W, (int)sizeof(sha_info->data)); -#endif - - for (i = 16; i < 64; ++i) { - W[i] = Gamma1(W[i - 2]) + W[i - 7] + Gamma0(W[i - 15]) + W[i - 16]; - } - for (i = 0; i < 8; ++i) { - S[i] = sha_info->digest[i]; - } - - /* Compress */ -#define RND(a,b,c,d,e,f,g,h,i,ki) \ - t0 = h + Sigma1(e) + Ch(e, f, g) + ki + W[i]; \ - t1 = Sigma0(a) + Maj(a, b, c); \ - d += t0; \ - h = t0 + t1; - - RND(S[0],S[1],S[2],S[3],S[4],S[5],S[6],S[7],0,0x428a2f98); - RND(S[7],S[0],S[1],S[2],S[3],S[4],S[5],S[6],1,0x71374491); - RND(S[6],S[7],S[0],S[1],S[2],S[3],S[4],S[5],2,0xb5c0fbcf); - RND(S[5],S[6],S[7],S[0],S[1],S[2],S[3],S[4],3,0xe9b5dba5); - RND(S[4],S[5],S[6],S[7],S[0],S[1],S[2],S[3],4,0x3956c25b); - RND(S[3],S[4],S[5],S[6],S[7],S[0],S[1],S[2],5,0x59f111f1); - RND(S[2],S[3],S[4],S[5],S[6],S[7],S[0],S[1],6,0x923f82a4); - RND(S[1],S[2],S[3],S[4],S[5],S[6],S[7],S[0],7,0xab1c5ed5); - RND(S[0],S[1],S[2],S[3],S[4],S[5],S[6],S[7],8,0xd807aa98); - RND(S[7],S[0],S[1],S[2],S[3],S[4],S[5],S[6],9,0x12835b01); - RND(S[6],S[7],S[0],S[1],S[2],S[3],S[4],S[5],10,0x243185be); - RND(S[5],S[6],S[7],S[0],S[1],S[2],S[3],S[4],11,0x550c7dc3); - RND(S[4],S[5],S[6],S[7],S[0],S[1],S[2],S[3],12,0x72be5d74); - RND(S[3],S[4],S[5],S[6],S[7],S[0],S[1],S[2],13,0x80deb1fe); - RND(S[2],S[3],S[4],S[5],S[6],S[7],S[0],S[1],14,0x9bdc06a7); - RND(S[1],S[2],S[3],S[4],S[5],S[6],S[7],S[0],15,0xc19bf174); - RND(S[0],S[1],S[2],S[3],S[4],S[5],S[6],S[7],16,0xe49b69c1); - RND(S[7],S[0],S[1],S[2],S[3],S[4],S[5],S[6],17,0xefbe4786); - RND(S[6],S[7],S[0],S[1],S[2],S[3],S[4],S[5],18,0x0fc19dc6); - RND(S[5],S[6],S[7],S[0],S[1],S[2],S[3],S[4],19,0x240ca1cc); - RND(S[4],S[5],S[6],S[7],S[0],S[1],S[2],S[3],20,0x2de92c6f); - RND(S[3],S[4],S[5],S[6],S[7],S[0],S[1],S[2],21,0x4a7484aa); - RND(S[2],S[3],S[4],S[5],S[6],S[7],S[0],S[1],22,0x5cb0a9dc); - RND(S[1],S[2],S[3],S[4],S[5],S[6],S[7],S[0],23,0x76f988da); - RND(S[0],S[1],S[2],S[3],S[4],S[5],S[6],S[7],24,0x983e5152); - RND(S[7],S[0],S[1],S[2],S[3],S[4],S[5],S[6],25,0xa831c66d); - RND(S[6],S[7],S[0],S[1],S[2],S[3],S[4],S[5],26,0xb00327c8); - RND(S[5],S[6],S[7],S[0],S[1],S[2],S[3],S[4],27,0xbf597fc7); - RND(S[4],S[5],S[6],S[7],S[0],S[1],S[2],S[3],28,0xc6e00bf3); - RND(S[3],S[4],S[5],S[6],S[7],S[0],S[1],S[2],29,0xd5a79147); - RND(S[2],S[3],S[4],S[5],S[6],S[7],S[0],S[1],30,0x06ca6351); - RND(S[1],S[2],S[3],S[4],S[5],S[6],S[7],S[0],31,0x14292967); - RND(S[0],S[1],S[2],S[3],S[4],S[5],S[6],S[7],32,0x27b70a85); - RND(S[7],S[0],S[1],S[2],S[3],S[4],S[5],S[6],33,0x2e1b2138); - RND(S[6],S[7],S[0],S[1],S[2],S[3],S[4],S[5],34,0x4d2c6dfc); - RND(S[5],S[6],S[7],S[0],S[1],S[2],S[3],S[4],35,0x53380d13); - RND(S[4],S[5],S[6],S[7],S[0],S[1],S[2],S[3],36,0x650a7354); - RND(S[3],S[4],S[5],S[6],S[7],S[0],S[1],S[2],37,0x766a0abb); - RND(S[2],S[3],S[4],S[5],S[6],S[7],S[0],S[1],38,0x81c2c92e); - RND(S[1],S[2],S[3],S[4],S[5],S[6],S[7],S[0],39,0x92722c85); - RND(S[0],S[1],S[2],S[3],S[4],S[5],S[6],S[7],40,0xa2bfe8a1); - RND(S[7],S[0],S[1],S[2],S[3],S[4],S[5],S[6],41,0xa81a664b); - RND(S[6],S[7],S[0],S[1],S[2],S[3],S[4],S[5],42,0xc24b8b70); - RND(S[5],S[6],S[7],S[0],S[1],S[2],S[3],S[4],43,0xc76c51a3); - RND(S[4],S[5],S[6],S[7],S[0],S[1],S[2],S[3],44,0xd192e819); - RND(S[3],S[4],S[5],S[6],S[7],S[0],S[1],S[2],45,0xd6990624); - RND(S[2],S[3],S[4],S[5],S[6],S[7],S[0],S[1],46,0xf40e3585); - RND(S[1],S[2],S[3],S[4],S[5],S[6],S[7],S[0],47,0x106aa070); - RND(S[0],S[1],S[2],S[3],S[4],S[5],S[6],S[7],48,0x19a4c116); - RND(S[7],S[0],S[1],S[2],S[3],S[4],S[5],S[6],49,0x1e376c08); - RND(S[6],S[7],S[0],S[1],S[2],S[3],S[4],S[5],50,0x2748774c); - RND(S[5],S[6],S[7],S[0],S[1],S[2],S[3],S[4],51,0x34b0bcb5); - RND(S[4],S[5],S[6],S[7],S[0],S[1],S[2],S[3],52,0x391c0cb3); - RND(S[3],S[4],S[5],S[6],S[7],S[0],S[1],S[2],53,0x4ed8aa4a); - RND(S[2],S[3],S[4],S[5],S[6],S[7],S[0],S[1],54,0x5b9cca4f); - RND(S[1],S[2],S[3],S[4],S[5],S[6],S[7],S[0],55,0x682e6ff3); - RND(S[0],S[1],S[2],S[3],S[4],S[5],S[6],S[7],56,0x748f82ee); - RND(S[7],S[0],S[1],S[2],S[3],S[4],S[5],S[6],57,0x78a5636f); - RND(S[6],S[7],S[0],S[1],S[2],S[3],S[4],S[5],58,0x84c87814); - RND(S[5],S[6],S[7],S[0],S[1],S[2],S[3],S[4],59,0x8cc70208); - RND(S[4],S[5],S[6],S[7],S[0],S[1],S[2],S[3],60,0x90befffa); - RND(S[3],S[4],S[5],S[6],S[7],S[0],S[1],S[2],61,0xa4506ceb); - RND(S[2],S[3],S[4],S[5],S[6],S[7],S[0],S[1],62,0xbef9a3f7); - RND(S[1],S[2],S[3],S[4],S[5],S[6],S[7],S[0],63,0xc67178f2); - -#undef RND - - /* feedback */ - for (i = 0; i < 8; i++) { - sha_info->digest[i] = sha_info->digest[i] + S[i]; - } - -} - - - -/* initialize the SHA digest */ - -static void -sha_init(SHAobject *sha_info) -{ - sha_info->digest[0] = 0x6A09E667L; - sha_info->digest[1] = 0xBB67AE85L; - sha_info->digest[2] = 0x3C6EF372L; - sha_info->digest[3] = 0xA54FF53AL; - sha_info->digest[4] = 0x510E527FL; - sha_info->digest[5] = 0x9B05688CL; - sha_info->digest[6] = 0x1F83D9ABL; - sha_info->digest[7] = 0x5BE0CD19L; - sha_info->count_lo = 0L; - sha_info->count_hi = 0L; - sha_info->local = 0; - sha_info->digestsize = 32; -} - -static void -sha224_init(SHAobject *sha_info) -{ - sha_info->digest[0] = 0xc1059ed8L; - sha_info->digest[1] = 0x367cd507L; - sha_info->digest[2] = 0x3070dd17L; - sha_info->digest[3] = 0xf70e5939L; - sha_info->digest[4] = 0xffc00b31L; - sha_info->digest[5] = 0x68581511L; - sha_info->digest[6] = 0x64f98fa7L; - sha_info->digest[7] = 0xbefa4fa4L; - sha_info->count_lo = 0L; - sha_info->count_hi = 0L; - sha_info->local = 0; - sha_info->digestsize = 28; -} - - -/* update the SHA digest */ - -static void -sha_update(SHAobject *sha_info, SHA_BYTE *buffer, Py_ssize_t count) -{ - Py_ssize_t i; - SHA_INT32 clo; - - clo = sha_info->count_lo + ((SHA_INT32) count << 3); - if (clo < sha_info->count_lo) { - ++sha_info->count_hi; - } - sha_info->count_lo = clo; - sha_info->count_hi += (SHA_INT32) count >> 29; - if (sha_info->local) { - i = SHA_BLOCKSIZE - sha_info->local; - if (i > count) { - i = count; - } - memcpy(((SHA_BYTE *) sha_info->data) + sha_info->local, buffer, i); - count -= i; - buffer += i; - sha_info->local += (int)i; - if (sha_info->local == SHA_BLOCKSIZE) { - sha_transform(sha_info); - } - else { - return; - } - } - while (count >= SHA_BLOCKSIZE) { - memcpy(sha_info->data, buffer, SHA_BLOCKSIZE); - buffer += SHA_BLOCKSIZE; - count -= SHA_BLOCKSIZE; - sha_transform(sha_info); - } - memcpy(sha_info->data, buffer, count); - sha_info->local = (int)count; -} - -/* finish computing the SHA digest */ - -static void -sha_final(unsigned char digest[SHA_DIGESTSIZE], SHAobject *sha_info) -{ - int count; - SHA_INT32 lo_bit_count, hi_bit_count; - - lo_bit_count = sha_info->count_lo; - hi_bit_count = sha_info->count_hi; - count = (int) ((lo_bit_count >> 3) & 0x3f); - ((SHA_BYTE *) sha_info->data)[count++] = 0x80; - if (count > SHA_BLOCKSIZE - 8) { - memset(((SHA_BYTE *) sha_info->data) + count, 0, - SHA_BLOCKSIZE - count); - sha_transform(sha_info); - memset((SHA_BYTE *) sha_info->data, 0, SHA_BLOCKSIZE - 8); - } - else { - memset(((SHA_BYTE *) sha_info->data) + count, 0, - SHA_BLOCKSIZE - 8 - count); - } - - /* GJS: note that we add the hi/lo in big-endian. sha_transform will - swap these values into host-order. */ - sha_info->data[56] = (hi_bit_count >> 24) & 0xff; - sha_info->data[57] = (hi_bit_count >> 16) & 0xff; - sha_info->data[58] = (hi_bit_count >> 8) & 0xff; - sha_info->data[59] = (hi_bit_count >> 0) & 0xff; - sha_info->data[60] = (lo_bit_count >> 24) & 0xff; - sha_info->data[61] = (lo_bit_count >> 16) & 0xff; - sha_info->data[62] = (lo_bit_count >> 8) & 0xff; - sha_info->data[63] = (lo_bit_count >> 0) & 0xff; - sha_transform(sha_info); - digest[ 0] = (unsigned char) ((sha_info->digest[0] >> 24) & 0xff); - digest[ 1] = (unsigned char) ((sha_info->digest[0] >> 16) & 0xff); - digest[ 2] = (unsigned char) ((sha_info->digest[0] >> 8) & 0xff); - digest[ 3] = (unsigned char) ((sha_info->digest[0] ) & 0xff); - digest[ 4] = (unsigned char) ((sha_info->digest[1] >> 24) & 0xff); - digest[ 5] = (unsigned char) ((sha_info->digest[1] >> 16) & 0xff); - digest[ 6] = (unsigned char) ((sha_info->digest[1] >> 8) & 0xff); - digest[ 7] = (unsigned char) ((sha_info->digest[1] ) & 0xff); - digest[ 8] = (unsigned char) ((sha_info->digest[2] >> 24) & 0xff); - digest[ 9] = (unsigned char) ((sha_info->digest[2] >> 16) & 0xff); - digest[10] = (unsigned char) ((sha_info->digest[2] >> 8) & 0xff); - digest[11] = (unsigned char) ((sha_info->digest[2] ) & 0xff); - digest[12] = (unsigned char) ((sha_info->digest[3] >> 24) & 0xff); - digest[13] = (unsigned char) ((sha_info->digest[3] >> 16) & 0xff); - digest[14] = (unsigned char) ((sha_info->digest[3] >> 8) & 0xff); - digest[15] = (unsigned char) ((sha_info->digest[3] ) & 0xff); - digest[16] = (unsigned char) ((sha_info->digest[4] >> 24) & 0xff); - digest[17] = (unsigned char) ((sha_info->digest[4] >> 16) & 0xff); - digest[18] = (unsigned char) ((sha_info->digest[4] >> 8) & 0xff); - digest[19] = (unsigned char) ((sha_info->digest[4] ) & 0xff); - digest[20] = (unsigned char) ((sha_info->digest[5] >> 24) & 0xff); - digest[21] = (unsigned char) ((sha_info->digest[5] >> 16) & 0xff); - digest[22] = (unsigned char) ((sha_info->digest[5] >> 8) & 0xff); - digest[23] = (unsigned char) ((sha_info->digest[5] ) & 0xff); - digest[24] = (unsigned char) ((sha_info->digest[6] >> 24) & 0xff); - digest[25] = (unsigned char) ((sha_info->digest[6] >> 16) & 0xff); - digest[26] = (unsigned char) ((sha_info->digest[6] >> 8) & 0xff); - digest[27] = (unsigned char) ((sha_info->digest[6] ) & 0xff); - digest[28] = (unsigned char) ((sha_info->digest[7] >> 24) & 0xff); - digest[29] = (unsigned char) ((sha_info->digest[7] >> 16) & 0xff); - digest[30] = (unsigned char) ((sha_info->digest[7] >> 8) & 0xff); - digest[31] = (unsigned char) ((sha_info->digest[7] ) & 0xff); -} - -/* - * End of copied SHA code. - * - * ------------------------------------------------------------------------ - */ - - static SHAobject * newSHA224object(_sha256_state *state) { @@ -409,14 +104,31 @@ SHA_traverse(PyObject *ptr, visitproc visit, void *arg) } static void -SHA_dealloc(PyObject *ptr) +SHA_dealloc(SHAobject *ptr) { + Hacl_Streaming_SHA2_free_256(ptr->state); PyTypeObject *tp = Py_TYPE(ptr); PyObject_GC_UnTrack(ptr); PyObject_GC_Del(ptr); Py_DECREF(tp); } +/* HACL* takes a uint32_t for the length of its parameter, but Py_ssize_t can be + * 64 bits. */ +static void update_256(Hacl_Streaming_SHA2_state_sha2_256 *state, uint8_t *buf, Py_ssize_t len) { + /* Note: we explicitly ignore the error code on the basis that it would take > + * 1 billion years to overflow the maximum admissible length for SHA2-256 + * (namely, 2^61-1 bytes). */ + while (len > UINT32_MAX) { + Hacl_Streaming_SHA2_update_256(state, buf, UINT32_MAX); + len -= UINT32_MAX; + buf += UINT32_MAX; + } + /* Cast to uint32_t is safe: upon exiting the loop, len <= UINT32_MAX, and + * therefore fits in a uint32_t */ + Hacl_Streaming_SHA2_update_256(state, buf, (uint32_t) len); +} + /* External methods for a hash object */ @@ -458,11 +170,10 @@ static PyObject * SHA256Type_digest_impl(SHAobject *self) /*[clinic end generated code: output=46616a5e909fbc3d input=f1f4cfea5cbde35c]*/ { - unsigned char digest[SHA_DIGESTSIZE]; - SHAobject temp; - - SHAcopy(self, &temp); - sha_final(digest, &temp); + uint8_t digest[SHA_DIGESTSIZE]; + // HACL performs copies under the hood so that self->state remains valid + // after this call. + Hacl_Streaming_SHA2_finish_256(self->state, digest); return PyBytes_FromStringAndSize((const char *)digest, self->digestsize); } @@ -476,13 +187,8 @@ static PyObject * SHA256Type_hexdigest_impl(SHAobject *self) /*[clinic end generated code: output=725f8a7041ae97f3 input=0cc4c714693010d1]*/ { - unsigned char digest[SHA_DIGESTSIZE]; - SHAobject temp; - - /* Get the raw (binary) digest value */ - SHAcopy(self, &temp); - sha_final(digest, &temp); - + uint8_t digest[SHA_DIGESTSIZE]; + Hacl_Streaming_SHA2_finish_256(self->state, digest); return _Py_strhex((const char *)digest, self->digestsize); } @@ -503,7 +209,7 @@ SHA256Type_update(SHAobject *self, PyObject *obj) GET_BUFFER_VIEW_OR_ERROUT(obj, &buf); - sha_update(self, buf.buf, buf.len); + update_256(self->state, buf.buf, buf.len); PyBuffer_Release(&buf); Py_RETURN_NONE; @@ -524,12 +230,12 @@ SHA256_get_block_size(PyObject *self, void *closure) } static PyObject * -SHA256_get_name(PyObject *self, void *closure) +SHA256_get_name(SHAobject *self, void *closure) { - if (((SHAobject *)self)->digestsize == 32) - return PyUnicode_FromStringAndSize("sha256", 6); - else + if (self->digestsize == 28) { return PyUnicode_FromStringAndSize("sha224", 6); + } + return PyUnicode_FromStringAndSize("sha256", 6); } static PyGetSetDef SHA_getseters[] = { @@ -606,7 +312,8 @@ _sha256_sha256_impl(PyObject *module, PyObject *string, int usedforsecurity) return NULL; } - sha_init(new); + new->state = Hacl_Streaming_SHA2_create_in_256(); + new->digestsize = 32; if (PyErr_Occurred()) { Py_DECREF(new); @@ -616,7 +323,7 @@ _sha256_sha256_impl(PyObject *module, PyObject *string, int usedforsecurity) return NULL; } if (string) { - sha_update(new, buf.buf, buf.len); + update_256(new->state, buf.buf, buf.len); PyBuffer_Release(&buf); } @@ -651,7 +358,8 @@ _sha256_sha224_impl(PyObject *module, PyObject *string, int usedforsecurity) return NULL; } - sha224_init(new); + new->state = Hacl_Streaming_SHA2_create_in_224(); + new->digestsize = 28; if (PyErr_Occurred()) { Py_DECREF(new); @@ -661,7 +369,7 @@ _sha256_sha224_impl(PyObject *module, PyObject *string, int usedforsecurity) return NULL; } if (string) { - sha_update(new, buf.buf, buf.len); + update_256(new->state, buf.buf, buf.len); PyBuffer_Release(&buf); } diff --git a/PCbuild/pythoncore.vcxproj b/PCbuild/pythoncore.vcxproj index 397d22abe23..e8e9ff01e30 100644 --- a/PCbuild/pythoncore.vcxproj +++ b/PCbuild/pythoncore.vcxproj @@ -100,7 +100,7 @@ /Zm200 %(AdditionalOptions) - $(PySourcePath)Python;%(AdditionalIncludeDirectories) + $(PySourcePath)Modules\_hacl\include;$(PySourcePath)Modules\_hacl\internal;$(PySourcePath)Python;%(AdditionalIncludeDirectories) $(zlibDir);%(AdditionalIncludeDirectories) _USRDLL;Py_BUILD_CORE;Py_BUILD_CORE_BUILTIN;Py_ENABLE_SHARED;MS_DLL_ID="$(SysWinVer)";%(PreprocessorDefinitions) _Py_HAVE_ZLIB;%(PreprocessorDefinitions) @@ -407,6 +407,7 @@ + diff --git a/PCbuild/pythoncore.vcxproj.filters b/PCbuild/pythoncore.vcxproj.filters index bcbedcc3235..4820db6f2c3 100644 --- a/PCbuild/pythoncore.vcxproj.filters +++ b/PCbuild/pythoncore.vcxproj.filters @@ -866,6 +866,9 @@ Modules + + Modules + Modules diff --git a/configure b/configure index aef8103085b..97694c602d1 100755 --- a/configure +++ b/configure @@ -24426,6 +24426,7 @@ SRCDIRS="\ Modules/_ctypes \ Modules/_decimal \ Modules/_decimal/libmpdec \ + Modules/_hacl \ Modules/_io \ Modules/_multiprocessing \ Modules/_sha3 \ @@ -26966,7 +26967,7 @@ fi as_fn_append MODULE_BLOCK "MODULE__SHA256_STATE=$py_cv_module__sha256$as_nl" if test "x$py_cv_module__sha256" = xyes; then : - + as_fn_append MODULE_BLOCK "MODULE__SHA256_CFLAGS=-I\$(srcdir)/Modules/_hacl/include -I\$(srcdir)/Modules/_hacl/internal -D_BSD_SOURCE -D_DEFAULT_SOURCE$as_nl" fi diff --git a/configure.ac b/configure.ac index 010bca855f0..09369b985b3 100644 --- a/configure.ac +++ b/configure.ac @@ -6508,6 +6508,7 @@ SRCDIRS="\ Modules/_ctypes \ Modules/_decimal \ Modules/_decimal/libmpdec \ + Modules/_hacl \ Modules/_io \ Modules/_multiprocessing \ Modules/_sha3 \ @@ -7197,7 +7198,9 @@ dnl By default we always compile these even when OpenSSL is available dnl (issue #14693). The modules are small. PY_STDLIB_MOD([_md5], [test "$with_builtin_md5" = yes]) PY_STDLIB_MOD([_sha1], [test "$with_builtin_sha1" = yes]) -PY_STDLIB_MOD([_sha256], [test "$with_builtin_sha256" = yes]) +PY_STDLIB_MOD([_sha256], + [test "$with_builtin_sha256" = yes], [], + [-I\$(srcdir)/Modules/_hacl/include -I\$(srcdir)/Modules/_hacl/internal -D_BSD_SOURCE -D_DEFAULT_SOURCE]) PY_STDLIB_MOD([_sha512], [test "$with_builtin_sha512" = yes]) PY_STDLIB_MOD([_sha3], [test "$with_builtin_sha3" = yes]) PY_STDLIB_MOD([_blake2],