languages/cpython
languages/cpython
1
0
Fork 0
mirror of https://github.com/python/cpython synced 2024-09-05 00:05:39 +00:00
Code Issues Packages Projects Releases Wiki Activity

gh-99108: Replace SHA2-224 & 256 with verified code from HACL* (#99109)

Browse source 
replacing hashlib primitives (for the non-OpenSSL case) with verified implementations from HACL*. This is the first PR in the series, and focuses specifically on SHA2-256 and SHA2-224.

This PR imports Hacl_Streaming_SHA2 into the Python tree. This is the HACL* implementation of SHA2, which combines a core implementation of SHA2 along with a layer of buffer management that allows updating the digest with any number of bytes. This supersedes the previous implementation in the tree.

@franziskuskiefer was kind enough to benchmark the changes: in addition to being verified (thus providing significant safety and security improvements), this implementation also provides a sizeable performance boost!

```
---------------------------------------------------------------
Benchmark                     Time             CPU   Iterations
---------------------------------------------------------------
Sha2_256_Streaming            3163 ns      3160 ns       219353     // this PR
LibTomCrypt_Sha2_256          5057 ns      5056 ns       136234     // library used by Python currently
``` 

The changes in this PR are as follows:
- import the subset of HACL* that covers SHA2-256/224 into `Modules/_hacl`
- rewire sha256module.c to use the HACL* implementation

Co-authored-by: Gregory P. Smith [Google LLC] <greg@krypto.org>
Co-authored-by: Erlend E. Aasland <erlend.aasland@protonmail.com>
This commit is contained in:
Jonathan Protzenko 2023-02-06 18:11:01 -08:00 committed by GitHub
parent 914f8fd9f7
commit 1fcc0efdaa
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
18 changed files with 1779 additions and 350 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
Lib/test/test_hashlib.py
View file

@ -22,6 +22,7 @@
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 @@ def test_large_update(self):
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()

2
Makefile.pre.in
View file

@ -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

4
Misc/NEWS.d/next/Security/2022-11-08-12-06-52.gh-issue-99108.4Wrsuh.rst Normal file
View file

@ -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* <https://github.com/hacl-star/hacl-star/>`_ project. The
builtins remain a fallback only used when OpenSSL does not provide them.

2
Modules/Setup.stdlib.in
View file

@ -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

682
Modules/_hacl/Hacl_Streaming_SHA2.c Normal file
View file

@ -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);
}

136
Modules/_hacl/Hacl_Streaming_SHA2.h Normal file
View file

@ -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 <string.h>
#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

29
Modules/_hacl/README.md Normal file
View file

@ -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.

109
Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h Normal file
View file

@ -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 <inttypes.h>
#include <stdbool.h>
#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

218
Modules/_hacl/include/krml/internal/target.h Normal file
View file

@ -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 <stdlib.h>
#include <stddef.h>
#include <stdio.h>
#include <stdbool.h>
#include <inttypes.h>
#include <limits.h>
#include <assert.h>
/* 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

230
Modules/_hacl/include/krml/lowstar_endianness.h Normal file
View file

@ -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 <string.h>
#include <inttypes.h>
/******************************************************************************/
/* Implementing C.fst (part 2: endian-ness macros) */
/******************************************************************************/
/* ... for Linux */
#if defined(__linux__) || defined(__CYGWIN__) || defined (__USE_SYSTEM_ENDIAN_H__) || defined(__GLIBC__)
# include <endian.h>
/* ... for OSX */
#elif defined(__APPLE__)
# include <libkern/OSByteOrder.h>
# 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 <sys/byteorder.h>
# 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 <sys/endian.h>
#elif defined(__OpenBSD__)
# include <endian.h>
/* ... for Windows (MSVC)... not targeting XBOX 360! */
#elif defined(_MSC_VER)
# include <stdlib.h>
# 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

28
Modules/_hacl/include/python_hacl_namespaces.h Normal file
View file

@ -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

135
Modules/_hacl/internal/Hacl_SHA2_Generic.h Normal file
View file

@ -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 <string.h>
#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

132
Modules/_hacl/refresh.sh Executable file
View file

@ -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:
#
# <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
# 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."

398
Modules/sha256module.c
View file

@ -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);
}

3
PCbuild/pythoncore.vcxproj
View file

@ -100,7 +100,7 @@
<ItemDefinitionGroup>
<ClCompile>
<AdditionalOptions>/Zm200 %(AdditionalOptions)</AdditionalOptions>
<AdditionalIncludeDirectories>$(PySourcePath)Python;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
<AdditionalIncludeDirectories>$(PySourcePath)Modules\_hacl\include;$(PySourcePath)Modules\_hacl\internal;$(PySourcePath)Python;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
<AdditionalIncludeDirectories Condition="$(IncludeExternals)">$(zlibDir);%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
<PreprocessorDefinitions>_USRDLL;Py_BUILD_CORE;Py_BUILD_CORE_BUILTIN;Py_ENABLE_SHARED;MS_DLL_ID="$(SysWinVer)";%(PreprocessorDefinitions)</PreprocessorDefinitions>
<PreprocessorDefinitions Condition="$(IncludeExternals)">_Py_HAVE_ZLIB;%(PreprocessorDefinitions)</PreprocessorDefinitions>
@ -407,6 +407,7 @@
<ClCompile Include="..\Modules\posixmodule.c" />
<ClCompile Include="..\Modules\rotatingtree.c" />
<ClCompile Include="..\Modules\sha1module.c" />
<ClCompile Include="..\Modules\_hacl\Hacl_Streaming_SHA2.c" />
<ClCompile Include="..\Modules\sha256module.c" />
<ClCompile Include="..\Modules\sha512module.c" />
<ClCompile Include="..\Modules\signalmodule.c" />

3
PCbuild/pythoncore.vcxproj.filters
View file

@ -866,6 +866,9 @@
<ClCompile Include="..\Modules\sha1module.c">
<Filter>Modules</Filter>
</ClCompile>
<ClCompile Include="..\Modules\_hacl\Hacl_Streaming_SHA2.c">
<Filter>Modules</Filter>
</ClCompile>
<ClCompile Include="..\Modules\sha256module.c">
<Filter>Modules</Filter>
</ClCompile>

3
configure generated vendored
View file

@ -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

5
configure.ac
View file

@ -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],