Mirrors_Framework/paparazzi
1
0
Fork 0
mirror of https://github.com/paparazzi/paparazzi.git synced 2026-05-09 14:18:00 +08:00
Code Issues Actions 27 Packages Projects Releases Wiki Activity

Added HACL-C module and secure telemetry module (#2163)

Browse Source
This commit is contained in:
Michal Podhradsky
2017-11-04 16:21:14 -07:00
committed by GitHub
parent 14d17a6558
commit bbb45f89d6
39 changed files with 10545 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
conf/modules/haclc.xml
+25
View File
@@ -0,0 +1,25 @@
<!DOCTYPE module SYSTEM "module.dtd">
<module name="haclc" dir="datalink/hacl-c" task="datalink">
<doc>
<description>
HACL* verified cryptographic library
see https://github.com/mitls/hacl-star for details
</description>
</doc>
<makefile target="!fbw|sim|nps|hitl">
<file name="Chacha20Poly1305.c"/>
<file name="kremlib.c"/>
<file name="Hacl_Policies.c"/>
<file name="AEAD_Poly1305_64.c"/>
<file name="Chacha20.c"/>
<file name="Curve25519.c"/>
<file name="Ed25519.c"/>
<file name="SHA2_512.c"/>
<raw>
# to not use 128 bit arithmetic
ap.CFLAGS += -DKRML_NOUINT128
</raw>
</makefile>
</module>
conf/modules/telemetry_transparent_secure.xml
+49
View File
@@ -0,0 +1,49 @@
<!DOCTYPE module SYSTEM "module.dtd">
<module name="telemetry_transparent_secure" dir="datalink" task="datalink">
<doc>
<description>
Telemetry using secure PPRZ protocol over UART
Similar to telemetry_transparent, except it uses message scheduling and encryption
</description>
<configure name="MODEM_PORT" value="UARTx" description="UART where the modem is connected to (UART1, UART2, etc)"/>
<configure name="MODEM_BAUD" value="B57600" description="UART baud rate"/>
</doc>
<autoload name="telemetry" type="nps"/>
<autoload name="telemetry" type="sim"/>
<autoload name="haclc"/>
<header>
<file name="spprz_dl.h"/>
</header>
<init fun="spprz_dl_init()"/>
<periodic fun="spprz_dl_periodic()" freq="PERIODIC_FREQUENCY" autorun="TRUE"/>
<event fun="spprz_dl_event()"/>
<makefile target="!fbw|sim|nps|hitl">
<configure name="MODEM_PORT" case="upper|lower"/>
<define name="USE_$(MODEM_PORT_UPPER)"/>
<define name="$(MODEM_PORT_UPPER)_BAUD" value="$(MODEM_BAUD)"/>
<define name="DOWNLINK"/>
<define name="PERIODIC_TELEMETRY"/>
<define name="DOWNLINK_DEVICE" value="$(MODEM_PORT_LOWER)"/>
<define name="PPRZ_UART" value="$(MODEM_PORT_LOWER)"/>
<define name="DOWNLINK_TRANSPORT" value="spprz_tp"/>
<define name="DATALINK" value="PPRZ"/>
<file name="spprz_dl.c"/>
<file name="downlink.c" dir="subsystems/datalink"/>
<file name="datalink.c" dir="subsystems/datalink"/>
<file name="telemetry.c" dir="subsystems/datalink"/>
<file name="secure_pprz_transport.c" dir="pprzlink/src"/>
</makefile>
<makefile target="ap" firmware="fixedwing">
<file name="fixedwing_datalink.c" dir="$(SRC_FIRMWARE)"/>
<file name="ap_downlink.c" dir="$(SRC_FIRMWARE)"/>
</makefile>
<makefile target="ap|fbw" firmware="fixedwing">
<file name="fbw_downlink.c" dir="$(SRC_FIRMWARE)"/>
</makefile>
<makefile target="ap" firmware="rotorcraft">
<file name="rotorcraft_datalink.c" dir="$(SRC_FIRMWARE)"/>
<file name="rotorcraft_telemetry.c" dir="$(SRC_FIRMWARE)"/>
</makefile>
</module>
sw/airborne/modules/datalink/hacl-c/AEAD_Poly1305_64.c
+475
View File
@@ -0,0 +1,475 @@
#include "AEAD_Poly1305_64.h"
inline static void Hacl_Bignum_Modulo_reduce(uint64_t *b)
{
uint64_t b0 = b[0];
b[0] = (b0 << (uint32_t )4) + (b0 << (uint32_t )2);
}
inline static void Hacl_Bignum_Modulo_carry_top(uint64_t *b)
{
uint64_t b2 = b[2];
uint64_t b0 = b[0];
uint64_t b2_42 = b2 >> (uint32_t )42;
b[2] = b2 & (uint64_t )0x3ffffffffff;
b[0] = (b2_42 << (uint32_t )2) + b2_42 + b0;
}
inline static void Hacl_Bignum_Modulo_carry_top_wide(FStar_UInt128_t *b)
{
FStar_UInt128_t b2 = b[2];
FStar_UInt128_t b0 = b[0];
FStar_UInt128_t
b2_ = FStar_UInt128_logand(b2, FStar_Int_Cast_Full_uint64_to_uint128((uint64_t )0x3ffffffffff));
uint64_t
b2_42 = FStar_Int_Cast_Full_uint128_to_uint64(FStar_UInt128_shift_right(b2, (uint32_t )42));
FStar_UInt128_t
b0_ =
FStar_UInt128_add(b0,
FStar_Int_Cast_Full_uint64_to_uint128((b2_42 << (uint32_t )2) + b2_42));
b[2] = b2_;
b[0] = b0_;
}
inline static void
Hacl_Bignum_Fproduct_copy_from_wide_(uint64_t *output, FStar_UInt128_t *input)
{
for (uint32_t i = (uint32_t )0; i < (uint32_t )3; i = i + (uint32_t )1)
{
FStar_UInt128_t uu____429 = input[i];
uint64_t uu____428 = FStar_Int_Cast_Full_uint128_to_uint64(uu____429);
output[i] = uu____428;
}
}
inline static void Hacl_Bignum_Fproduct_shift(uint64_t *output)
{
uint64_t tmp = output[2];
for (uint32_t i = (uint32_t )0; i < (uint32_t )2; i = i + (uint32_t )1)
{
uint32_t ctr = (uint32_t )3 - i - (uint32_t )1;
uint64_t z = output[ctr - (uint32_t )1];
output[ctr] = z;
}
output[0] = tmp;
}
inline static void
Hacl_Bignum_Fproduct_sum_scalar_multiplication_(
FStar_UInt128_t *output,
uint64_t *input,
uint64_t s
)
{
for (uint32_t i = (uint32_t )0; i < (uint32_t )3; i = i + (uint32_t )1)
{
FStar_UInt128_t uu____871 = output[i];
uint64_t uu____874 = input[i];
FStar_UInt128_t
uu____870 = FStar_UInt128_add_mod(uu____871, FStar_UInt128_mul_wide(uu____874, s));
output[i] = uu____870;
}
}
inline static void Hacl_Bignum_Fproduct_carry_wide_(FStar_UInt128_t *tmp)
{
for (uint32_t i = (uint32_t )0; i < (uint32_t )2; i = i + (uint32_t )1)
{
uint32_t ctr = i;
FStar_UInt128_t tctr = tmp[ctr];
FStar_UInt128_t tctrp1 = tmp[ctr + (uint32_t )1];
uint64_t
r0 =
FStar_Int_Cast_Full_uint128_to_uint64(tctr)
& (((uint64_t )1 << (uint32_t )44) - (uint64_t )1);
FStar_UInt128_t c = FStar_UInt128_shift_right(tctr, (uint32_t )44);
tmp[ctr] = FStar_Int_Cast_Full_uint64_to_uint128(r0);
tmp[ctr + (uint32_t )1] = FStar_UInt128_add(tctrp1, c);
}
}
inline static void Hacl_Bignum_Fproduct_carry_limb_(uint64_t *tmp)
{
for (uint32_t i = (uint32_t )0; i < (uint32_t )2; i = i + (uint32_t )1)
{
uint32_t ctr = i;
uint64_t tctr = tmp[ctr];
uint64_t tctrp1 = tmp[ctr + (uint32_t )1];
uint64_t r0 = tctr & (((uint64_t )1 << (uint32_t )44) - (uint64_t )1);
uint64_t c = tctr >> (uint32_t )44;
tmp[ctr] = r0;
tmp[ctr + (uint32_t )1] = tctrp1 + c;
}
}
inline static void Hacl_Bignum_Fmul_shift_reduce(uint64_t *output)
{
Hacl_Bignum_Fproduct_shift(output);
Hacl_Bignum_Modulo_reduce(output);
}
static void
Hacl_Bignum_Fmul_mul_shift_reduce_(FStar_UInt128_t *output, uint64_t *input, uint64_t *input2)
{
for (uint32_t i = (uint32_t )0; i < (uint32_t )2; i = i + (uint32_t )1)
{
uint64_t input2i = input2[i];
Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i);
Hacl_Bignum_Fmul_shift_reduce(input);
}
uint32_t i = (uint32_t )2;
uint64_t input2i = input2[i];
Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i);
}
inline static void Hacl_Bignum_Fmul_fmul_(uint64_t *output, uint64_t *input, uint64_t *input2)
{
KRML_CHECK_SIZE(FStar_Int_Cast_Full_uint64_to_uint128((uint64_t )0), (uint32_t )3);
FStar_UInt128_t t[3];
for (uintmax_t _i = 0; _i < (uint32_t )3; ++_i)
t[_i] = FStar_Int_Cast_Full_uint64_to_uint128((uint64_t )0);
Hacl_Bignum_Fmul_mul_shift_reduce_(t, input, input2);
Hacl_Bignum_Fproduct_carry_wide_(t);
Hacl_Bignum_Modulo_carry_top_wide(t);
Hacl_Bignum_Fproduct_copy_from_wide_(output, t);
uint64_t i0 = output[0];
uint64_t i1 = output[1];
uint64_t i0_ = i0 & (((uint64_t )1 << (uint32_t )44) - (uint64_t )1);
uint64_t i1_ = i1 + (i0 >> (uint32_t )44);
output[0] = i0_;
output[1] = i1_;
}
inline static void Hacl_Bignum_Fmul_fmul(uint64_t *output, uint64_t *input, uint64_t *input2)
{
uint64_t tmp[3] = { 0 };
memcpy(tmp, input, (uint32_t )3 * sizeof input[0]);
Hacl_Bignum_Fmul_fmul_(output, tmp, input2);
}
inline static void
Hacl_Bignum_AddAndMultiply_add_and_multiply(uint64_t *acc, uint64_t *block, uint64_t *r)
{
for (uint32_t i = (uint32_t )0; i < (uint32_t )3; i = i + (uint32_t )1)
{
uint64_t uu____871 = acc[i];
uint64_t uu____874 = block[i];
uint64_t uu____870 = uu____871 + uu____874;
acc[i] = uu____870;
}
Hacl_Bignum_Fmul_fmul(acc, acc, r);
}
inline static void
Hacl_Impl_Poly1305_64_poly1305_update(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *m
)
{
Hacl_Impl_Poly1305_64_State_poly1305_state scrut0 = st;
uint64_t *h = scrut0.h;
uint64_t *acc = h;
Hacl_Impl_Poly1305_64_State_poly1305_state scrut = st;
uint64_t *r = scrut.r;
uint64_t *r3 = r;
uint64_t tmp[3] = { 0 };
FStar_UInt128_t m0 = load128_le(m);
uint64_t r0 = FStar_Int_Cast_Full_uint128_to_uint64(m0) & (uint64_t )0xfffffffffff;
uint64_t
r1 =
FStar_Int_Cast_Full_uint128_to_uint64(FStar_UInt128_shift_right(m0, (uint32_t )44))
& (uint64_t )0xfffffffffff;
uint64_t
r2 = FStar_Int_Cast_Full_uint128_to_uint64(FStar_UInt128_shift_right(m0, (uint32_t )88));
tmp[0] = r0;
tmp[1] = r1;
tmp[2] = r2;
uint64_t b2 = tmp[2];
uint64_t b2_ = (uint64_t )0x10000000000 | b2;
tmp[2] = b2_;
Hacl_Bignum_AddAndMultiply_add_and_multiply(acc, tmp, r3);
}
inline static void
Hacl_Impl_Poly1305_64_poly1305_process_last_block_(
uint8_t *block,
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *m,
uint64_t rem_
)
{
uint64_t tmp[3] = { 0 };
FStar_UInt128_t m0 = load128_le(block);
uint64_t r0 = FStar_Int_Cast_Full_uint128_to_uint64(m0) & (uint64_t )0xfffffffffff;
uint64_t
r1 =
FStar_Int_Cast_Full_uint128_to_uint64(FStar_UInt128_shift_right(m0, (uint32_t )44))
& (uint64_t )0xfffffffffff;
uint64_t
r2 = FStar_Int_Cast_Full_uint128_to_uint64(FStar_UInt128_shift_right(m0, (uint32_t )88));
tmp[0] = r0;
tmp[1] = r1;
tmp[2] = r2;
Hacl_Impl_Poly1305_64_State_poly1305_state scrut0 = st;
uint64_t *h = scrut0.h;
Hacl_Impl_Poly1305_64_State_poly1305_state scrut = st;
uint64_t *r = scrut.r;
Hacl_Bignum_AddAndMultiply_add_and_multiply(h, tmp, r);
}
inline static void
Hacl_Impl_Poly1305_64_poly1305_process_last_block(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *m,
uint64_t rem_
)
{
uint8_t zero1 = (uint8_t )0;
KRML_CHECK_SIZE(zero1, (uint32_t )16);
uint8_t block[16];
for (uintmax_t _i = 0; _i < (uint32_t )16; ++_i)
block[_i] = zero1;
uint32_t i0 = (uint32_t )rem_;
uint32_t i = (uint32_t )rem_;
memcpy(block, m, i * sizeof m[0]);
block[i0] = (uint8_t )1;
Hacl_Impl_Poly1305_64_poly1305_process_last_block_(block, st, m, rem_);
}
static void Hacl_Impl_Poly1305_64_poly1305_last_pass(uint64_t *acc)
{
Hacl_Bignum_Fproduct_carry_limb_(acc);
Hacl_Bignum_Modulo_carry_top(acc);
uint64_t a0 = acc[0];
uint64_t a10 = acc[1];
uint64_t a20 = acc[2];
uint64_t a0_ = a0 & (uint64_t )0xfffffffffff;
uint64_t r0 = a0 >> (uint32_t )44;
uint64_t a1_ = (a10 + r0) & (uint64_t )0xfffffffffff;
uint64_t r1 = (a10 + r0) >> (uint32_t )44;
uint64_t a2_ = a20 + r1;
acc[0] = a0_;
acc[1] = a1_;
acc[2] = a2_;
Hacl_Bignum_Modulo_carry_top(acc);
uint64_t i0 = acc[0];
uint64_t i1 = acc[1];
uint64_t i0_ = i0 & (((uint64_t )1 << (uint32_t )44) - (uint64_t )1);
uint64_t i1_ = i1 + (i0 >> (uint32_t )44);
acc[0] = i0_;
acc[1] = i1_;
uint64_t a00 = acc[0];
uint64_t a1 = acc[1];
uint64_t a2 = acc[2];
uint64_t mask0 = FStar_UInt64_gte_mask(a00, (uint64_t )0xffffffffffb);
uint64_t mask1 = FStar_UInt64_eq_mask(a1, (uint64_t )0xfffffffffff);
uint64_t mask2 = FStar_UInt64_eq_mask(a2, (uint64_t )0x3ffffffffff);
uint64_t mask = mask0 & mask1 & mask2;
uint64_t a0_0 = a00 - ((uint64_t )0xffffffffffb & mask);
uint64_t a1_0 = a1 - ((uint64_t )0xfffffffffff & mask);
uint64_t a2_0 = a2 - ((uint64_t )0x3ffffffffff & mask);
acc[0] = a0_0;
acc[1] = a1_0;
acc[2] = a2_0;
}
static Hacl_Impl_Poly1305_64_State_poly1305_state
Hacl_Impl_Poly1305_64_mk_state(uint64_t *r, uint64_t *h)
{
return ((Hacl_Impl_Poly1305_64_State_poly1305_state ){ .r = r, .h = h });
}
static void
Hacl_Standalone_Poly1305_64_poly1305_blocks(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *m,
uint64_t len1
)
{
if (len1 == (uint64_t )0)
{
}
else
{
uint8_t *block = m;
uint8_t *tail1 = m + (uint32_t )16;
Hacl_Impl_Poly1305_64_poly1305_update(st, block);
uint64_t len2 = len1 - (uint64_t )1;
Hacl_Standalone_Poly1305_64_poly1305_blocks(st, tail1, len2);
}
}
static void
Hacl_Standalone_Poly1305_64_poly1305_partial(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *input,
uint64_t len1,
uint8_t *kr
)
{
Hacl_Impl_Poly1305_64_State_poly1305_state scrut = st;
uint64_t *r = scrut.r;
uint64_t *x0 = r;
FStar_UInt128_t k1 = load128_le(kr);
FStar_UInt128_t
k_clamped =
FStar_UInt128_logand(k1,
FStar_UInt128_logor(FStar_UInt128_shift_left(FStar_Int_Cast_Full_uint64_to_uint128((uint64_t )0x0ffffffc0ffffffc),
(uint32_t )64),
FStar_Int_Cast_Full_uint64_to_uint128((uint64_t )0x0ffffffc0fffffff)));
uint64_t r0 = FStar_Int_Cast_Full_uint128_to_uint64(k_clamped) & (uint64_t )0xfffffffffff;
uint64_t
r1 =
FStar_Int_Cast_Full_uint128_to_uint64(FStar_UInt128_shift_right(k_clamped, (uint32_t )44))
& (uint64_t )0xfffffffffff;
uint64_t
r2 = FStar_Int_Cast_Full_uint128_to_uint64(FStar_UInt128_shift_right(k_clamped, (uint32_t )88));
x0[0] = r0;
x0[1] = r1;
x0[2] = r2;
Hacl_Impl_Poly1305_64_State_poly1305_state scrut0 = st;
uint64_t *h = scrut0.h;
uint64_t *x00 = h;
x00[0] = (uint64_t )0;
x00[1] = (uint64_t )0;
x00[2] = (uint64_t )0;
Hacl_Standalone_Poly1305_64_poly1305_blocks(st, input, len1);
}
Prims_nat AEAD_Poly1305_64_seval(void *b)
{
printf("KreMLin abort at %s:%d\n%s\n", __FILE__, __LINE__, "noextract flag");
exit(255);
}
Prims_int AEAD_Poly1305_64_selem(void *s)
{
printf("KreMLin abort at %s:%d\n%s\n", __FILE__, __LINE__, "noextract flag");
exit(255);
}
Hacl_Impl_Poly1305_64_State_poly1305_state
AEAD_Poly1305_64_mk_state(uint64_t *r, uint64_t *acc)
{
return Hacl_Impl_Poly1305_64_mk_state(r, acc);
}
uint32_t AEAD_Poly1305_64_mul_div_16(uint32_t len1)
{
return (uint32_t )16 * (len1 >> (uint32_t )4);
}
void
AEAD_Poly1305_64_pad_last(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *input,
uint32_t len1
)
{
uint8_t b[16];
if (len1 == (uint32_t )0)
{
}
else
{
memset(b, 0, (uint32_t )16 * sizeof b[0]);
memcpy(b, input, len1 * sizeof input[0]);
uint8_t *b0 = b;
Hacl_Impl_Poly1305_64_poly1305_update(st, b0);
}
}
void
AEAD_Poly1305_64_poly1305_blocks_init(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *input,
uint32_t len1,
uint8_t *k1
)
{
uint32_t len_16 = len1 >> (uint32_t )4;
uint32_t rem_16 = len1 & (uint32_t )15;
uint8_t *kr = k1;
uint32_t len_ = (uint32_t )16 * (len1 >> (uint32_t )4);
uint8_t *part_input = input;
uint8_t *last_block = input + len_;
Hacl_Standalone_Poly1305_64_poly1305_partial(st, part_input, (uint64_t )len_16, kr);
AEAD_Poly1305_64_pad_last(st, last_block, rem_16);
}
void
AEAD_Poly1305_64_poly1305_blocks_continue(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *input,
uint32_t len1
)
{
uint32_t len_16 = len1 >> (uint32_t )4;
uint32_t rem_16 = len1 & (uint32_t )15;
uint32_t len_ = (uint32_t )16 * (len1 >> (uint32_t )4);
uint8_t *part_input = input;
uint8_t *last_block = input + len_;
Hacl_Standalone_Poly1305_64_poly1305_blocks(st, part_input, (uint64_t )len_16);
AEAD_Poly1305_64_pad_last(st, last_block, rem_16);
}
void
AEAD_Poly1305_64_poly1305_blocks_finish_(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *input
)
{
Hacl_Impl_Poly1305_64_poly1305_update(st, input);
uint8_t *x2 = input + (uint32_t )16;
if ((uint64_t )0 == (uint64_t )0)
{
}
else
Hacl_Impl_Poly1305_64_poly1305_process_last_block(st, x2, (uint64_t )0);
Hacl_Impl_Poly1305_64_State_poly1305_state scrut = st;
uint64_t *h = scrut.h;
uint64_t *acc = h;
Hacl_Impl_Poly1305_64_poly1305_last_pass(acc);
}
void
AEAD_Poly1305_64_poly1305_blocks_finish(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *input,
uint8_t *mac,
uint8_t *key_s
)
{
Hacl_Impl_Poly1305_64_poly1305_update(st, input);
uint8_t *x2 = input + (uint32_t )16;
if ((uint64_t )0 == (uint64_t )0)
{
}
else
Hacl_Impl_Poly1305_64_poly1305_process_last_block(st, x2, (uint64_t )0);
Hacl_Impl_Poly1305_64_State_poly1305_state scrut = st;
uint64_t *h = scrut.h;
uint64_t *acc = h;
Hacl_Impl_Poly1305_64_poly1305_last_pass(acc);
Hacl_Impl_Poly1305_64_State_poly1305_state scrut0 = st;
uint64_t *h3 = scrut0.h;
uint64_t *acc0 = h3;
FStar_UInt128_t k_ = load128_le(key_s);
uint64_t h0 = acc0[0];
uint64_t h1 = acc0[1];
uint64_t h2 = acc0[2];
FStar_UInt128_t
acc_ =
FStar_UInt128_logor(FStar_UInt128_shift_left(FStar_Int_Cast_Full_uint64_to_uint128(h2
<< (uint32_t )24
| h1 >> (uint32_t )20),
(uint32_t )64),
FStar_Int_Cast_Full_uint64_to_uint128(h1 << (uint32_t )44 | h0));
FStar_UInt128_t mac_ = FStar_UInt128_add_mod(acc_, k_);
store128_le(mac, mac_);
}
sw/airborne/modules/datalink/hacl-c/AEAD_Poly1305_64.h
+101
View File
@@ -0,0 +1,101 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __AEAD_Poly1305_64_H
#define __AEAD_Poly1305_64_H
#include "testlib.h"
typedef uint64_t Hacl_Bignum_Constants_limb;
typedef FStar_UInt128_t Hacl_Bignum_Constants_wide;
typedef FStar_UInt128_t Hacl_Bignum_Wide_t;
typedef uint64_t Hacl_Bignum_Limb_t;
typedef void *Hacl_Impl_Poly1305_64_State_log_t;
typedef uint8_t *Hacl_Impl_Poly1305_64_State_uint8_p;
typedef uint64_t *Hacl_Impl_Poly1305_64_State_bigint;
typedef void *Hacl_Impl_Poly1305_64_State_seqelem;
typedef uint64_t *Hacl_Impl_Poly1305_64_State_elemB;
typedef uint8_t *Hacl_Impl_Poly1305_64_State_wordB;
typedef uint8_t *Hacl_Impl_Poly1305_64_State_wordB_16;
typedef struct
{
uint64_t *r;
uint64_t *h;
}
Hacl_Impl_Poly1305_64_State_poly1305_state;
typedef void *Hacl_Impl_Poly1305_64_log_t;
typedef uint64_t *Hacl_Impl_Poly1305_64_bigint;
typedef uint8_t *Hacl_Impl_Poly1305_64_uint8_p;
typedef uint64_t *Hacl_Impl_Poly1305_64_elemB;
typedef uint8_t *Hacl_Impl_Poly1305_64_wordB;
typedef uint8_t *Hacl_Impl_Poly1305_64_wordB_16;
typedef uint8_t *AEAD_Poly1305_64_uint8_p;
typedef uint8_t *AEAD_Poly1305_64_key;
Prims_nat AEAD_Poly1305_64_seval(void *b);
Prims_int AEAD_Poly1305_64_selem(void *s);
typedef Hacl_Impl_Poly1305_64_State_poly1305_state AEAD_Poly1305_64_state;
Hacl_Impl_Poly1305_64_State_poly1305_state
AEAD_Poly1305_64_mk_state(uint64_t *r, uint64_t *acc);
uint32_t AEAD_Poly1305_64_mul_div_16(uint32_t len1);
void
AEAD_Poly1305_64_pad_last(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *input,
uint32_t len1
);
void
AEAD_Poly1305_64_poly1305_blocks_init(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *input,
uint32_t len1,
uint8_t *k1
);
void
AEAD_Poly1305_64_poly1305_blocks_continue(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *input,
uint32_t len1
);
void
AEAD_Poly1305_64_poly1305_blocks_finish_(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *input
);
void
AEAD_Poly1305_64_poly1305_blocks_finish(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *input,
uint8_t *mac,
uint8_t *key_s
);
#endif
sw/airborne/modules/datalink/hacl-c/Chacha20.c
+246
View File
@@ -0,0 +1,246 @@
#include "Chacha20.h"
static void
Hacl_Lib_LoadStore32_uint32s_from_le_bytes(uint32_t *output, uint8_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t *x0 = input + (uint32_t )4 * i;
uint32_t inputi = load32_le(x0);
output[i] = inputi;
}
}
static void
Hacl_Lib_LoadStore32_uint32s_to_le_bytes(uint8_t *output, uint32_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint32_t hd1 = input[i];
uint8_t *x0 = output + (uint32_t )4 * i;
store32_le(x0, hd1);
}
}
inline static void Hacl_Impl_Chacha20_setup(uint32_t *st, uint8_t *k, uint8_t *n1, uint32_t c)
{
uint32_t *stcst = st;
uint32_t *stk = st + (uint32_t )4;
uint32_t *stc = st + (uint32_t )12;
uint32_t *stn = st + (uint32_t )13;
stcst[0] = (uint32_t )0x61707865;
stcst[1] = (uint32_t )0x3320646e;
stcst[2] = (uint32_t )0x79622d32;
stcst[3] = (uint32_t )0x6b206574;
Hacl_Lib_LoadStore32_uint32s_from_le_bytes(stk, k, (uint32_t )8);
stc[0] = c;
Hacl_Lib_LoadStore32_uint32s_from_le_bytes(stn, n1, (uint32_t )3);
}
inline static void
Hacl_Impl_Chacha20_quarter_round(uint32_t *st, uint32_t a, uint32_t b, uint32_t c, uint32_t d)
{
uint32_t sa = st[a];
uint32_t sb0 = st[b];
st[a] = sa + sb0;
uint32_t sd = st[d];
uint32_t sa10 = st[a];
uint32_t sda = sd ^ sa10;
st[d] = sda << (uint32_t )16 | sda >> (uint32_t )32 - (uint32_t )16;
uint32_t sa0 = st[c];
uint32_t sb1 = st[d];
st[c] = sa0 + sb1;
uint32_t sd0 = st[b];
uint32_t sa11 = st[c];
uint32_t sda0 = sd0 ^ sa11;
st[b] = sda0 << (uint32_t )12 | sda0 >> (uint32_t )32 - (uint32_t )12;
uint32_t sa2 = st[a];
uint32_t sb2 = st[b];
st[a] = sa2 + sb2;
uint32_t sd1 = st[d];
uint32_t sa12 = st[a];
uint32_t sda1 = sd1 ^ sa12;
st[d] = sda1 << (uint32_t )8 | sda1 >> (uint32_t )32 - (uint32_t )8;
uint32_t sa3 = st[c];
uint32_t sb = st[d];
st[c] = sa3 + sb;
uint32_t sd2 = st[b];
uint32_t sa1 = st[c];
uint32_t sda2 = sd2 ^ sa1;
st[b] = sda2 << (uint32_t )7 | sda2 >> (uint32_t )32 - (uint32_t )7;
}
inline static void Hacl_Impl_Chacha20_double_round(uint32_t *st)
{
Hacl_Impl_Chacha20_quarter_round(st, (uint32_t )0, (uint32_t )4, (uint32_t )8, (uint32_t )12);
Hacl_Impl_Chacha20_quarter_round(st, (uint32_t )1, (uint32_t )5, (uint32_t )9, (uint32_t )13);
Hacl_Impl_Chacha20_quarter_round(st, (uint32_t )2, (uint32_t )6, (uint32_t )10, (uint32_t )14);
Hacl_Impl_Chacha20_quarter_round(st, (uint32_t )3, (uint32_t )7, (uint32_t )11, (uint32_t )15);
Hacl_Impl_Chacha20_quarter_round(st, (uint32_t )0, (uint32_t )5, (uint32_t )10, (uint32_t )15);
Hacl_Impl_Chacha20_quarter_round(st, (uint32_t )1, (uint32_t )6, (uint32_t )11, (uint32_t )12);
Hacl_Impl_Chacha20_quarter_round(st, (uint32_t )2, (uint32_t )7, (uint32_t )8, (uint32_t )13);
Hacl_Impl_Chacha20_quarter_round(st, (uint32_t )3, (uint32_t )4, (uint32_t )9, (uint32_t )14);
}
inline static void Hacl_Impl_Chacha20_rounds(uint32_t *st)
{
for (uint32_t i = (uint32_t )0; i < (uint32_t )10; i = i + (uint32_t )1)
Hacl_Impl_Chacha20_double_round(st);
}
inline static void Hacl_Impl_Chacha20_sum_states(uint32_t *st, uint32_t *st_)
{
for (uint32_t i = (uint32_t )0; i < (uint32_t )16; i = i + (uint32_t )1)
{
uint32_t uu____871 = st[i];
uint32_t uu____874 = st_[i];
uint32_t uu____870 = uu____871 + uu____874;
st[i] = uu____870;
}
}
inline static void Hacl_Impl_Chacha20_copy_state(uint32_t *st, uint32_t *st_)
{
memcpy(st, st_, (uint32_t )16 * sizeof st_[0]);
}
inline static void Hacl_Impl_Chacha20_chacha20_core(uint32_t *k, uint32_t *st, uint32_t ctr)
{
st[12] = ctr;
Hacl_Impl_Chacha20_copy_state(k, st);
Hacl_Impl_Chacha20_rounds(k);
Hacl_Impl_Chacha20_sum_states(k, st);
}
inline static void
Hacl_Impl_Chacha20_chacha20_block(uint8_t *stream_block, uint32_t *st, uint32_t ctr)
{
uint32_t st_[16] = { 0 };
Hacl_Impl_Chacha20_chacha20_core(st_, st, ctr);
Hacl_Lib_LoadStore32_uint32s_to_le_bytes(stream_block, st_, (uint32_t )16);
}
inline static void Hacl_Impl_Chacha20_init(uint32_t *st, uint8_t *k, uint8_t *n1)
{
Hacl_Impl_Chacha20_setup(st, k, n1, (uint32_t )0);
}
static void
Hacl_Impl_Chacha20_update_last(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint32_t *st,
uint32_t ctr
)
{
uint8_t block[64] = { 0 };
Hacl_Impl_Chacha20_chacha20_block(block, st, ctr);
uint8_t *mask = block;
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t uu____602 = plain[i];
uint8_t uu____605 = mask[i];
uint8_t uu____601 = uu____602 ^ uu____605;
output[i] = uu____601;
}
}
static void
Hacl_Impl_Chacha20_update(uint8_t *output, uint8_t *plain, uint32_t *st, uint32_t ctr)
{
uint32_t b[48] = { 0 };
uint32_t *k = b;
uint32_t *ib = b + (uint32_t )16;
uint32_t *ob = b + (uint32_t )32;
Hacl_Impl_Chacha20_chacha20_core(k, st, ctr);
Hacl_Lib_LoadStore32_uint32s_from_le_bytes(ib, plain, (uint32_t )16);
for (uint32_t i = (uint32_t )0; i < (uint32_t )16; i = i + (uint32_t )1)
{
uint32_t uu____602 = ib[i];
uint32_t uu____605 = k[i];
uint32_t uu____601 = uu____602 ^ uu____605;
ob[i] = uu____601;
}
Hacl_Lib_LoadStore32_uint32s_to_le_bytes(output, ob, (uint32_t )16);
}
static void
Hacl_Impl_Chacha20_chacha20_counter_mode_blocks(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint32_t *st,
uint32_t ctr
)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t *b = plain + (uint32_t )64 * i;
uint8_t *o = output + (uint32_t )64 * i;
Hacl_Impl_Chacha20_update(o, b, st, ctr + i);
}
}
static void
Hacl_Impl_Chacha20_chacha20_counter_mode(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint32_t *st,
uint32_t ctr
)
{
uint32_t blocks_len = len >> (uint32_t )6;
uint32_t part_len = len & (uint32_t )0x3f;
uint8_t *output_ = output;
uint8_t *plain_ = plain;
uint8_t *output__ = output + (uint32_t )64 * blocks_len;
uint8_t *plain__ = plain + (uint32_t )64 * blocks_len;
Hacl_Impl_Chacha20_chacha20_counter_mode_blocks(output_, plain_, blocks_len, st, ctr);
if (part_len > (uint32_t )0)
Hacl_Impl_Chacha20_update_last(output__, plain__, part_len, st, ctr + blocks_len);
}
static void
Hacl_Impl_Chacha20_chacha20(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint8_t *k,
uint8_t *n1,
uint32_t ctr
)
{
uint32_t buf[16] = { 0 };
uint32_t *st = buf;
Hacl_Impl_Chacha20_init(st, k, n1);
Hacl_Impl_Chacha20_chacha20_counter_mode(output, plain, len, st, ctr);
}
void *Chacha20_op_String_Access(FStar_Monotonic_HyperStack_mem h, uint8_t *m)
{
return (void *)(uint8_t )0;
}
void Chacha20_chacha20_key_block(uint8_t *block, uint8_t *k, uint8_t *n1, uint32_t ctr)
{
uint32_t buf[16] = { 0 };
uint32_t *st = buf;
Hacl_Impl_Chacha20_init(st, k, n1);
Hacl_Impl_Chacha20_chacha20_block(block, st, ctr);
}
void
Chacha20_chacha20(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint8_t *k,
uint8_t *n1,
uint32_t ctr
)
{
Hacl_Impl_Chacha20_chacha20(output, plain, len, k, n1, ctr);
}
sw/airborne/modules/datalink/hacl-c/Chacha20.h
+54
View File
@@ -0,0 +1,54 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __Chacha20_H
#define __Chacha20_H
#include "testlib.h"
typedef uint32_t Hacl_Impl_Xor_Lemmas_u32;
typedef uint8_t Hacl_Impl_Xor_Lemmas_u8;
typedef uint8_t *Hacl_Lib_LoadStore32_uint8_p;
typedef uint32_t Hacl_Impl_Chacha20_u32;
typedef uint32_t Hacl_Impl_Chacha20_h32;
typedef uint8_t *Hacl_Impl_Chacha20_uint8_p;
typedef uint32_t *Hacl_Impl_Chacha20_state;
typedef uint32_t Hacl_Impl_Chacha20_idx;
typedef struct
{
void *k;
void *n;
}
Hacl_Impl_Chacha20_log_t_;
typedef void *Hacl_Impl_Chacha20_log_t;
typedef uint32_t Hacl_Lib_Create_h32;
typedef uint8_t *Chacha20_uint8_p;
typedef uint32_t Chacha20_uint32_t;
void *Chacha20_op_String_Access(FStar_Monotonic_HyperStack_mem h, uint8_t *m);
void Chacha20_chacha20_key_block(uint8_t *block, uint8_t *k, uint8_t *n1, uint32_t ctr);
void
Chacha20_chacha20(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint8_t *k,
uint8_t *n1,
uint32_t ctr
);
#endif
sw/airborne/modules/datalink/hacl-c/Chacha20Poly1305.c
+109
View File
@@ -0,0 +1,109 @@
#include "Chacha20Poly1305.h"
Prims_int Chacha20Poly1305_noncelen;
Prims_int Chacha20Poly1305_keylen;
Prims_int Chacha20Poly1305_maclen;
static void
Chacha20Poly1305_aead_encrypt_poly(
uint8_t *c,
uint32_t mlen,
uint8_t *mac,
uint8_t *aad1,
uint32_t aadlen,
uint8_t *tmp
)
{
uint8_t *b = tmp;
uint8_t *lb = tmp + (uint32_t )64;
uint8_t *mk = b;
uint8_t *key_s = mk + (uint32_t )16;
uint64_t tmp1[6] = { 0 };
Hacl_Impl_Poly1305_64_State_poly1305_state
st = AEAD_Poly1305_64_mk_state(tmp1, tmp1 + (uint32_t )3);
(void )AEAD_Poly1305_64_poly1305_blocks_init(st, aad1, aadlen, mk);
(void )AEAD_Poly1305_64_poly1305_blocks_continue(st, c, mlen);
AEAD_Poly1305_64_poly1305_blocks_finish(st, lb, mac, key_s);
}
void Chacha20Poly1305_encode_length(uint8_t *lb, uint32_t aad_len, uint32_t mlen)
{
store64_le(lb, (uint64_t )aad_len);
uint8_t *x0 = lb + (uint32_t )8;
store64_le(x0, (uint64_t )mlen);
}
uint32_t
Chacha20Poly1305_aead_encrypt_(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint32_t mlen,
uint8_t *aad1,
uint32_t aadlen,
uint8_t *k1,
uint8_t *n1
)
{
uint8_t tmp[80] = { 0 };
uint8_t *b = tmp;
uint8_t *lb = tmp + (uint32_t )64;
Chacha20Poly1305_encode_length(lb, aadlen, mlen);
Chacha20_chacha20(c, m, mlen, k1, n1, (uint32_t )1);
Chacha20_chacha20_key_block(b, k1, n1, (uint32_t )0);
Chacha20Poly1305_aead_encrypt_poly(c, mlen, mac, aad1, aadlen, tmp);
return (uint32_t )0;
}
uint32_t
Chacha20Poly1305_aead_encrypt(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint32_t mlen,
uint8_t *aad1,
uint32_t aadlen,
uint8_t *k1,
uint8_t *n1
)
{
uint32_t z = Chacha20Poly1305_aead_encrypt_(c, mac, m, mlen, aad1, aadlen, k1, n1);
return z;
}
uint32_t
Chacha20Poly1305_aead_decrypt(
uint8_t *m,
uint8_t *c,
uint32_t mlen,
uint8_t *mac,
uint8_t *aad1,
uint32_t aadlen,
uint8_t *k1,
uint8_t *n1
)
{
uint8_t tmp[96] = { 0 };
uint8_t *b = tmp;
uint8_t *lb = tmp + (uint32_t )64;
Chacha20Poly1305_encode_length(lb, aadlen, mlen);
uint8_t *rmac = tmp + (uint32_t )80;
Chacha20_chacha20_key_block(b, k1, n1, (uint32_t )0);
uint8_t *mk = b;
(void )(mk + (uint32_t )16);
Chacha20Poly1305_aead_encrypt_poly(c, mlen, rmac, aad1, aadlen, tmp);
uint8_t result = Hacl_Policies_cmp_bytes(mac, rmac, (uint32_t )16);
uint8_t verify = result;
uint32_t res;
if (verify == (uint8_t )0)
{
Chacha20_chacha20(m, c, mlen, k1, n1, (uint32_t )1);
res = (uint32_t )0;
}
else
res = (uint32_t )1;
return res;
}
sw/airborne/modules/datalink/hacl-c/Chacha20Poly1305.h
+58
View File
@@ -0,0 +1,58 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __Chacha20Poly1305_H
#define __Chacha20Poly1305_H
#include "Hacl_Policies.h"
#include "Chacha20.h"
#include "AEAD_Poly1305_64.h"
extern Prims_int Chacha20Poly1305_noncelen;
extern Prims_int Chacha20Poly1305_keylen;
extern Prims_int Chacha20Poly1305_maclen;
typedef Hacl_Impl_Poly1305_64_State_poly1305_state Chacha20Poly1305_state;
typedef void *Chacha20Poly1305_log_t;
void Chacha20Poly1305_encode_length(uint8_t *lb, uint32_t aad_len, uint32_t mlen);
uint32_t
Chacha20Poly1305_aead_encrypt_(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint32_t mlen,
uint8_t *aad1,
uint32_t aadlen,
uint8_t *k1,
uint8_t *n1
);
uint32_t
Chacha20Poly1305_aead_encrypt(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint32_t mlen,
uint8_t *aad1,
uint32_t aadlen,
uint8_t *k1,
uint8_t *n1
);
uint32_t
Chacha20Poly1305_aead_decrypt(
uint8_t *m,
uint8_t *c,
uint32_t mlen,
uint8_t *mac,
uint8_t *aad1,
uint32_t aadlen,
uint8_t *k1,
uint8_t *n1
);
#endif
sw/airborne/modules/datalink/hacl-c/Chacha20_Vec128.c
+371
View File
@@ -0,0 +1,371 @@
#include "Chacha20_Vec128.h"
inline static void Hacl_Impl_Chacha20_Vec128_State_state_incr(vec *k)
{
vec k3 = k[3];
k[3] = vec_add(k3, one_le);
}
inline static void
Hacl_Impl_Chacha20_Vec128_State_state_to_key_block(uint8_t *stream_block, vec *k)
{
vec k0 = k[0];
vec k1 = k[1];
vec k2 = k[2];
vec k3 = k[3];
uint8_t *a = stream_block;
uint8_t *b = stream_block + (uint32_t )16;
uint8_t *c = stream_block + (uint32_t )32;
uint8_t *d = stream_block + (uint32_t )48;
vec_store_le(a, k0);
vec_store_le(b, k1);
vec_store_le(c, k2);
vec_store_le(d, k3);
}
inline static void
Hacl_Impl_Chacha20_Vec128_State_state_setup(vec *st, uint8_t *k, uint8_t *n1, uint32_t c)
{
st[0] =
vec_load_32x4((uint32_t )0x61707865,
(uint32_t )0x3320646e,
(uint32_t )0x79622d32,
(uint32_t )0x6b206574);
vec k0 = vec_load128_le(k);
vec k1 = vec_load128_le(k + (uint32_t )16);
st[1] = k0;
st[2] = k1;
uint32_t n0 = load32_le(n1);
uint8_t *x00 = n1 + (uint32_t )4;
uint32_t n10 = load32_le(x00);
uint8_t *x0 = n1 + (uint32_t )8;
uint32_t n2 = load32_le(x0);
vec v1 = vec_load_32x4(c, n0, n10, n2);
st[3] = v1;
}
inline static void
Hacl_Impl_Chacha20_Vec128_line(vec *st, uint32_t a, uint32_t b, uint32_t d, uint32_t s)
{
vec sa = st[a];
vec sb = st[b];
vec sd = st[d];
vec sa1 = vec_add(sa, sb);
vec sd1 = vec_rotate_left(vec_xor(sd, sa1), s);
st[a] = sa1;
st[d] = sd1;
}
inline static void Hacl_Impl_Chacha20_Vec128_round(vec *st)
{
Hacl_Impl_Chacha20_Vec128_line(st, (uint32_t )0, (uint32_t )1, (uint32_t )3, (uint32_t )16);
Hacl_Impl_Chacha20_Vec128_line(st, (uint32_t )2, (uint32_t )3, (uint32_t )1, (uint32_t )12);
Hacl_Impl_Chacha20_Vec128_line(st, (uint32_t )0, (uint32_t )1, (uint32_t )3, (uint32_t )8);
Hacl_Impl_Chacha20_Vec128_line(st, (uint32_t )2, (uint32_t )3, (uint32_t )1, (uint32_t )7);
}
inline static void Hacl_Impl_Chacha20_Vec128_double_round(vec *st)
{
Hacl_Impl_Chacha20_Vec128_round(st);
vec r1 = st[1];
vec r20 = st[2];
vec r30 = st[3];
st[1] = vec_shuffle_right(r1, (uint32_t )1);
st[2] = vec_shuffle_right(r20, (uint32_t )2);
st[3] = vec_shuffle_right(r30, (uint32_t )3);
Hacl_Impl_Chacha20_Vec128_round(st);
vec r10 = st[1];
vec r2 = st[2];
vec r3 = st[3];
st[1] = vec_shuffle_right(r10, (uint32_t )3);
st[2] = vec_shuffle_right(r2, (uint32_t )2);
st[3] = vec_shuffle_right(r3, (uint32_t )1);
}
inline static void Hacl_Impl_Chacha20_Vec128_double_round3(vec *st, vec *st_, vec *st__)
{
Hacl_Impl_Chacha20_Vec128_double_round(st);
Hacl_Impl_Chacha20_Vec128_double_round(st_);
Hacl_Impl_Chacha20_Vec128_double_round(st__);
}
inline static void Hacl_Impl_Chacha20_Vec128_sum_states(vec *st_, vec *st)
{
vec s0 = st[0];
vec s1 = st[1];
vec s2 = st[2];
vec s3 = st[3];
vec s0_ = st_[0];
vec s1_ = st_[1];
vec s2_ = st_[2];
vec s3_ = st_[3];
st_[0] = vec_add(s0_, s0);
st_[1] = vec_add(s1_, s1);
st_[2] = vec_add(s2_, s2);
st_[3] = vec_add(s3_, s3);
}
inline static void Hacl_Impl_Chacha20_Vec128_copy_state(vec *st_, vec *st)
{
vec uu____3478 = st[0];
st_[0] = uu____3478;
vec uu____3520 = st[1];
st_[1] = uu____3520;
vec uu____3562 = st[2];
st_[2] = uu____3562;
vec uu____3604 = st[3];
st_[3] = uu____3604;
}
inline static void Hacl_Impl_Chacha20_Vec128_chacha20_core(vec *k, vec *st)
{
Hacl_Impl_Chacha20_Vec128_copy_state(k, st);
for (uint32_t i = (uint32_t )0; i < (uint32_t )10; i = i + (uint32_t )1)
Hacl_Impl_Chacha20_Vec128_double_round(k);
Hacl_Impl_Chacha20_Vec128_sum_states(k, st);
}
static void Hacl_Impl_Chacha20_Vec128_state_incr(vec *st)
{
Hacl_Impl_Chacha20_Vec128_State_state_incr(st);
}
inline static void Hacl_Impl_Chacha20_Vec128_chacha20_incr3(vec *k0, vec *k1, vec *k2, vec *st)
{
Hacl_Impl_Chacha20_Vec128_copy_state(k0, st);
Hacl_Impl_Chacha20_Vec128_copy_state(k1, st);
Hacl_Impl_Chacha20_Vec128_state_incr(k1);
Hacl_Impl_Chacha20_Vec128_copy_state(k2, k1);
Hacl_Impl_Chacha20_Vec128_state_incr(k2);
}
inline static void Hacl_Impl_Chacha20_Vec128_chacha20_sum3(vec *k0, vec *k1, vec *k2, vec *st)
{
Hacl_Impl_Chacha20_Vec128_sum_states(k0, st);
Hacl_Impl_Chacha20_Vec128_state_incr(st);
Hacl_Impl_Chacha20_Vec128_sum_states(k1, st);
Hacl_Impl_Chacha20_Vec128_state_incr(st);
Hacl_Impl_Chacha20_Vec128_sum_states(k2, st);
}
inline static void Hacl_Impl_Chacha20_Vec128_chacha20_core3(vec *k0, vec *k1, vec *k2, vec *st)
{
Hacl_Impl_Chacha20_Vec128_chacha20_incr3(k0, k1, k2, st);
for (uint32_t i = (uint32_t )0; i < (uint32_t )10; i = i + (uint32_t )1)
Hacl_Impl_Chacha20_Vec128_double_round3(k0, k1, k2);
Hacl_Impl_Chacha20_Vec128_chacha20_sum3(k0, k1, k2, st);
}
inline static void Hacl_Impl_Chacha20_Vec128_chacha20_block(uint8_t *stream_block, vec *st)
{
KRML_CHECK_SIZE(zero, (uint32_t )4);
vec k[4];
for (uintmax_t _i = 0; _i < (uint32_t )4; ++_i)
k[_i] = zero;
Hacl_Impl_Chacha20_Vec128_chacha20_core(k, st);
Hacl_Impl_Chacha20_Vec128_State_state_to_key_block(stream_block, k);
}
inline static void
Hacl_Impl_Chacha20_Vec128_init(vec *st, uint8_t *k, uint8_t *n1, uint32_t ctr)
{
Hacl_Impl_Chacha20_Vec128_State_state_setup(st, k, n1, ctr);
}
static void
Hacl_Impl_Chacha20_Vec128_update_last(uint8_t *output, uint8_t *plain, uint32_t len, vec *st)
{
uint8_t block[64] = { 0 };
Hacl_Impl_Chacha20_Vec128_chacha20_block(block, st);
uint8_t *mask = block;
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t uu____602 = plain[i];
uint8_t uu____605 = mask[i];
uint8_t uu____601 = uu____602 ^ uu____605;
output[i] = uu____601;
}
}
static void
Hacl_Impl_Chacha20_Vec128_store_4_vec(uint8_t *output, vec v0, vec v1, vec v2, vec v3)
{
uint8_t *o0 = output;
uint8_t *o1 = output + (uint32_t )16;
uint8_t *o2 = output + (uint32_t )32;
uint8_t *o3 = output + (uint32_t )48;
vec_store_le(o0, v0);
vec_store_le(o1, v1);
vec_store_le(o2, v2);
vec_store_le(o3, v3);
}
static void Hacl_Impl_Chacha20_Vec128_xor_block(uint8_t *output, uint8_t *plain, vec *st)
{
vec p0 = vec_load_le(plain);
vec p1 = vec_load_le(plain + (uint32_t )16);
vec p2 = vec_load_le(plain + (uint32_t )32);
vec p3 = vec_load_le(plain + (uint32_t )48);
vec k0 = st[0];
vec k1 = st[1];
vec k2 = st[2];
vec k3 = st[3];
vec o0 = vec_xor(p0, k0);
vec o1 = vec_xor(p1, k1);
vec o2 = vec_xor(p2, k2);
vec o3 = vec_xor(p3, k3);
Hacl_Impl_Chacha20_Vec128_store_4_vec(output, o0, o1, o2, o3);
}
static void Hacl_Impl_Chacha20_Vec128_update(uint8_t *output, uint8_t *plain, vec *st)
{
KRML_CHECK_SIZE(zero, (uint32_t )4);
vec k[4];
for (uintmax_t _i = 0; _i < (uint32_t )4; ++_i)
k[_i] = zero;
Hacl_Impl_Chacha20_Vec128_chacha20_core(k, st);
Hacl_Impl_Chacha20_Vec128_xor_block(output, plain, k);
}
static void Hacl_Impl_Chacha20_Vec128_update3(uint8_t *output, uint8_t *plain, vec *st)
{
KRML_CHECK_SIZE(zero, (uint32_t )4);
vec k0[4];
for (uintmax_t _i = 0; _i < (uint32_t )4; ++_i)
k0[_i] = zero;
KRML_CHECK_SIZE(zero, (uint32_t )4);
vec k1[4];
for (uintmax_t _i = 0; _i < (uint32_t )4; ++_i)
k1[_i] = zero;
KRML_CHECK_SIZE(zero, (uint32_t )4);
vec k2[4];
for (uintmax_t _i = 0; _i < (uint32_t )4; ++_i)
k2[_i] = zero;
Hacl_Impl_Chacha20_Vec128_chacha20_core3(k0, k1, k2, st);
uint8_t *p0 = plain;
uint8_t *p1 = plain + (uint32_t )64;
uint8_t *p2 = plain + (uint32_t )128;
uint8_t *o0 = output;
uint8_t *o1 = output + (uint32_t )64;
uint8_t *o2 = output + (uint32_t )128;
Hacl_Impl_Chacha20_Vec128_xor_block(o0, p0, k0);
Hacl_Impl_Chacha20_Vec128_xor_block(o1, p1, k1);
Hacl_Impl_Chacha20_Vec128_xor_block(o2, p2, k2);
}
static void
Hacl_Impl_Chacha20_Vec128_update3_(
uint8_t *output,
uint8_t *plain,
uint32_t len,
vec *st,
uint32_t i
)
{
uint8_t *out_block = output + (uint32_t )192 * i;
uint8_t *plain_block = plain + (uint32_t )192 * i;
Hacl_Impl_Chacha20_Vec128_update3(out_block, plain_block, st);
Hacl_Impl_Chacha20_Vec128_state_incr(st);
}
static void
Hacl_Impl_Chacha20_Vec128_chacha20_counter_mode_blocks3(
uint8_t *output,
uint8_t *plain,
uint32_t len,
vec *st
)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
Hacl_Impl_Chacha20_Vec128_update3_(output, plain, len, st, i);
}
static void
Hacl_Impl_Chacha20_Vec128_chacha20_counter_mode_blocks(
uint8_t *output,
uint8_t *plain,
uint32_t len,
vec *st
)
{
uint32_t len3 = len / (uint32_t )3;
uint32_t rest3 = len % (uint32_t )3;
uint8_t *plain_ = plain;
uint8_t *blocks1 = plain + (uint32_t )192 * len3;
uint8_t *output_ = output;
uint8_t *outs = output + (uint32_t )192 * len3;
Hacl_Impl_Chacha20_Vec128_chacha20_counter_mode_blocks3(output_, plain_, len3, st);
if (rest3 == (uint32_t )2)
{
uint8_t *block0 = blocks1;
uint8_t *block1 = blocks1 + (uint32_t )64;
uint8_t *out0 = outs;
uint8_t *out1 = outs + (uint32_t )64;
Hacl_Impl_Chacha20_Vec128_update(out0, block0, st);
Hacl_Impl_Chacha20_Vec128_state_incr(st);
Hacl_Impl_Chacha20_Vec128_update(out1, block1, st);
Hacl_Impl_Chacha20_Vec128_state_incr(st);
}
else if (rest3 == (uint32_t )1)
{
Hacl_Impl_Chacha20_Vec128_update(outs, blocks1, st);
Hacl_Impl_Chacha20_Vec128_state_incr(st);
}
}
static void
Hacl_Impl_Chacha20_Vec128_chacha20_counter_mode(
uint8_t *output,
uint8_t *plain,
uint32_t len,
vec *st
)
{
uint32_t blocks_len = len >> (uint32_t )6;
uint32_t part_len = len & (uint32_t )0x3f;
uint8_t *output_ = output;
uint8_t *plain_ = plain;
uint8_t *output__ = output + (uint32_t )64 * blocks_len;
uint8_t *plain__ = plain + (uint32_t )64 * blocks_len;
Hacl_Impl_Chacha20_Vec128_chacha20_counter_mode_blocks(output_, plain_, blocks_len, st);
if (part_len > (uint32_t )0)
Hacl_Impl_Chacha20_Vec128_update_last(output__, plain__, part_len, st);
}
static void
Hacl_Impl_Chacha20_Vec128_chacha20(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint8_t *k,
uint8_t *n1,
uint32_t ctr
)
{
KRML_CHECK_SIZE(zero, (uint32_t )4);
vec buf[4];
for (uintmax_t _i = 0; _i < (uint32_t )4; ++_i)
buf[_i] = zero;
vec *st = buf;
Hacl_Impl_Chacha20_Vec128_init(st, k, n1, ctr);
Hacl_Impl_Chacha20_Vec128_chacha20_counter_mode(output, plain, len, st);
}
void *Chacha20_Vec128_op_String_Access(FStar_Monotonic_HyperStack_mem h, uint8_t *b)
{
return (void *)(uint8_t )0;
}
void
Chacha20_Vec128_chacha20(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint8_t *k,
uint8_t *n1,
uint32_t ctr
)
{
Hacl_Impl_Chacha20_Vec128_chacha20(output, plain, len, k, n1, ctr);
}
sw/airborne/modules/datalink/hacl-c/Chacha20_Vec128.h
+54
View File
@@ -0,0 +1,54 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __Chacha20_Vec128_H
#define __Chacha20_Vec128_H
#include "testlib.h"
#include "vec128.h"
typedef uint32_t Hacl_Impl_Xor_Lemmas_u32;
typedef uint8_t Hacl_Impl_Xor_Lemmas_u8;
typedef uint32_t Hacl_Impl_Chacha20_Vec128_State_u32;
typedef uint32_t Hacl_Impl_Chacha20_Vec128_State_h32;
typedef uint8_t *Hacl_Impl_Chacha20_Vec128_State_uint8_p;
typedef vec *Hacl_Impl_Chacha20_Vec128_State_state;
typedef uint32_t Hacl_Impl_Chacha20_Vec128_u32;
typedef uint32_t Hacl_Impl_Chacha20_Vec128_h32;
typedef uint8_t *Hacl_Impl_Chacha20_Vec128_uint8_p;
typedef uint32_t Hacl_Impl_Chacha20_Vec128_idx;
typedef struct
{
void *k;
void *n;
uint32_t ctr;
}
Hacl_Impl_Chacha20_Vec128_log_t_;
typedef void *Hacl_Impl_Chacha20_Vec128_log_t;
typedef uint8_t *Chacha20_Vec128_uint8_p;
void *Chacha20_Vec128_op_String_Access(FStar_Monotonic_HyperStack_mem h, uint8_t *b);
void
Chacha20_Vec128_chacha20(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint8_t *k,
uint8_t *n1,
uint32_t ctr
);
#endif
sw/airborne/modules/datalink/hacl-c/Curve25519.c
+1000
View File
File diff suppressed because it is too large Load Diff
sw/airborne/modules/datalink/hacl-c/Curve25519.h
+49
View File
@@ -0,0 +1,49 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __Curve25519_H
#define __Curve25519_H
#include "testlib.h"
typedef uint64_t Hacl_Bignum_Constants_limb;
typedef FStar_UInt128_t Hacl_Bignum_Constants_wide;
typedef uint64_t Hacl_Bignum_Parameters_limb;
typedef FStar_UInt128_t Hacl_Bignum_Parameters_wide;
typedef uint32_t Hacl_Bignum_Parameters_ctr;
typedef uint64_t *Hacl_Bignum_Parameters_felem;
typedef FStar_UInt128_t *Hacl_Bignum_Parameters_felem_wide;
typedef void *Hacl_Bignum_Parameters_seqelem;
typedef void *Hacl_Bignum_Parameters_seqelem_wide;
typedef FStar_UInt128_t Hacl_Bignum_Wide_t;
typedef uint64_t Hacl_Bignum_Limb_t;
extern void Hacl_Bignum_lemma_diff(Prims_int x0, Prims_int x1, Prims_pos x2);
typedef uint64_t *Hacl_EC_Point_point;
typedef uint8_t *Hacl_EC_Ladder_SmallLoop_uint8_p;
typedef uint8_t *Hacl_EC_Ladder_uint8_p;
typedef uint8_t *Hacl_EC_Format_uint8_p;
void Hacl_EC_crypto_scalarmult(uint8_t *mypublic, uint8_t *secret, uint8_t *basepoint);
typedef uint8_t *Curve25519_uint8_p;
void *Curve25519_op_String_Access(FStar_Monotonic_HyperStack_mem h, uint8_t *b);
void Curve25519_crypto_scalarmult(uint8_t *mypublic, uint8_t *secret, uint8_t *basepoint);
#endif
sw/airborne/modules/datalink/hacl-c/Ed25519.c
+2987
View File
File diff suppressed because it is too large Load Diff
sw/airborne/modules/datalink/hacl-c/Ed25519.h
+261
View File
@@ -0,0 +1,261 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __Ed25519_H
#define __Ed25519_H
typedef uint64_t Hacl_Lib_Create64_h64;
typedef uint64_t Hacl_Bignum_Constants_limb;
typedef FStar_UInt128_t Hacl_Bignum_Constants_wide;
typedef uint64_t Hacl_Bignum_Parameters_limb;
typedef FStar_UInt128_t Hacl_Bignum_Parameters_wide;
typedef uint32_t Hacl_Bignum_Parameters_ctr;
typedef uint64_t *Hacl_Bignum_Parameters_felem;
typedef FStar_UInt128_t *Hacl_Bignum_Parameters_felem_wide;
typedef void *Hacl_Bignum_Parameters_seqelem;
typedef void *Hacl_Bignum_Parameters_seqelem_wide;
typedef FStar_UInt128_t Hacl_Bignum_Wide_t;
typedef uint64_t Hacl_Bignum_Limb_t;
typedef Prims_int Hacl_Spec_Bignum_Field_elem;
extern void
Hacl_Spec_Bignum_Field_lemma_addition_associativity(Prims_int x0, Prims_int x1, Prims_int x2);
extern void
Hacl_Spec_Bignum_Field_lemma_multiplication_associativity(
Prims_int x0,
Prims_int x1,
Prims_int x2
);
extern void Hacl_Spec_Bignum_Field_lemma_addition_symmetry(Prims_int x0);
extern void Hacl_Spec_Bignum_Field_lemma_multiplication_symmetry(Prims_int x0);
typedef Prims_int Hacl_Spec_Bignum_elem;
typedef void *Hacl_Spec_EC_AddAndDouble2_s_513;
typedef void *Hacl_Spec_EC_AddAndDouble2_s_52;
typedef void *Hacl_Spec_EC_AddAndDouble2_s_53;
typedef void *Hacl_Spec_EC_AddAndDouble2_s_5413;
typedef void *Hacl_Spec_Bignum_Crecip_s_513;
extern void Hacl_Bignum_lemma_diff(Prims_int x0, Prims_int x1, Prims_pos x2);
typedef Prims_nat Hacl_Spec_EC_Format_Lemmas_u51;
typedef struct
{
void *fst;
void *snd;
}
K___FStar_Seq_Base_seq_uint64_t_FStar_Seq_Base_seq_uint64_t;
typedef K___FStar_Seq_Base_seq_uint64_t_FStar_Seq_Base_seq_uint64_t Hacl_Spec_EC_Point_spoint;
typedef void *Hacl_Spec_EC_Point_s_513;
typedef K___FStar_Seq_Base_seq_uint64_t_FStar_Seq_Base_seq_uint64_t
Hacl_Spec_EC_Point_spoint_513;
typedef void *Hacl_Spec_EC_Format_uint8_s;
typedef uint64_t *Hacl_EC_Point_point;
typedef uint8_t *Hacl_EC_Format_uint8_p;
typedef uint64_t Hacl_Bignum25519_limb;
typedef uint64_t *Hacl_Bignum25519_felem;
typedef void *Hacl_Bignum25519_seqelem;
typedef uint64_t *Hacl_Impl_Ed25519_ExtPoint_point;
typedef uint8_t *Hacl_Impl_Store51_uint8_p;
typedef uint64_t *Hacl_Impl_Store51_felem;
typedef uint8_t *Hacl_Impl_Ed25519_PointCompress_hint8_p;
typedef uint64_t *Hacl_Impl_Ed25519_PointCompress_hint64_p;
typedef uint64_t *Hacl_Impl_Ed25519_SwapConditional_felem;
typedef uint8_t *Hacl_Impl_Ed25519_Ladder_Step_uint8_p;
typedef uint64_t *Hacl_Impl_Ed25519_Ladder_elemB;
typedef uint8_t *Hacl_Hash_Lib_LoadStore_uint8_p;
typedef uint8_t Hacl_Hash_Lib_Create_uint8_t;
typedef uint32_t Hacl_Hash_Lib_Create_uint32_t;
typedef uint64_t Hacl_Hash_Lib_Create_uint64_t;
typedef uint8_t Hacl_Hash_Lib_Create_uint8_ht;
typedef uint32_t Hacl_Hash_Lib_Create_uint32_ht;
typedef uint64_t Hacl_Hash_Lib_Create_uint64_ht;
typedef uint8_t *Hacl_Hash_Lib_Create_uint8_p;
typedef uint32_t *Hacl_Hash_Lib_Create_uint32_p;
typedef uint64_t *Hacl_Hash_Lib_Create_uint64_p;
typedef uint8_t Hacl_Hash_SHA2_512_Lemmas_uint8_t;
typedef uint32_t Hacl_Hash_SHA2_512_Lemmas_uint32_t;
typedef uint64_t Hacl_Hash_SHA2_512_Lemmas_uint64_t;
typedef uint8_t Hacl_Hash_SHA2_512_Lemmas_uint8_ht;
typedef uint32_t Hacl_Hash_SHA2_512_Lemmas_uint32_ht;
typedef uint64_t Hacl_Hash_SHA2_512_Lemmas_uint64_ht;
typedef FStar_UInt128_t Hacl_Hash_SHA2_512_Lemmas_uint128_ht;
typedef uint64_t *Hacl_Hash_SHA2_512_Lemmas_uint64_p;
typedef uint8_t *Hacl_Hash_SHA2_512_Lemmas_uint8_p;
typedef uint8_t Hacl_Hash_SHA2_512_uint8_t;
typedef uint32_t Hacl_Hash_SHA2_512_uint32_t;
typedef uint64_t Hacl_Hash_SHA2_512_uint64_t;
typedef uint8_t Hacl_Hash_SHA2_512_uint8_ht;
typedef uint32_t Hacl_Hash_SHA2_512_uint32_ht;
typedef uint64_t Hacl_Hash_SHA2_512_uint64_ht;
typedef FStar_UInt128_t Hacl_Hash_SHA2_512_uint128_ht;
typedef uint64_t *Hacl_Hash_SHA2_512_uint64_p;
typedef uint8_t *Hacl_Hash_SHA2_512_uint8_p;
typedef uint8_t SHA2_512_uint8_t;
typedef uint32_t SHA2_512_uint32_t;
typedef uint64_t SHA2_512_uint64_t;
typedef uint8_t SHA2_512_uint8_ht;
typedef uint32_t SHA2_512_uint32_ht;
typedef uint64_t SHA2_512_uint64_ht;
typedef FStar_UInt128_t SHA2_512_uint128_ht;
typedef uint64_t *SHA2_512_uint64_p;
typedef uint8_t *SHA2_512_uint8_p;
typedef uint8_t *Hacl_Impl_Ed25519_SecretExpand_hint8_p;
typedef uint8_t *Hacl_Impl_Ed25519_SecretToPublic_hint8_p;
typedef Prims_nat Hacl_Impl_Ed25519_Verify_Lemmas_u51;
typedef void *Hacl_Spec_BignumQ_Eval_qelem;
typedef uint32_t Hacl_Spec_BignumQ_Eval_u32;
typedef uint64_t Hacl_Spec_BignumQ_Eval_u64;
typedef uint8_t *Hacl_Impl_Ed25519_PointEqual_uint8_p;
typedef uint64_t *Hacl_Impl_Ed25519_PointEqual_felem;
typedef uint32_t Hacl_Impl_Load56_u32;
typedef uint8_t Hacl_Impl_Load56_h8;
typedef uint64_t Hacl_Impl_Load56_h64;
typedef uint8_t *Hacl_Impl_Load56_hint8_p;
typedef uint64_t *Hacl_Impl_Ed25519_RecoverX_elemB;
typedef uint32_t Hacl_Impl_Load51_u32;
typedef uint8_t Hacl_Impl_Load51_h8;
typedef uint64_t Hacl_Impl_Load51_h64;
typedef uint8_t *Hacl_Impl_Load51_hint8_p;
typedef uint8_t *Hacl_Impl_Store56_hint8_p;
typedef uint64_t *Hacl_Impl_Store56_qelem;
typedef uint8_t *Hacl_Impl_SHA512_Ed25519_1_hint8_p;
typedef uint8_t *Hacl_Impl_SHA512_Ed25519_hint8_p;
typedef uint8_t *Hacl_Impl_Sha512_hint8_p;
typedef FStar_UInt128_t Hacl_Lib_Create128_h128;
typedef uint64_t Hacl_Spec_BignumQ_Mul_Lemmas_3_u56;
typedef Prims_nat Hacl_Spec_BignumQ_Mul_Lemmas_1_u56;
typedef void *Hacl_Spec_BignumQ_Mul_qelem_56;
typedef uint64_t *Hacl_Impl_BignumQ_Mul_qelemB;
typedef uint64_t Hacl_Impl_BignumQ_Mul_h64;
typedef uint8_t *Hacl_Impl_Ed25519_Verify_Steps_uint8_p;
typedef uint64_t *Hacl_Impl_Ed25519_Verify_Steps_felem;
typedef uint8_t *Hacl_Impl_Ed25519_Verify_uint8_p;
typedef uint64_t *Hacl_Impl_Ed25519_Verify_felem;
typedef uint8_t *Hacl_Impl_Ed25519_Sign_Steps_hint8_p;
typedef uint8_t *Hacl_Impl_Ed25519_Sign_hint8_p;
typedef uint8_t *Ed25519_uint8_p;
typedef uint8_t *Ed25519_hint8_p;
void *Ed25519_op_String_Access(FStar_Monotonic_HyperStack_mem h, uint8_t *b);
void Ed25519_sign(uint8_t *signature, uint8_t *secret, uint8_t *msg, uint32_t len1);
bool Ed25519_verify(uint8_t *public, uint8_t *msg, uint32_t len1, uint8_t *signature);
void Ed25519_secret_to_public(uint8_t *out, uint8_t *secret);
#endif
sw/airborne/modules/datalink/hacl-c/FStar.h
+294
View File
@@ -0,0 +1,294 @@
/* This file was auto-generated by KreMLin! */
#ifndef __FStar_H
#define __FStar_H
typedef struct
{
uint64_t low;
uint64_t high;
}
FStar_UInt128_uint128;
typedef FStar_UInt128_uint128 FStar_UInt128_t;
typedef struct
{
uint64_t fst;
uint64_t snd;
uint64_t thd;
uint64_t f3;
}
K___uint64_t_uint64_t_uint64_t_uint64_t;
static uint64_t FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b)
{
return (a ^ ((a ^ b) | ((a - b) ^ b))) >> (uint32_t )63;
}
static uint64_t FStar_UInt128_carry(uint64_t a, uint64_t b)
{
return FStar_UInt128_constant_time_carry(a, b);
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
{
return
(
(FStar_UInt128_uint128 ){
.low = a.low + b.low,
.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low)
}
);
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
{
return
(
(FStar_UInt128_uint128 ){
.low = a.low + b.low,
.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low)
}
);
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
{
return
(
(FStar_UInt128_uint128 ){
.low = a.low - b.low,
.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low)
}
);
}
static FStar_UInt128_uint128 __attribute__((unused))
FStar_UInt128_sub_mod_impl(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
{
return
(
(FStar_UInt128_uint128 ){
.low = a.low - b.low,
.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low)
}
);
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_sub_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
{
return FStar_UInt128_sub_mod_impl(a, b);
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_logand(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
{
return ((FStar_UInt128_uint128 ){ .low = a.low & b.low, .high = a.high & b.high });
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
{
return ((FStar_UInt128_uint128 ){ .low = a.low ^ b.low, .high = a.high ^ b.high });
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
{
return ((FStar_UInt128_uint128 ){ .low = a.low | b.low, .high = a.high | b.high });
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_lognot(FStar_UInt128_uint128 a)
{
return ((FStar_UInt128_uint128 ){ .low = ~a.low, .high = ~a.high });
}
static uint32_t FStar_UInt128_u32_64 = (uint32_t )64;
static uint64_t FStar_UInt128_add_u64_shift_left(uint64_t hi, uint64_t lo, uint32_t s)
{
return (hi << s) + (lo >> (FStar_UInt128_u32_64 - s));
}
static uint64_t FStar_UInt128_add_u64_shift_left_respec(uint64_t hi, uint64_t lo, uint32_t s)
{
return FStar_UInt128_add_u64_shift_left(hi, lo, s);
}
static FStar_UInt128_uint128 __attribute__((unused))
FStar_UInt128_shift_left_small(FStar_UInt128_uint128 a, uint32_t s)
{
if (s == (uint32_t )0)
return a;
else
return
(
(FStar_UInt128_uint128 ){
.low = a.low << s,
.high = FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s)
}
);
}
static FStar_UInt128_uint128 __attribute__((unused))
FStar_UInt128_shift_left_large(FStar_UInt128_uint128 a, uint32_t s)
{
return
((FStar_UInt128_uint128 ){ .low = (uint64_t )0, .high = a.low << (s - FStar_UInt128_u32_64) });
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_shift_left(FStar_UInt128_uint128 a, uint32_t s)
{
if (s < FStar_UInt128_u32_64)
return FStar_UInt128_shift_left_small(a, s);
else
return FStar_UInt128_shift_left_large(a, s);
}
static uint64_t FStar_UInt128_add_u64_shift_right(uint64_t hi, uint64_t lo, uint32_t s)
{
return (lo >> s) + (hi << (FStar_UInt128_u32_64 - s));
}
static uint64_t FStar_UInt128_add_u64_shift_right_respec(uint64_t hi, uint64_t lo, uint32_t s)
{
return FStar_UInt128_add_u64_shift_right(hi, lo, s);
}
static FStar_UInt128_uint128 __attribute__((unused))
FStar_UInt128_shift_right_small(FStar_UInt128_uint128 a, uint32_t s)
{
if (s == (uint32_t )0)
return a;
else
return
(
(FStar_UInt128_uint128 ){
.low = FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s),
.high = a.high >> s
}
);
}
static FStar_UInt128_uint128 __attribute__((unused))
FStar_UInt128_shift_right_large(FStar_UInt128_uint128 a, uint32_t s)
{
return
((FStar_UInt128_uint128 ){ .low = a.high >> (s - FStar_UInt128_u32_64), .high = (uint64_t )0 });
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_shift_right(FStar_UInt128_uint128 a, uint32_t s)
{
if (s < FStar_UInt128_u32_64)
return FStar_UInt128_shift_right_small(a, s);
else
return FStar_UInt128_shift_right_large(a, s);
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_eq_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
{
return
(
(FStar_UInt128_uint128 ){
.low = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high),
.high = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high)
}
);
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_gte_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
{
return
(
(FStar_UInt128_uint128 ){
.low = (FStar_UInt64_gte_mask(a.high,
b.high)
& ~FStar_UInt64_eq_mask(a.high, b.high))
| (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low)),
.high = (FStar_UInt64_gte_mask(a.high,
b.high)
& ~FStar_UInt64_eq_mask(a.high, b.high))
| (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low))
}
);
}
static FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t a)
{
return ((FStar_UInt128_uint128 ){ .low = a, .high = (uint64_t )0 });
}
static uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a)
{
return a.low;
}
static uint64_t FStar_UInt128_u64_l32_mask = (uint64_t )0xffffffff;
static uint64_t FStar_UInt128_u64_mod_32(uint64_t a)
{
return a & FStar_UInt128_u64_l32_mask;
}
static uint32_t FStar_UInt128_u32_32 = (uint32_t )32;
static K___uint64_t_uint64_t_uint64_t_uint64_t
FStar_UInt128_mul_wide_impl_t_(uint64_t x, uint64_t y)
{
return
(
(K___uint64_t_uint64_t_uint64_t_uint64_t ){
.fst = FStar_UInt128_u64_mod_32(x),
.snd = FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y)),
.thd = x >> FStar_UInt128_u32_32,
.f3 = (x >> FStar_UInt128_u32_32)
* FStar_UInt128_u64_mod_32(y)
+ (FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y) >> FStar_UInt128_u32_32)
}
);
}
static uint64_t FStar_UInt128_u32_combine_(uint64_t hi, uint64_t lo)
{
return lo + (hi << FStar_UInt128_u32_32);
}
static FStar_UInt128_uint128 FStar_UInt128_mul_wide_impl(uint64_t x, uint64_t y)
{
K___uint64_t_uint64_t_uint64_t_uint64_t scrut = FStar_UInt128_mul_wide_impl_t_(x, y);
uint64_t u1 = scrut.fst;
uint64_t w3 = scrut.snd;
uint64_t x_ = scrut.thd;
uint64_t t_ = scrut.f3;
return
(
(FStar_UInt128_uint128 ){
.low = FStar_UInt128_u32_combine_(u1
* (y >> FStar_UInt128_u32_32)
+ FStar_UInt128_u64_mod_32(t_),
w3),
.high = x_
* (y >> FStar_UInt128_u32_32)
+ (t_ >> FStar_UInt128_u32_32)
+
((u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_))
>> FStar_UInt128_u32_32)
}
);
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_UInt128_mul_wide(uint64_t x, uint64_t y)
{
return FStar_UInt128_mul_wide_impl(x, y);
}
static FStar_UInt128_uint128 __attribute__((unused)) FStar_Int_Cast_Full_uint64_to_uint128(uint64_t a)
{
return FStar_UInt128_uint64_to_uint128(a);
}
static uint64_t __attribute__((unused)) FStar_Int_Cast_Full_uint128_to_uint64(FStar_UInt128_uint128 a)
{
return FStar_UInt128_uint128_to_uint64(a);
}
#endif
sw/airborne/modules/datalink/hacl-c/HMAC_SHA2_256.c
+348
View File
@@ -0,0 +1,348 @@
#include "HMAC_SHA2_256.h"
static void
Hacl_Hash_Lib_LoadStore_uint32s_from_be_bytes(uint32_t *output, uint8_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t *x0 = input + (uint32_t )4 * i;
uint32_t inputi = load32_be(x0);
output[i] = inputi;
}
}
static void
Hacl_Hash_Lib_LoadStore_uint32s_to_be_bytes(uint8_t *output, uint32_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint32_t hd1 = input[i];
uint8_t *x0 = output + (uint32_t )4 * i;
store32_be(x0, hd1);
}
}
static void Hacl_Hash_SHA2_256_init(uint32_t *state)
{
(void )(state + (uint32_t )136);
uint32_t *k1 = state;
uint32_t *h_01 = state + (uint32_t )128;
uint32_t *p10 = k1;
uint32_t *p20 = k1 + (uint32_t )16;
uint32_t *p3 = k1 + (uint32_t )32;
uint32_t *p4 = k1 + (uint32_t )48;
uint32_t *p11 = p10;
uint32_t *p21 = p10 + (uint32_t )8;
uint32_t *p12 = p11;
uint32_t *p22 = p11 + (uint32_t )4;
p12[0] = (uint32_t )0x428a2f98;
p12[1] = (uint32_t )0x71374491;
p12[2] = (uint32_t )0xb5c0fbcf;
p12[3] = (uint32_t )0xe9b5dba5;
p22[0] = (uint32_t )0x3956c25b;
p22[1] = (uint32_t )0x59f111f1;
p22[2] = (uint32_t )0x923f82a4;
p22[3] = (uint32_t )0xab1c5ed5;
uint32_t *p13 = p21;
uint32_t *p23 = p21 + (uint32_t )4;
p13[0] = (uint32_t )0xd807aa98;
p13[1] = (uint32_t )0x12835b01;
p13[2] = (uint32_t )0x243185be;
p13[3] = (uint32_t )0x550c7dc3;
p23[0] = (uint32_t )0x72be5d74;
p23[1] = (uint32_t )0x80deb1fe;
p23[2] = (uint32_t )0x9bdc06a7;
p23[3] = (uint32_t )0xc19bf174;
uint32_t *p14 = p20;
uint32_t *p24 = p20 + (uint32_t )8;
uint32_t *p15 = p14;
uint32_t *p25 = p14 + (uint32_t )4;
p15[0] = (uint32_t )0xe49b69c1;
p15[1] = (uint32_t )0xefbe4786;
p15[2] = (uint32_t )0x0fc19dc6;
p15[3] = (uint32_t )0x240ca1cc;
p25[0] = (uint32_t )0x2de92c6f;
p25[1] = (uint32_t )0x4a7484aa;
p25[2] = (uint32_t )0x5cb0a9dc;
p25[3] = (uint32_t )0x76f988da;
uint32_t *p16 = p24;
uint32_t *p26 = p24 + (uint32_t )4;
p16[0] = (uint32_t )0x983e5152;
p16[1] = (uint32_t )0xa831c66d;
p16[2] = (uint32_t )0xb00327c8;
p16[3] = (uint32_t )0xbf597fc7;
p26[0] = (uint32_t )0xc6e00bf3;
p26[1] = (uint32_t )0xd5a79147;
p26[2] = (uint32_t )0x06ca6351;
p26[3] = (uint32_t )0x14292967;
uint32_t *p17 = p3;
uint32_t *p27 = p3 + (uint32_t )8;
uint32_t *p18 = p17;
uint32_t *p28 = p17 + (uint32_t )4;
p18[0] = (uint32_t )0x27b70a85;
p18[1] = (uint32_t )0x2e1b2138;
p18[2] = (uint32_t )0x4d2c6dfc;
p18[3] = (uint32_t )0x53380d13;
p28[0] = (uint32_t )0x650a7354;
p28[1] = (uint32_t )0x766a0abb;
p28[2] = (uint32_t )0x81c2c92e;
p28[3] = (uint32_t )0x92722c85;
uint32_t *p19 = p27;
uint32_t *p29 = p27 + (uint32_t )4;
p19[0] = (uint32_t )0xa2bfe8a1;
p19[1] = (uint32_t )0xa81a664b;
p19[2] = (uint32_t )0xc24b8b70;
p19[3] = (uint32_t )0xc76c51a3;
p29[0] = (uint32_t )0xd192e819;
p29[1] = (uint32_t )0xd6990624;
p29[2] = (uint32_t )0xf40e3585;
p29[3] = (uint32_t )0x106aa070;
uint32_t *p110 = p4;
uint32_t *p210 = p4 + (uint32_t )8;
uint32_t *p1 = p110;
uint32_t *p211 = p110 + (uint32_t )4;
p1[0] = (uint32_t )0x19a4c116;
p1[1] = (uint32_t )0x1e376c08;
p1[2] = (uint32_t )0x2748774c;
p1[3] = (uint32_t )0x34b0bcb5;
p211[0] = (uint32_t )0x391c0cb3;
p211[1] = (uint32_t )0x4ed8aa4a;
p211[2] = (uint32_t )0x5b9cca4f;
p211[3] = (uint32_t )0x682e6ff3;
uint32_t *p111 = p210;
uint32_t *p212 = p210 + (uint32_t )4;
p111[0] = (uint32_t )0x748f82ee;
p111[1] = (uint32_t )0x78a5636f;
p111[2] = (uint32_t )0x84c87814;
p111[3] = (uint32_t )0x8cc70208;
p212[0] = (uint32_t )0x90befffa;
p212[1] = (uint32_t )0xa4506ceb;
p212[2] = (uint32_t )0xbef9a3f7;
p212[3] = (uint32_t )0xc67178f2;
uint32_t *p112 = h_01;
uint32_t *p2 = h_01 + (uint32_t )4;
p112[0] = (uint32_t )0x6a09e667;
p112[1] = (uint32_t )0xbb67ae85;
p112[2] = (uint32_t )0x3c6ef372;
p112[3] = (uint32_t )0xa54ff53a;
p2[0] = (uint32_t )0x510e527f;
p2[1] = (uint32_t )0x9b05688c;
p2[2] = (uint32_t )0x1f83d9ab;
p2[3] = (uint32_t )0x5be0cd19;
}
static void Hacl_Hash_SHA2_256_update(uint32_t *state, uint8_t *data)
{
uint32_t data_w[16] = { 0 };
Hacl_Hash_Lib_LoadStore_uint32s_from_be_bytes(data_w, data, (uint32_t )16);
uint32_t *hash_w = state + (uint32_t )128;
uint32_t *ws_w = state + (uint32_t )64;
uint32_t *k_w = state;
uint32_t *counter_w = state + (uint32_t )136;
for (uint32_t i = (uint32_t )0; i < (uint32_t )16; i = i + (uint32_t )1)
{
uint32_t uu____206 = data_w[i];
ws_w[i] = uu____206;
}
for (uint32_t i = (uint32_t )16; i < (uint32_t )64; i = i + (uint32_t )1)
{
uint32_t t16 = ws_w[i - (uint32_t )16];
uint32_t t15 = ws_w[i - (uint32_t )15];
uint32_t t7 = ws_w[i - (uint32_t )7];
uint32_t t2 = ws_w[i - (uint32_t )2];
ws_w[i] =
((t2 >> (uint32_t )17 | t2 << (uint32_t )32 - (uint32_t )17)
^ (t2 >> (uint32_t )19 | t2 << (uint32_t )32 - (uint32_t )19) ^ t2 >> (uint32_t )10)
+
t7
+
((t15 >> (uint32_t )7 | t15 << (uint32_t )32 - (uint32_t )7)
^ (t15 >> (uint32_t )18 | t15 << (uint32_t )32 - (uint32_t )18) ^ t15 >> (uint32_t )3)
+ t16;
}
uint32_t hash_0[8] = { 0 };
memcpy(hash_0, hash_w, (uint32_t )8 * sizeof hash_w[0]);
for (uint32_t i = (uint32_t )0; i < (uint32_t )64; i = i + (uint32_t )1)
{
uint32_t a = hash_0[0];
uint32_t b = hash_0[1];
uint32_t c = hash_0[2];
uint32_t d = hash_0[3];
uint32_t e = hash_0[4];
uint32_t f1 = hash_0[5];
uint32_t g = hash_0[6];
uint32_t h = hash_0[7];
uint32_t kt = k_w[i];
uint32_t wst = ws_w[i];
uint32_t
t1 =
h
+
((e >> (uint32_t )6 | e << (uint32_t )32 - (uint32_t )6)
^
(e >> (uint32_t )11 | e << (uint32_t )32 - (uint32_t )11)
^ (e >> (uint32_t )25 | e << (uint32_t )32 - (uint32_t )25))
+ (e & f1 ^ ~e & g)
+ kt
+ wst;
uint32_t
t2 =
((a >> (uint32_t )2 | a << (uint32_t )32 - (uint32_t )2)
^
(a >> (uint32_t )13 | a << (uint32_t )32 - (uint32_t )13)
^ (a >> (uint32_t )22 | a << (uint32_t )32 - (uint32_t )22))
+ (a & b ^ a & c ^ b & c);
uint32_t x1 = t1 + t2;
uint32_t x5 = d + t1;
uint32_t *p1 = hash_0;
uint32_t *p2 = hash_0 + (uint32_t )4;
p1[0] = x1;
p1[1] = a;
p1[2] = b;
p1[3] = c;
p2[0] = x5;
p2[1] = e;
p2[2] = f1;
p2[3] = g;
}
for (uint32_t i = (uint32_t )0; i < (uint32_t )8; i = i + (uint32_t )1)
{
uint32_t uu____871 = hash_w[i];
uint32_t uu____874 = hash_0[i];
uint32_t uu____870 = uu____871 + uu____874;
hash_w[i] = uu____870;
}
uint32_t c0 = counter_w[0];
uint32_t one1 = (uint32_t )1;
counter_w[0] = c0 + one1;
}
static void Hacl_Hash_SHA2_256_update_multi(uint32_t *state, uint8_t *data, uint32_t n1)
{
for (uint32_t i = (uint32_t )0; i < n1; i = i + (uint32_t )1)
{
uint8_t *b = data + i * (uint32_t )64;
Hacl_Hash_SHA2_256_update(state, b);
}
}
static void Hacl_Hash_SHA2_256_update_last(uint32_t *state, uint8_t *data, uint32_t len)
{
uint8_t blocks[128] = { 0 };
K___uint32_t_uint8_t_ uu____1925;
if (len < (uint32_t )56)
uu____1925 = ((K___uint32_t_uint8_t_ ){ .fst = (uint32_t )1, .snd = blocks + (uint32_t )64 });
else
uu____1925 = ((K___uint32_t_uint8_t_ ){ .fst = (uint32_t )2, .snd = blocks });
K___uint32_t_uint8_t_ scrut = uu____1925;
uint32_t nb = scrut.fst;
uint8_t *final_blocks = scrut.snd;
memcpy(final_blocks, data, len * sizeof data[0]);
uint32_t n1 = state[136];
uint8_t *padding = final_blocks + len;
uint32_t
pad0len = ((uint32_t )64 - (len + (uint32_t )8 + (uint32_t )1) % (uint32_t )64) % (uint32_t )64;
uint8_t *buf1 = padding;
(void )(padding + (uint32_t )1);
uint8_t *buf2 = padding + (uint32_t )1 + pad0len;
uint64_t
encodedlen =
((uint64_t )n1 * (uint64_t )(uint32_t )64 + (uint64_t )len)
* (uint64_t )(uint32_t )8;
buf1[0] = (uint8_t )0x80;
store64_be(buf2, encodedlen);
Hacl_Hash_SHA2_256_update_multi(state, final_blocks, nb);
}
static void Hacl_Hash_SHA2_256_finish(uint32_t *state, uint8_t *hash1)
{
uint32_t *hash_w = state + (uint32_t )128;
Hacl_Hash_Lib_LoadStore_uint32s_to_be_bytes(hash1, hash_w, (uint32_t )8);
}
static void Hacl_Hash_SHA2_256_hash(uint8_t *hash1, uint8_t *input, uint32_t len)
{
uint32_t state[137] = { 0 };
uint32_t n1 = len / (uint32_t )64;
uint32_t r = len % (uint32_t )64;
uint8_t *input_blocks = input;
uint8_t *input_last = input + n1 * (uint32_t )64;
Hacl_Hash_SHA2_256_init(state);
Hacl_Hash_SHA2_256_update_multi(state, input_blocks, n1);
Hacl_Hash_SHA2_256_update_last(state, input_last, r);
Hacl_Hash_SHA2_256_finish(state, hash1);
}
static void Hacl_HMAC_SHA2_256_xor_bytes_inplace(uint8_t *a, uint8_t *b, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t uu____871 = a[i];
uint8_t uu____874 = b[i];
uint8_t uu____870 = uu____871 ^ uu____874;
a[i] = uu____870;
}
}
static void
Hacl_HMAC_SHA2_256_hmac_core(uint8_t *mac, uint8_t *key, uint8_t *data, uint32_t len)
{
uint8_t ipad[64];
for (uintmax_t _i = 0; _i < (uint32_t )64; ++_i)
ipad[_i] = (uint8_t )0x36;
uint8_t opad[64];
for (uintmax_t _i = 0; _i < (uint32_t )64; ++_i)
opad[_i] = (uint8_t )0x5c;
Hacl_HMAC_SHA2_256_xor_bytes_inplace(ipad, key, (uint32_t )64);
uint32_t state0[137] = { 0 };
uint32_t n0 = len / (uint32_t )64;
uint32_t r0 = len % (uint32_t )64;
uint8_t *blocks0 = data;
uint8_t *last0 = data + n0 * (uint32_t )64;
Hacl_Hash_SHA2_256_init(state0);
Hacl_Hash_SHA2_256_update(state0, ipad);
Hacl_Hash_SHA2_256_update_multi(state0, blocks0, n0);
Hacl_Hash_SHA2_256_update_last(state0, last0, r0);
uint8_t *hash0 = ipad;
Hacl_Hash_SHA2_256_finish(state0, hash0);
uint8_t *s4 = ipad;
Hacl_HMAC_SHA2_256_xor_bytes_inplace(opad, key, (uint32_t )64);
uint32_t state1[137] = { 0 };
Hacl_Hash_SHA2_256_init(state1);
Hacl_Hash_SHA2_256_update(state1, opad);
Hacl_Hash_SHA2_256_update_last(state1, s4, (uint32_t )32);
Hacl_Hash_SHA2_256_finish(state1, mac);
}
static void
Hacl_HMAC_SHA2_256_hmac(
uint8_t *mac,
uint8_t *key,
uint32_t keylen,
uint8_t *data,
uint32_t datalen
)
{
uint8_t nkey[64];
for (uintmax_t _i = 0; _i < (uint32_t )64; ++_i)
nkey[_i] = (uint8_t )0x00;
if (keylen <= (uint32_t )64)
memcpy(nkey, key, keylen * sizeof key[0]);
else
{
uint8_t *nkey0 = nkey;
Hacl_Hash_SHA2_256_hash(nkey0, key, keylen);
}
Hacl_HMAC_SHA2_256_hmac_core(mac, nkey, data, datalen);
}
void hmac_core(uint8_t *mac, uint8_t *key, uint8_t *data, uint32_t len)
{
Hacl_HMAC_SHA2_256_hmac_core(mac, key, data, len);
}
void hmac(uint8_t *mac, uint8_t *key, uint32_t keylen, uint8_t *data, uint32_t datalen)
{
Hacl_HMAC_SHA2_256_hmac(mac, key, keylen, data, datalen);
}
sw/airborne/modules/datalink/hacl-c/HMAC_SHA2_256.h
+78
View File
@@ -0,0 +1,78 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __HMAC_SHA2_256_H
#define __HMAC_SHA2_256_H
#include "testlib.h"
typedef uint8_t Hacl_Hash_Lib_Create_uint8_t;
typedef uint32_t Hacl_Hash_Lib_Create_uint32_t;
typedef uint64_t Hacl_Hash_Lib_Create_uint64_t;
typedef uint8_t Hacl_Hash_Lib_Create_uint8_ht;
typedef uint32_t Hacl_Hash_Lib_Create_uint32_ht;
typedef uint64_t Hacl_Hash_Lib_Create_uint64_ht;
typedef uint8_t *Hacl_Hash_Lib_Create_uint8_p;
typedef uint32_t *Hacl_Hash_Lib_Create_uint32_p;
typedef uint64_t *Hacl_Hash_Lib_Create_uint64_p;
typedef uint8_t *Hacl_Hash_Lib_LoadStore_uint8_p;
typedef uint8_t Hacl_Hash_SHA2_256_uint8_t;
typedef uint32_t Hacl_Hash_SHA2_256_uint32_t;
typedef uint64_t Hacl_Hash_SHA2_256_uint64_t;
typedef uint8_t Hacl_Hash_SHA2_256_uint8_ht;
typedef uint32_t Hacl_Hash_SHA2_256_uint32_ht;
typedef uint64_t Hacl_Hash_SHA2_256_uint64_ht;
typedef uint32_t *Hacl_Hash_SHA2_256_uint32_p;
typedef uint8_t *Hacl_Hash_SHA2_256_uint8_p;
typedef struct
{
uint32_t fst;
uint8_t *snd;
}
K___uint32_t_uint8_t_;
typedef uint8_t Hacl_HMAC_SHA2_256_uint8_t;
typedef uint32_t Hacl_HMAC_SHA2_256_uint32_t;
typedef uint64_t Hacl_HMAC_SHA2_256_uint64_t;
typedef uint8_t Hacl_HMAC_SHA2_256_uint8_ht;
typedef uint32_t Hacl_HMAC_SHA2_256_uint32_ht;
typedef uint64_t Hacl_HMAC_SHA2_256_uint64_ht;
typedef uint32_t *Hacl_HMAC_SHA2_256_uint32_p;
typedef uint8_t *Hacl_HMAC_SHA2_256_uint8_p;
typedef uint8_t uint8_ht;
typedef uint32_t uint32_t;
typedef uint8_t *uint8_p;
void hmac_core(uint8_t *mac, uint8_t *key, uint8_t *data, uint32_t len);
void hmac(uint8_t *mac, uint8_t *key, uint32_t keylen, uint8_t *data, uint32_t datalen);
#endif
sw/airborne/modules/datalink/hacl-c/Hacl_Policies.c
+42
View File
@@ -0,0 +1,42 @@
#include "Hacl_Policies.h"
uint8_t Hacl_Policies_declassify_u8(uint8_t x)
{
return x;
}
uint32_t Hacl_Policies_declassify_u32(uint32_t x)
{
return x;
}
uint64_t Hacl_Policies_declassify_u64(uint64_t x)
{
return x;
}
FStar_UInt128_t Hacl_Policies_declassify_u128(FStar_UInt128_t x)
{
return x;
}
uint8_t Hacl_Policies_cmp_bytes_(uint8_t *b1, uint8_t *b2, uint32_t len, uint8_t *tmp)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t bi1 = b1[i];
uint8_t bi2 = b2[i];
uint8_t z0 = tmp[0];
tmp[0] = FStar_UInt8_eq_mask(bi1, bi2) & z0;
}
return tmp[0];
}
uint8_t Hacl_Policies_cmp_bytes(uint8_t *b1, uint8_t *b2, uint32_t len)
{
uint8_t tmp[1];
tmp[0] = (uint8_t )255;
uint8_t z = Hacl_Policies_cmp_bytes_(b1, b2, len, tmp);
return ~z;
}
sw/airborne/modules/datalink/hacl-c/Hacl_Policies.h
+21
View File
@@ -0,0 +1,21 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __Hacl_Policies_H
#define __Hacl_Policies_H
uint8_t Hacl_Policies_declassify_u8(uint8_t x);
uint32_t Hacl_Policies_declassify_u32(uint32_t x);
uint64_t Hacl_Policies_declassify_u64(uint64_t x);
FStar_UInt128_t Hacl_Policies_declassify_u128(FStar_UInt128_t x);
uint8_t Hacl_Policies_cmp_bytes_(uint8_t *b1, uint8_t *b2, uint32_t len, uint8_t *tmp);
uint8_t Hacl_Policies_cmp_bytes(uint8_t *b1, uint8_t *b2, uint32_t len);
#endif
sw/airborne/modules/datalink/hacl-c/NaCl.c
+439
View File
@@ -0,0 +1,439 @@
#include "NaCl.h"
static void Hacl_SecretBox_ZeroPad_set_zero_bytes(uint8_t *b)
{
uint8_t zero1 = (uint8_t )0;
b[0] = zero1;
b[1] = zero1;
b[2] = zero1;
b[3] = zero1;
b[4] = zero1;
b[5] = zero1;
b[6] = zero1;
b[7] = zero1;
b[8] = zero1;
b[9] = zero1;
b[10] = zero1;
b[11] = zero1;
b[12] = zero1;
b[13] = zero1;
b[14] = zero1;
b[15] = zero1;
b[16] = zero1;
b[17] = zero1;
b[18] = zero1;
b[19] = zero1;
b[20] = zero1;
b[21] = zero1;
b[22] = zero1;
b[23] = zero1;
b[24] = zero1;
b[25] = zero1;
b[26] = zero1;
b[27] = zero1;
b[28] = zero1;
b[29] = zero1;
b[30] = zero1;
b[31] = zero1;
}
static uint32_t
Hacl_SecretBox_ZeroPad_crypto_secretbox_detached(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
)
{
uint32_t mlen_ = (uint32_t )mlen;
uint8_t subkey[32] = { 0 };
Salsa20_hsalsa20(subkey, k1, n1);
Salsa20_salsa20(c, m, mlen_ + (uint32_t )32, subkey, n1 + (uint32_t )16, (uint64_t )0);
Poly1305_64_crypto_onetimeauth(mac, c + (uint32_t )32, mlen, c);
Hacl_SecretBox_ZeroPad_set_zero_bytes(c);
Hacl_SecretBox_ZeroPad_set_zero_bytes(subkey);
return (uint32_t )0;
}
static uint32_t
Hacl_SecretBox_ZeroPad_crypto_secretbox_open_detached_decrypt(
uint8_t *m,
uint8_t *c,
uint64_t clen,
uint8_t *n1,
uint8_t *subkey,
uint8_t verify
)
{
uint32_t clen_ = (uint32_t )clen;
if (verify == (uint8_t )0)
{
Salsa20_salsa20(m, c, clen_ + (uint32_t )32, subkey, n1 + (uint32_t )16, (uint64_t )0);
Hacl_SecretBox_ZeroPad_set_zero_bytes(subkey);
Hacl_SecretBox_ZeroPad_set_zero_bytes(m);
return (uint32_t )0;
}
else
return (uint32_t )0xffffffff;
}
static uint32_t
Hacl_SecretBox_ZeroPad_crypto_secretbox_open_detached(
uint8_t *m,
uint8_t *c,
uint8_t *mac,
uint64_t clen,
uint8_t *n1,
uint8_t *k1
)
{
uint8_t tmp[112] = { 0 };
uint8_t *subkey = tmp;
uint8_t *mackey = tmp + (uint32_t )32;
uint8_t *mackey_ = tmp + (uint32_t )64;
uint8_t *cmac = tmp + (uint32_t )96;
Salsa20_hsalsa20(subkey, k1, n1);
Salsa20_salsa20(mackey, mackey_, (uint32_t )32, subkey, n1 + (uint32_t )16, (uint64_t )0);
Poly1305_64_crypto_onetimeauth(cmac, c + (uint32_t )32, clen, mackey);
uint8_t result = Hacl_Policies_cmp_bytes(mac, cmac, (uint32_t )16);
uint8_t verify = result;
uint32_t
z =
Hacl_SecretBox_ZeroPad_crypto_secretbox_open_detached_decrypt(m,
c,
clen,
n1,
subkey,
verify);
return z;
}
static uint32_t
Hacl_SecretBox_ZeroPad_crypto_secretbox_easy(
uint8_t *c,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
)
{
uint8_t cmac[16] = { 0 };
uint32_t res = Hacl_SecretBox_ZeroPad_crypto_secretbox_detached(c, cmac, m, mlen, n1, k1);
memcpy(c + (uint32_t )16, cmac, (uint32_t )16 * sizeof cmac[0]);
return res;
}
static uint32_t
Hacl_SecretBox_ZeroPad_crypto_secretbox_open_easy(
uint8_t *m,
uint8_t *c,
uint64_t clen,
uint8_t *n1,
uint8_t *k1
)
{
uint8_t *mac = c;
return Hacl_SecretBox_ZeroPad_crypto_secretbox_open_detached(m, c, mac, clen, n1, k1);
}
static uint32_t Hacl_Box_ZeroPad_crypto_box_beforenm(uint8_t *k1, uint8_t *pk, uint8_t *sk)
{
uint8_t tmp[48] = { 0 };
uint8_t *hsalsa_k = tmp;
uint8_t *hsalsa_n = tmp + (uint32_t )32;
Curve25519_crypto_scalarmult(hsalsa_k, sk, pk);
Salsa20_hsalsa20(k1, hsalsa_k, hsalsa_n);
return (uint32_t )0;
}
static uint32_t
Hacl_Box_ZeroPad_crypto_box_detached_afternm(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
)
{
return Hacl_SecretBox_ZeroPad_crypto_secretbox_detached(c, mac, m, mlen, n1, k1);
}
static uint32_t
Hacl_Box_ZeroPad_crypto_box_detached(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *pk,
uint8_t *sk
)
{
uint8_t key[80] = { 0 };
uint8_t *k1 = key;
uint8_t *subkey = key + (uint32_t )32;
uint8_t *hsalsa_n = key + (uint32_t )64;
Curve25519_crypto_scalarmult(k1, sk, pk);
Salsa20_hsalsa20(subkey, k1, hsalsa_n);
uint32_t z = Hacl_SecretBox_ZeroPad_crypto_secretbox_detached(c, mac, m, mlen, n1, subkey);
return z;
}
static uint32_t
Hacl_Box_ZeroPad_crypto_box_open_detached(
uint8_t *m,
uint8_t *c,
uint8_t *mac,
uint64_t mlen,
uint8_t *n1,
uint8_t *pk,
uint8_t *sk
)
{
uint8_t key[80] = { 0 };
uint8_t *k1 = key;
uint8_t *subkey = key + (uint32_t )32;
uint8_t *hsalsa_n = key + (uint32_t )64;
Curve25519_crypto_scalarmult(k1, sk, pk);
Salsa20_hsalsa20(subkey, k1, hsalsa_n);
uint32_t
z = Hacl_SecretBox_ZeroPad_crypto_secretbox_open_detached(m, c, mac, mlen, n1, subkey);
return z;
}
static uint32_t
Hacl_Box_ZeroPad_crypto_box_easy_afternm(
uint8_t *c,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
)
{
uint8_t cmac[16] = { 0 };
uint32_t z = Hacl_Box_ZeroPad_crypto_box_detached_afternm(c, cmac, m, mlen, n1, k1);
memcpy(c + (uint32_t )16, cmac, (uint32_t )16 * sizeof cmac[0]);
return z;
}
static uint32_t
Hacl_Box_ZeroPad_crypto_box_easy(
uint8_t *c,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *pk,
uint8_t *sk
)
{
uint8_t cmac[16] = { 0 };
uint32_t res = Hacl_Box_ZeroPad_crypto_box_detached(c, cmac, m, mlen, n1, pk, sk);
memcpy(c + (uint32_t )16, cmac, (uint32_t )16 * sizeof cmac[0]);
return res;
}
static uint32_t
Hacl_Box_ZeroPad_crypto_box_open_easy(
uint8_t *m,
uint8_t *c,
uint64_t mlen,
uint8_t *n1,
uint8_t *pk,
uint8_t *sk
)
{
uint8_t *mac = c + (uint32_t )16;
return Hacl_Box_ZeroPad_crypto_box_open_detached(m, c, mac, mlen, n1, pk, sk);
}
static uint32_t
Hacl_Box_ZeroPad_crypto_box_open_detached_afternm(
uint8_t *m,
uint8_t *c,
uint8_t *mac,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
)
{
return Hacl_SecretBox_ZeroPad_crypto_secretbox_open_detached(m, c, mac, mlen, n1, k1);
}
static uint32_t
Hacl_Box_ZeroPad_crypto_box_open_easy_afternm(
uint8_t *m,
uint8_t *c,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
)
{
uint8_t *mac = c;
uint32_t t = Hacl_Box_ZeroPad_crypto_box_open_detached_afternm(m, c, mac, mlen, n1, k1);
return t;
}
Prims_int NaCl_crypto_box_NONCEBYTES;
Prims_int NaCl_crypto_box_PUBLICKEYBYTES;
Prims_int NaCl_crypto_box_SECRETKEYBYTES;
Prims_int NaCl_crypto_box_MACBYTES;
Prims_int NaCl_crypto_secretbox_NONCEBYTES;
Prims_int NaCl_crypto_secretbox_KEYBYTES;
Prims_int NaCl_crypto_secretbox_MACBYTES;
uint32_t
NaCl_crypto_secretbox_detached(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
)
{
return Hacl_SecretBox_ZeroPad_crypto_secretbox_detached(c, mac, m, mlen, n1, k1);
}
uint32_t
NaCl_crypto_secretbox_open_detached(
uint8_t *m,
uint8_t *c,
uint8_t *mac,
uint64_t clen,
uint8_t *n1,
uint8_t *k1
)
{
return Hacl_SecretBox_ZeroPad_crypto_secretbox_open_detached(m, c, mac, clen, n1, k1);
}
uint32_t
NaCl_crypto_secretbox_easy(uint8_t *c, uint8_t *m, uint64_t mlen, uint8_t *n1, uint8_t *k1)
{
return Hacl_SecretBox_ZeroPad_crypto_secretbox_easy(c, m, mlen, n1, k1);
}
uint32_t
NaCl_crypto_secretbox_open_easy(
uint8_t *m,
uint8_t *c,
uint64_t clen,
uint8_t *n1,
uint8_t *k1
)
{
return Hacl_SecretBox_ZeroPad_crypto_secretbox_open_easy(m, c, clen, n1, k1);
}
uint32_t NaCl_crypto_box_beforenm(uint8_t *k1, uint8_t *pk, uint8_t *sk)
{
return Hacl_Box_ZeroPad_crypto_box_beforenm(k1, pk, sk);
}
uint32_t
NaCl_crypto_box_detached_afternm(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
)
{
return Hacl_Box_ZeroPad_crypto_box_detached_afternm(c, mac, m, mlen, n1, k1);
}
uint32_t
NaCl_crypto_box_detached(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *pk,
uint8_t *sk
)
{
return Hacl_Box_ZeroPad_crypto_box_detached(c, mac, m, mlen, n1, pk, sk);
}
uint32_t
NaCl_crypto_box_open_detached(
uint8_t *m,
uint8_t *c,
uint8_t *mac,
uint64_t mlen,
uint8_t *n1,
uint8_t *pk,
uint8_t *sk
)
{
return Hacl_Box_ZeroPad_crypto_box_open_detached(m, c, mac, mlen, n1, pk, sk);
}
uint32_t
NaCl_crypto_box_easy_afternm(uint8_t *c, uint8_t *m, uint64_t mlen, uint8_t *n1, uint8_t *k1)
{
return Hacl_Box_ZeroPad_crypto_box_easy_afternm(c, m, mlen, n1, k1);
}
uint32_t
NaCl_crypto_box_easy(
uint8_t *c,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *pk,
uint8_t *sk
)
{
return Hacl_Box_ZeroPad_crypto_box_easy(c, m, mlen, n1, pk, sk);
}
uint32_t
NaCl_crypto_box_open_easy(
uint8_t *m,
uint8_t *c,
uint64_t mlen,
uint8_t *n1,
uint8_t *pk,
uint8_t *sk
)
{
return Hacl_Box_ZeroPad_crypto_box_open_easy(m, c, mlen, n1, pk, sk);
}
uint32_t
NaCl_crypto_box_open_detached_afternm(
uint8_t *m,
uint8_t *c,
uint8_t *mac,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
)
{
return Hacl_Box_ZeroPad_crypto_box_open_detached_afternm(m, c, mac, mlen, n1, k1);
}
uint32_t
NaCl_crypto_box_open_easy_afternm(
uint8_t *m,
uint8_t *c,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
)
{
return Hacl_Box_ZeroPad_crypto_box_open_easy_afternm(m, c, mlen, n1, k1);
}
sw/airborne/modules/datalink/hacl-c/NaCl.h
+134
View File
@@ -0,0 +1,134 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __NaCl_H
#define __NaCl_H
#include "Curve25519.h"
#include "Salsa20.h"
#include "Poly1305_64.h"
#include "Hacl_Policies.h"
extern Prims_int NaCl_crypto_box_NONCEBYTES;
extern Prims_int NaCl_crypto_box_PUBLICKEYBYTES;
extern Prims_int NaCl_crypto_box_SECRETKEYBYTES;
extern Prims_int NaCl_crypto_box_MACBYTES;
extern Prims_int NaCl_crypto_secretbox_NONCEBYTES;
extern Prims_int NaCl_crypto_secretbox_KEYBYTES;
extern Prims_int NaCl_crypto_secretbox_MACBYTES;
uint32_t
NaCl_crypto_secretbox_detached(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
);
uint32_t
NaCl_crypto_secretbox_open_detached(
uint8_t *m,
uint8_t *c,
uint8_t *mac,
uint64_t clen,
uint8_t *n1,
uint8_t *k1
);
uint32_t
NaCl_crypto_secretbox_easy(uint8_t *c, uint8_t *m, uint64_t mlen, uint8_t *n1, uint8_t *k1);
uint32_t
NaCl_crypto_secretbox_open_easy(
uint8_t *m,
uint8_t *c,
uint64_t clen,
uint8_t *n1,
uint8_t *k1
);
uint32_t NaCl_crypto_box_beforenm(uint8_t *k1, uint8_t *pk, uint8_t *sk);
uint32_t
NaCl_crypto_box_detached_afternm(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
);
uint32_t
NaCl_crypto_box_detached(
uint8_t *c,
uint8_t *mac,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *pk,
uint8_t *sk
);
uint32_t
NaCl_crypto_box_open_detached(
uint8_t *m,
uint8_t *c,
uint8_t *mac,
uint64_t mlen,
uint8_t *n1,
uint8_t *pk,
uint8_t *sk
);
uint32_t
NaCl_crypto_box_easy_afternm(uint8_t *c, uint8_t *m, uint64_t mlen, uint8_t *n1, uint8_t *k1);
uint32_t
NaCl_crypto_box_easy(
uint8_t *c,
uint8_t *m,
uint64_t mlen,
uint8_t *n1,
uint8_t *pk,
uint8_t *sk
);
uint32_t
NaCl_crypto_box_open_easy(
uint8_t *m,
uint8_t *c,
uint64_t mlen,
uint8_t *n1,
uint8_t *pk,
uint8_t *sk
);
uint32_t
NaCl_crypto_box_open_detached_afternm(
uint8_t *m,
uint8_t *c,
uint8_t *mac,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
);
uint32_t
NaCl_crypto_box_open_easy_afternm(
uint8_t *m,
uint8_t *c,
uint64_t mlen,
uint8_t *n1,
uint8_t *k1
);
#endif
sw/airborne/modules/datalink/hacl-c/Poly1305_64.c
+518
View File
File diff suppressed because it is too large Load Diff
sw/airborne/modules/datalink/hacl-c/Poly1305_64.h
+84
View File
@@ -0,0 +1,84 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __Poly1305_64_H
#define __Poly1305_64_H
#include "testlib.h"
typedef uint64_t Hacl_Bignum_Constants_limb;
typedef FStar_UInt128_t Hacl_Bignum_Constants_wide;
typedef FStar_UInt128_t Hacl_Bignum_Wide_t;
typedef uint64_t Hacl_Bignum_Limb_t;
typedef void *Hacl_Impl_Poly1305_64_State_log_t;
typedef uint8_t *Hacl_Impl_Poly1305_64_State_uint8_p;
typedef uint64_t *Hacl_Impl_Poly1305_64_State_bigint;
typedef void *Hacl_Impl_Poly1305_64_State_seqelem;
typedef uint64_t *Hacl_Impl_Poly1305_64_State_elemB;
typedef uint8_t *Hacl_Impl_Poly1305_64_State_wordB;
typedef uint8_t *Hacl_Impl_Poly1305_64_State_wordB_16;
typedef struct
{
uint64_t *r;
uint64_t *h;
}
Hacl_Impl_Poly1305_64_State_poly1305_state;
typedef void *Hacl_Impl_Poly1305_64_log_t;
typedef uint64_t *Hacl_Impl_Poly1305_64_bigint;
typedef uint8_t *Hacl_Impl_Poly1305_64_uint8_p;
typedef uint64_t *Hacl_Impl_Poly1305_64_elemB;
typedef uint8_t *Hacl_Impl_Poly1305_64_wordB;
typedef uint8_t *Hacl_Impl_Poly1305_64_wordB_16;
typedef uint8_t *Poly1305_64_uint8_p;
typedef uint64_t Poly1305_64_uint64_t;
void *Poly1305_64_op_String_Access(FStar_Monotonic_HyperStack_mem h, uint8_t *b);
typedef uint8_t *Poly1305_64_key;
typedef Hacl_Impl_Poly1305_64_State_poly1305_state Poly1305_64_state;
Hacl_Impl_Poly1305_64_State_poly1305_state Poly1305_64_mk_state(uint64_t *r, uint64_t *acc);
void Poly1305_64_init(Hacl_Impl_Poly1305_64_State_poly1305_state st, uint8_t *k1);
extern void *Poly1305_64_empty_log;
void Poly1305_64_update_block(Hacl_Impl_Poly1305_64_State_poly1305_state st, uint8_t *m);
void
Poly1305_64_update(Hacl_Impl_Poly1305_64_State_poly1305_state st, uint8_t *m, uint32_t len1);
void
Poly1305_64_update_last(
Hacl_Impl_Poly1305_64_State_poly1305_state st,
uint8_t *m,
uint32_t len1
);
void
Poly1305_64_finish(Hacl_Impl_Poly1305_64_State_poly1305_state st, uint8_t *mac, uint8_t *k1);
void
Poly1305_64_crypto_onetimeauth(uint8_t *output, uint8_t *input, uint64_t len1, uint8_t *k1);
#endif
sw/airborne/modules/datalink/hacl-c/README.md
+145
View File
@@ -0,0 +1,145 @@
HACL*
=====
HACL* is a formally verified cryptographic library in [F\*],
developed by the [Prosecco](http://prosecco.inria.fr) team at
[INRIA Paris](https://www.inria.fr/en/centre/paris) in collaboration
with Microsoft Research, as part of [Project Everest].
HACL stands for High-Assurance Cryptographic Library and its design is
inspired by discussions at the [HACS series of workshops](https://github.com/HACS-workshop).
The goal of this library is to develop verified C reference implementations
for popular cryptographic primitives and to verify them for memory safety,
functional correctness, and secret independence.
More details about the HACL* library and its design can be found in our ACM CCS 2017 research paper:
https://eprint.iacr.org/2017/536
All our code is written and verified in [F\*] and then compiled to C via
the [KreMLin tool](https://github.com/FStarLang/kremlin/). Details on the verification and compilation
toolchain and their formal guarantees can be found in the ICFP 2017 paper:
https://arxiv.org/abs/1703.00053
# Supported Cryptographic Algorithms
The primitives and constructions supported currently are:
* Stream ciphers: Chacha20, Salsa20, XSalsa20
* MACs: Poly1305, HMAC
* Elliptic Curves: Curve25519
* Elliptic Curves Signatures: Ed25519
* Hash functions: SHA2 (256,384,512)
* NaCl API: secret_box, box, sign
* TLS API: IETF Chacha20Poly1305 AEAD
Developers can use HACL* through the [NaCl API].
In particular, we implement the same C API as [libsodium] for the
NaCl constructions, so any application that relies on
libsodium only for these constructions can be immediately ported to use the verified code in HACL*
instead. (Warning: libsodium also implements other algorithms not in NaCl
that are not implemented by HACL*)
The verified primitives can also be used to support larger F* verification projects.
For example, HACL* code is used through the agile cryptographic model developed in
[secure_api/] as the basis for cryptographic proofs of the TLS record layer in [miTLS].
A detailed description of the code in [secure_api/] and its formal security guarantees
appears in the IEEE S&P 2017 paper: https://eprint.iacr.org/2016/1178.pdf
[F\*]: https://github.com/FStarLang/FStar
[KreMLin]: https://github.com/FStarLang/kremlin
[miTLS]: https://github.com/mitls/mitls-fstar
[NaCl API]: https://nacl.cr.yp.to
[libsodium]: https://github.com/jedisct1/libsodium
[Project Everest]: https://github.com/project-everest
[secure_api/]: https://github.com/mitls/hacl-star/tree/master/secure_api
# Warning
This library is at the pre-production stage.
Please consult the authors before using it in production systems.
The first release is to be expected around the time of [ACM CCS].
Any feedback is welcome in the meantime.
[ACM CCS]: https://www.sigsac.org/ccs/CCS2017/
# Licenses
All F* source code is released under Apache 2.0
All generated C code is released under MIT
# Installation
See [INSTALL.md](INSTALL.md) for prerequisites.
For convenience, C code for our verified primitives has already been extracted
and is available in [snapshots/hacl-c](snapshots/hacl-c).
To build the library, you need a modern C compiler (preferably GCC-7).
[INSTALL.md]: https://github.com/mitls/hacl-star/INSTALL.md
# Verifying and Building HACL*
Type `make` to get more information:
```
HACL* Makefile:
If you want to run and test the C library:
- 'make build' will generate a shared library from the hacl-c snapshot (no verification)
- 'make unit-tests' will run tests on the library built rom the hacl-c snapshot (no verification)
- 'make clean-build' will clean 'build' artifacts
If you want to verify the F* code and regenerate the C library:
- 'make prepare' will try to install F* and Kremlin (still has some prerequisites)
- 'make verify' will run F* verification on all specs, code and secure-api directories
- 'make extract' will generate all the C code into a snapshot and test it (no verification)
- 'make test-all' will generate and test everything (no verification)
- 'make world' will run everything (except make prepare)
- 'make clean' will remove all artifacts created by other targets
```
Verification and C code generation requires [F\*] and [KreMLin].
Benchmarking performance in `test-all` requires [openssl] and [libsodium].
An additional CMake build is available and can be run with `make build-cmake`.
# Performance
To measure see the performance of HACL* primitives on your platform and C compiler,
run the targets from `test/Makefile` if you have the dependencies installed. (experimental)
To compare its performance with the C reference code (not the assembly versions) in [libsodium] and [openssl],
download and compile [libsodium] with the `--disable-asm` flag and [openssl] with the `-no-asm` flag.
While HACL* is typically as fast as hand-written C code, it is typically 1.1-5.7x slower than
assembly code in our experiments. In the future, we hope to close this gap by using verified assembly implementations
like [Vale](https://github.com/project-everest/vale) for some primitives.
[openssl]: https://github.com/openssl/openssl
[libsodium]: https://github.com/jedisct1/libsodium
# Experimental features
The [code/experimental](code/experimental) directory includes other (partially verified) cryptographic primitives that will become part of the library in the near future:
* Encryption: AES-128, AES-256
* MACs: GCM
* Key Derivation: HKDF
* Signatures: RSA-PSS
We are also working on a JavaScript backend for F* that would enable us to extract HACL* as a JavaScript library.
# Authors and Maintainers
HACL* was originially developed as part of the Ph.D. thesis of Jean Karim Zinzindohoué
in the [Prosecco](http://prosecco.inria.fr) team at [INRIA Paris](https://www.inria.fr/en/centre/paris).
It contains contributions from many researchers at INRIA and Microsoft Research, and is
being actively developed and maintained within [Project Everest].
For questions and comments, or if you want to contribute to the project, do contact the current maintainers at:
* Benjamin Beurdouche (benjamin.beurdouche@inria.fr)
* Karthikeyan Bhargavan (karthikeyan.bhargavan@inria.fr)
sw/airborne/modules/datalink/hacl-c/SHA2_256.c
+311
View File
@@ -0,0 +1,311 @@
#include "SHA2_256.h"
static void
Hacl_Hash_Lib_LoadStore_uint32s_from_be_bytes(uint32_t *output, uint8_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t *x0 = input + (uint32_t )4 * i;
uint32_t inputi = load32_be(x0);
output[i] = inputi;
}
}
static void
Hacl_Hash_Lib_LoadStore_uint32s_to_be_bytes(uint8_t *output, uint32_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint32_t hd1 = input[i];
uint8_t *x0 = output + (uint32_t )4 * i;
store32_be(x0, hd1);
}
}
static void Hacl_Hash_SHA2_256_init(uint32_t *state)
{
(void )(state + (uint32_t )136);
uint32_t *k1 = state;
uint32_t *h_01 = state + (uint32_t )128;
uint32_t *p10 = k1;
uint32_t *p20 = k1 + (uint32_t )16;
uint32_t *p3 = k1 + (uint32_t )32;
uint32_t *p4 = k1 + (uint32_t )48;
uint32_t *p11 = p10;
uint32_t *p21 = p10 + (uint32_t )8;
uint32_t *p12 = p11;
uint32_t *p22 = p11 + (uint32_t )4;
p12[0] = (uint32_t )0x428a2f98;
p12[1] = (uint32_t )0x71374491;
p12[2] = (uint32_t )0xb5c0fbcf;
p12[3] = (uint32_t )0xe9b5dba5;
p22[0] = (uint32_t )0x3956c25b;
p22[1] = (uint32_t )0x59f111f1;
p22[2] = (uint32_t )0x923f82a4;
p22[3] = (uint32_t )0xab1c5ed5;
uint32_t *p13 = p21;
uint32_t *p23 = p21 + (uint32_t )4;
p13[0] = (uint32_t )0xd807aa98;
p13[1] = (uint32_t )0x12835b01;
p13[2] = (uint32_t )0x243185be;
p13[3] = (uint32_t )0x550c7dc3;
p23[0] = (uint32_t )0x72be5d74;
p23[1] = (uint32_t )0x80deb1fe;
p23[2] = (uint32_t )0x9bdc06a7;
p23[3] = (uint32_t )0xc19bf174;
uint32_t *p14 = p20;
uint32_t *p24 = p20 + (uint32_t )8;
uint32_t *p15 = p14;
uint32_t *p25 = p14 + (uint32_t )4;
p15[0] = (uint32_t )0xe49b69c1;
p15[1] = (uint32_t )0xefbe4786;
p15[2] = (uint32_t )0x0fc19dc6;
p15[3] = (uint32_t )0x240ca1cc;
p25[0] = (uint32_t )0x2de92c6f;
p25[1] = (uint32_t )0x4a7484aa;
p25[2] = (uint32_t )0x5cb0a9dc;
p25[3] = (uint32_t )0x76f988da;
uint32_t *p16 = p24;
uint32_t *p26 = p24 + (uint32_t )4;
p16[0] = (uint32_t )0x983e5152;
p16[1] = (uint32_t )0xa831c66d;
p16[2] = (uint32_t )0xb00327c8;
p16[3] = (uint32_t )0xbf597fc7;
p26[0] = (uint32_t )0xc6e00bf3;
p26[1] = (uint32_t )0xd5a79147;
p26[2] = (uint32_t )0x06ca6351;
p26[3] = (uint32_t )0x14292967;
uint32_t *p17 = p3;
uint32_t *p27 = p3 + (uint32_t )8;
uint32_t *p18 = p17;
uint32_t *p28 = p17 + (uint32_t )4;
p18[0] = (uint32_t )0x27b70a85;
p18[1] = (uint32_t )0x2e1b2138;
p18[2] = (uint32_t )0x4d2c6dfc;
p18[3] = (uint32_t )0x53380d13;
p28[0] = (uint32_t )0x650a7354;
p28[1] = (uint32_t )0x766a0abb;
p28[2] = (uint32_t )0x81c2c92e;
p28[3] = (uint32_t )0x92722c85;
uint32_t *p19 = p27;
uint32_t *p29 = p27 + (uint32_t )4;
p19[0] = (uint32_t )0xa2bfe8a1;
p19[1] = (uint32_t )0xa81a664b;
p19[2] = (uint32_t )0xc24b8b70;
p19[3] = (uint32_t )0xc76c51a3;
p29[0] = (uint32_t )0xd192e819;
p29[1] = (uint32_t )0xd6990624;
p29[2] = (uint32_t )0xf40e3585;
p29[3] = (uint32_t )0x106aa070;
uint32_t *p110 = p4;
uint32_t *p210 = p4 + (uint32_t )8;
uint32_t *p1 = p110;
uint32_t *p211 = p110 + (uint32_t )4;
p1[0] = (uint32_t )0x19a4c116;
p1[1] = (uint32_t )0x1e376c08;
p1[2] = (uint32_t )0x2748774c;
p1[3] = (uint32_t )0x34b0bcb5;
p211[0] = (uint32_t )0x391c0cb3;
p211[1] = (uint32_t )0x4ed8aa4a;
p211[2] = (uint32_t )0x5b9cca4f;
p211[3] = (uint32_t )0x682e6ff3;
uint32_t *p111 = p210;
uint32_t *p212 = p210 + (uint32_t )4;
p111[0] = (uint32_t )0x748f82ee;
p111[1] = (uint32_t )0x78a5636f;
p111[2] = (uint32_t )0x84c87814;
p111[3] = (uint32_t )0x8cc70208;
p212[0] = (uint32_t )0x90befffa;
p212[1] = (uint32_t )0xa4506ceb;
p212[2] = (uint32_t )0xbef9a3f7;
p212[3] = (uint32_t )0xc67178f2;
uint32_t *p112 = h_01;
uint32_t *p2 = h_01 + (uint32_t )4;
p112[0] = (uint32_t )0x6a09e667;
p112[1] = (uint32_t )0xbb67ae85;
p112[2] = (uint32_t )0x3c6ef372;
p112[3] = (uint32_t )0xa54ff53a;
p2[0] = (uint32_t )0x510e527f;
p2[1] = (uint32_t )0x9b05688c;
p2[2] = (uint32_t )0x1f83d9ab;
p2[3] = (uint32_t )0x5be0cd19;
}
static void Hacl_Hash_SHA2_256_update(uint32_t *state, uint8_t *data)
{
uint32_t data_w[16] = { 0 };
Hacl_Hash_Lib_LoadStore_uint32s_from_be_bytes(data_w, data, (uint32_t )16);
uint32_t *hash_w = state + (uint32_t )128;
uint32_t *ws_w = state + (uint32_t )64;
uint32_t *k_w = state;
uint32_t *counter_w = state + (uint32_t )136;
for (uint32_t i = (uint32_t )0; i < (uint32_t )16; i = i + (uint32_t )1)
{
uint32_t uu____206 = data_w[i];
ws_w[i] = uu____206;
}
for (uint32_t i = (uint32_t )16; i < (uint32_t )64; i = i + (uint32_t )1)
{
uint32_t t16 = ws_w[i - (uint32_t )16];
uint32_t t15 = ws_w[i - (uint32_t )15];
uint32_t t7 = ws_w[i - (uint32_t )7];
uint32_t t2 = ws_w[i - (uint32_t )2];
ws_w[i] =
((t2 >> (uint32_t )17 | t2 << (uint32_t )32 - (uint32_t )17)
^ (t2 >> (uint32_t )19 | t2 << (uint32_t )32 - (uint32_t )19) ^ t2 >> (uint32_t )10)
+
t7
+
((t15 >> (uint32_t )7 | t15 << (uint32_t )32 - (uint32_t )7)
^ (t15 >> (uint32_t )18 | t15 << (uint32_t )32 - (uint32_t )18) ^ t15 >> (uint32_t )3)
+ t16;
}
uint32_t hash_0[8] = { 0 };
memcpy(hash_0, hash_w, (uint32_t )8 * sizeof hash_w[0]);
for (uint32_t i = (uint32_t )0; i < (uint32_t )64; i = i + (uint32_t )1)
{
uint32_t a = hash_0[0];
uint32_t b = hash_0[1];
uint32_t c = hash_0[2];
uint32_t d = hash_0[3];
uint32_t e = hash_0[4];
uint32_t f1 = hash_0[5];
uint32_t g = hash_0[6];
uint32_t h = hash_0[7];
uint32_t kt = k_w[i];
uint32_t wst = ws_w[i];
uint32_t
t1 =
h
+
((e >> (uint32_t )6 | e << (uint32_t )32 - (uint32_t )6)
^
(e >> (uint32_t )11 | e << (uint32_t )32 - (uint32_t )11)
^ (e >> (uint32_t )25 | e << (uint32_t )32 - (uint32_t )25))
+ (e & f1 ^ ~e & g)
+ kt
+ wst;
uint32_t
t2 =
((a >> (uint32_t )2 | a << (uint32_t )32 - (uint32_t )2)
^
(a >> (uint32_t )13 | a << (uint32_t )32 - (uint32_t )13)
^ (a >> (uint32_t )22 | a << (uint32_t )32 - (uint32_t )22))
+ (a & b ^ a & c ^ b & c);
uint32_t x1 = t1 + t2;
uint32_t x5 = d + t1;
uint32_t *p1 = hash_0;
uint32_t *p2 = hash_0 + (uint32_t )4;
p1[0] = x1;
p1[1] = a;
p1[2] = b;
p1[3] = c;
p2[0] = x5;
p2[1] = e;
p2[2] = f1;
p2[3] = g;
}
for (uint32_t i = (uint32_t )0; i < (uint32_t )8; i = i + (uint32_t )1)
{
uint32_t uu____871 = hash_w[i];
uint32_t uu____874 = hash_0[i];
uint32_t uu____870 = uu____871 + uu____874;
hash_w[i] = uu____870;
}
uint32_t c0 = counter_w[0];
uint32_t one1 = (uint32_t )1;
counter_w[0] = c0 + one1;
}
static void Hacl_Hash_SHA2_256_update_multi(uint32_t *state, uint8_t *data, uint32_t n1)
{
for (uint32_t i = (uint32_t )0; i < n1; i = i + (uint32_t )1)
{
uint8_t *b = data + i * (uint32_t )64;
Hacl_Hash_SHA2_256_update(state, b);
}
}
static void Hacl_Hash_SHA2_256_update_last(uint32_t *state, uint8_t *data, uint32_t len)
{
uint8_t blocks[128] = { 0 };
K___uint32_t_uint8_t_ uu____1925;
if (len < (uint32_t )56)
uu____1925 = ((K___uint32_t_uint8_t_ ){ .fst = (uint32_t )1, .snd = blocks + (uint32_t )64 });
else
uu____1925 = ((K___uint32_t_uint8_t_ ){ .fst = (uint32_t )2, .snd = blocks });
K___uint32_t_uint8_t_ scrut = uu____1925;
uint32_t nb = scrut.fst;
uint8_t *final_blocks = scrut.snd;
memcpy(final_blocks, data, len * sizeof data[0]);
uint32_t n1 = state[136];
uint8_t *padding = final_blocks + len;
uint32_t
pad0len = ((uint32_t )64 - (len + (uint32_t )8 + (uint32_t )1) % (uint32_t )64) % (uint32_t )64;
uint8_t *buf1 = padding;
(void )(padding + (uint32_t )1);
uint8_t *buf2 = padding + (uint32_t )1 + pad0len;
uint64_t
encodedlen =
((uint64_t )n1 * (uint64_t )(uint32_t )64 + (uint64_t )len)
* (uint64_t )(uint32_t )8;
buf1[0] = (uint8_t )0x80;
store64_be(buf2, encodedlen);
Hacl_Hash_SHA2_256_update_multi(state, final_blocks, nb);
}
static void Hacl_Hash_SHA2_256_finish(uint32_t *state, uint8_t *hash1)
{
uint32_t *hash_w = state + (uint32_t )128;
Hacl_Hash_Lib_LoadStore_uint32s_to_be_bytes(hash1, hash_w, (uint32_t )8);
}
static void Hacl_Hash_SHA2_256_hash(uint8_t *hash1, uint8_t *input, uint32_t len)
{
uint32_t state[137] = { 0 };
uint32_t n1 = len / (uint32_t )64;
uint32_t r = len % (uint32_t )64;
uint8_t *input_blocks = input;
uint8_t *input_last = input + n1 * (uint32_t )64;
Hacl_Hash_SHA2_256_init(state);
Hacl_Hash_SHA2_256_update_multi(state, input_blocks, n1);
Hacl_Hash_SHA2_256_update_last(state, input_last, r);
Hacl_Hash_SHA2_256_finish(state, hash1);
}
uint32_t SHA2_256_size_hash = (uint32_t )32;
uint32_t SHA2_256_size_block = (uint32_t )64;
uint32_t SHA2_256_size_state = (uint32_t )137;
void SHA2_256_init(uint32_t *state)
{
Hacl_Hash_SHA2_256_init(state);
}
void SHA2_256_update(uint32_t *state, uint8_t *data_8)
{
Hacl_Hash_SHA2_256_update(state, data_8);
}
void SHA2_256_update_multi(uint32_t *state, uint8_t *data, uint32_t n1)
{
Hacl_Hash_SHA2_256_update_multi(state, data, n1);
}
void SHA2_256_update_last(uint32_t *state, uint8_t *data, uint32_t len)
{
Hacl_Hash_SHA2_256_update_last(state, data, len);
}
void SHA2_256_finish(uint32_t *state, uint8_t *hash1)
{
Hacl_Hash_SHA2_256_finish(state, hash1);
}
void SHA2_256_hash(uint8_t *hash1, uint8_t *input, uint32_t len)
{
Hacl_Hash_SHA2_256_hash(hash1, input, len);
}
sw/airborne/modules/datalink/hacl-c/SHA2_256.h
+84
View File
@@ -0,0 +1,84 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __SHA2_256_H
#define __SHA2_256_H
#include "testlib.h"
typedef uint8_t Hacl_Hash_Lib_Create_uint8_t;
typedef uint32_t Hacl_Hash_Lib_Create_uint32_t;
typedef uint64_t Hacl_Hash_Lib_Create_uint64_t;
typedef uint8_t Hacl_Hash_Lib_Create_uint8_ht;
typedef uint32_t Hacl_Hash_Lib_Create_uint32_ht;
typedef uint64_t Hacl_Hash_Lib_Create_uint64_ht;
typedef uint8_t *Hacl_Hash_Lib_Create_uint8_p;
typedef uint32_t *Hacl_Hash_Lib_Create_uint32_p;
typedef uint64_t *Hacl_Hash_Lib_Create_uint64_p;
typedef uint8_t *Hacl_Hash_Lib_LoadStore_uint8_p;
typedef uint8_t Hacl_Hash_SHA2_256_uint8_t;
typedef uint32_t Hacl_Hash_SHA2_256_uint32_t;
typedef uint64_t Hacl_Hash_SHA2_256_uint64_t;
typedef uint8_t Hacl_Hash_SHA2_256_uint8_ht;
typedef uint32_t Hacl_Hash_SHA2_256_uint32_ht;
typedef uint64_t Hacl_Hash_SHA2_256_uint64_ht;
typedef uint32_t *Hacl_Hash_SHA2_256_uint32_p;
typedef uint8_t *Hacl_Hash_SHA2_256_uint8_p;
typedef struct
{
uint32_t fst;
uint8_t *snd;
}
K___uint32_t_uint8_t_;
typedef uint8_t SHA2_256_uint8_t;
typedef uint32_t SHA2_256_uint32_t;
typedef uint64_t SHA2_256_uint64_t;
typedef uint8_t SHA2_256_uint8_ht;
typedef uint32_t SHA2_256_uint32_ht;
typedef uint32_t *SHA2_256_uint32_p;
typedef uint8_t *SHA2_256_uint8_p;
extern uint32_t SHA2_256_size_hash;
extern uint32_t SHA2_256_size_block;
extern uint32_t SHA2_256_size_state;
void SHA2_256_init(uint32_t *state);
void SHA2_256_update(uint32_t *state, uint8_t *data_8);
void SHA2_256_update_multi(uint32_t *state, uint8_t *data, uint32_t n1);
void SHA2_256_update_last(uint32_t *state, uint8_t *data, uint32_t len);
void SHA2_256_finish(uint32_t *state, uint8_t *hash1);
void SHA2_256_hash(uint8_t *hash1, uint8_t *input, uint32_t len);
#endif
sw/airborne/modules/datalink/hacl-c/SHA2_384.c
+346
View File
@@ -0,0 +1,346 @@
#include "SHA2_384.h"
static void
Hacl_Hash_Lib_LoadStore_uint64s_from_be_bytes(uint64_t *output, uint8_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t *x0 = input + (uint32_t )8 * i;
uint64_t inputi = load64_be(x0);
output[i] = inputi;
}
}
static void
Hacl_Hash_Lib_LoadStore_uint64s_to_be_bytes(uint8_t *output, uint64_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint64_t hd1 = input[i];
uint8_t *x0 = output + (uint32_t )8 * i;
store64_be(x0, hd1);
}
}
static void Hacl_Hash_SHA2_384_init(uint64_t *state)
{
(void )(state + (uint32_t )168);
uint64_t *k1 = state;
uint64_t *h_01 = state + (uint32_t )160;
uint64_t *p10 = k1;
uint64_t *p20 = k1 + (uint32_t )16;
uint64_t *p3 = k1 + (uint32_t )32;
uint64_t *p4 = k1 + (uint32_t )48;
uint64_t *p5 = k1 + (uint32_t )64;
uint64_t *p11 = p10;
uint64_t *p21 = p10 + (uint32_t )8;
uint64_t *p12 = p11;
uint64_t *p22 = p11 + (uint32_t )4;
p12[0] = (uint64_t )0x428a2f98d728ae22;
p12[1] = (uint64_t )0x7137449123ef65cd;
p12[2] = (uint64_t )0xb5c0fbcfec4d3b2f;
p12[3] = (uint64_t )0xe9b5dba58189dbbc;
p22[0] = (uint64_t )0x3956c25bf348b538;
p22[1] = (uint64_t )0x59f111f1b605d019;
p22[2] = (uint64_t )0x923f82a4af194f9b;
p22[3] = (uint64_t )0xab1c5ed5da6d8118;
uint64_t *p13 = p21;
uint64_t *p23 = p21 + (uint32_t )4;
p13[0] = (uint64_t )0xd807aa98a3030242;
p13[1] = (uint64_t )0x12835b0145706fbe;
p13[2] = (uint64_t )0x243185be4ee4b28c;
p13[3] = (uint64_t )0x550c7dc3d5ffb4e2;
p23[0] = (uint64_t )0x72be5d74f27b896f;
p23[1] = (uint64_t )0x80deb1fe3b1696b1;
p23[2] = (uint64_t )0x9bdc06a725c71235;
p23[3] = (uint64_t )0xc19bf174cf692694;
uint64_t *p14 = p20;
uint64_t *p24 = p20 + (uint32_t )8;
uint64_t *p15 = p14;
uint64_t *p25 = p14 + (uint32_t )4;
p15[0] = (uint64_t )0xe49b69c19ef14ad2;
p15[1] = (uint64_t )0xefbe4786384f25e3;
p15[2] = (uint64_t )0x0fc19dc68b8cd5b5;
p15[3] = (uint64_t )0x240ca1cc77ac9c65;
p25[0] = (uint64_t )0x2de92c6f592b0275;
p25[1] = (uint64_t )0x4a7484aa6ea6e483;
p25[2] = (uint64_t )0x5cb0a9dcbd41fbd4;
p25[3] = (uint64_t )0x76f988da831153b5;
uint64_t *p16 = p24;
uint64_t *p26 = p24 + (uint32_t )4;
p16[0] = (uint64_t )0x983e5152ee66dfab;
p16[1] = (uint64_t )0xa831c66d2db43210;
p16[2] = (uint64_t )0xb00327c898fb213f;
p16[3] = (uint64_t )0xbf597fc7beef0ee4;
p26[0] = (uint64_t )0xc6e00bf33da88fc2;
p26[1] = (uint64_t )0xd5a79147930aa725;
p26[2] = (uint64_t )0x06ca6351e003826f;
p26[3] = (uint64_t )0x142929670a0e6e70;
uint64_t *p17 = p3;
uint64_t *p27 = p3 + (uint32_t )8;
uint64_t *p18 = p17;
uint64_t *p28 = p17 + (uint32_t )4;
p18[0] = (uint64_t )0x27b70a8546d22ffc;
p18[1] = (uint64_t )0x2e1b21385c26c926;
p18[2] = (uint64_t )0x4d2c6dfc5ac42aed;
p18[3] = (uint64_t )0x53380d139d95b3df;
p28[0] = (uint64_t )0x650a73548baf63de;
p28[1] = (uint64_t )0x766a0abb3c77b2a8;
p28[2] = (uint64_t )0x81c2c92e47edaee6;
p28[3] = (uint64_t )0x92722c851482353b;
uint64_t *p19 = p27;
uint64_t *p29 = p27 + (uint32_t )4;
p19[0] = (uint64_t )0xa2bfe8a14cf10364;
p19[1] = (uint64_t )0xa81a664bbc423001;
p19[2] = (uint64_t )0xc24b8b70d0f89791;
p19[3] = (uint64_t )0xc76c51a30654be30;
p29[0] = (uint64_t )0xd192e819d6ef5218;
p29[1] = (uint64_t )0xd69906245565a910;
p29[2] = (uint64_t )0xf40e35855771202a;
p29[3] = (uint64_t )0x106aa07032bbd1b8;
uint64_t *p110 = p4;
uint64_t *p210 = p4 + (uint32_t )8;
uint64_t *p111 = p110;
uint64_t *p211 = p110 + (uint32_t )4;
p111[0] = (uint64_t )0x19a4c116b8d2d0c8;
p111[1] = (uint64_t )0x1e376c085141ab53;
p111[2] = (uint64_t )0x2748774cdf8eeb99;
p111[3] = (uint64_t )0x34b0bcb5e19b48a8;
p211[0] = (uint64_t )0x391c0cb3c5c95a63;
p211[1] = (uint64_t )0x4ed8aa4ae3418acb;
p211[2] = (uint64_t )0x5b9cca4f7763e373;
p211[3] = (uint64_t )0x682e6ff3d6b2b8a3;
uint64_t *p112 = p210;
uint64_t *p212 = p210 + (uint32_t )4;
p112[0] = (uint64_t )0x748f82ee5defb2fc;
p112[1] = (uint64_t )0x78a5636f43172f60;
p112[2] = (uint64_t )0x84c87814a1f0ab72;
p112[3] = (uint64_t )0x8cc702081a6439ec;
p212[0] = (uint64_t )0x90befffa23631e28;
p212[1] = (uint64_t )0xa4506cebde82bde9;
p212[2] = (uint64_t )0xbef9a3f7b2c67915;
p212[3] = (uint64_t )0xc67178f2e372532b;
uint64_t *p113 = p5;
uint64_t *p213 = p5 + (uint32_t )8;
uint64_t *p1 = p113;
uint64_t *p214 = p113 + (uint32_t )4;
p1[0] = (uint64_t )0xca273eceea26619c;
p1[1] = (uint64_t )0xd186b8c721c0c207;
p1[2] = (uint64_t )0xeada7dd6cde0eb1e;
p1[3] = (uint64_t )0xf57d4f7fee6ed178;
p214[0] = (uint64_t )0x06f067aa72176fba;
p214[1] = (uint64_t )0x0a637dc5a2c898a6;
p214[2] = (uint64_t )0x113f9804bef90dae;
p214[3] = (uint64_t )0x1b710b35131c471b;
uint64_t *p114 = p213;
uint64_t *p215 = p213 + (uint32_t )4;
p114[0] = (uint64_t )0x28db77f523047d84;
p114[1] = (uint64_t )0x32caab7b40c72493;
p114[2] = (uint64_t )0x3c9ebe0a15c9bebc;
p114[3] = (uint64_t )0x431d67c49c100d4c;
p215[0] = (uint64_t )0x4cc5d4becb3e42b6;
p215[1] = (uint64_t )0x597f299cfc657e2a;
p215[2] = (uint64_t )0x5fcb6fab3ad6faec;
p215[3] = (uint64_t )0x6c44198c4a475817;
uint64_t *p115 = h_01;
uint64_t *p2 = h_01 + (uint32_t )4;
p115[0] = (uint64_t )0xcbbb9d5dc1059ed8;
p115[1] = (uint64_t )0x629a292a367cd507;
p115[2] = (uint64_t )0x9159015a3070dd17;
p115[3] = (uint64_t )0x152fecd8f70e5939;
p2[0] = (uint64_t )0x67332667ffc00b31;
p2[1] = (uint64_t )0x8eb44a8768581511;
p2[2] = (uint64_t )0xdb0c2e0d64f98fa7;
p2[3] = (uint64_t )0x47b5481dbefa4fa4;
}
static void Hacl_Hash_SHA2_384_update(uint64_t *state, uint8_t *data)
{
KRML_CHECK_SIZE((uint64_t )(uint32_t )0, (uint32_t )16);
uint64_t data_w[16];
for (uintmax_t _i = 0; _i < (uint32_t )16; ++_i)
data_w[_i] = (uint64_t )(uint32_t )0;
Hacl_Hash_Lib_LoadStore_uint64s_from_be_bytes(data_w, data, (uint32_t )16);
uint64_t *hash_w = state + (uint32_t )160;
uint64_t *ws_w = state + (uint32_t )80;
uint64_t *k_w = state;
uint64_t *counter_w = state + (uint32_t )168;
for (uint32_t i = (uint32_t )0; i < (uint32_t )16; i = i + (uint32_t )1)
{
uint64_t uu____242 = data_w[i];
ws_w[i] = uu____242;
}
for (uint32_t i = (uint32_t )16; i < (uint32_t )80; i = i + (uint32_t )1)
{
uint64_t t16 = ws_w[i - (uint32_t )16];
uint64_t t15 = ws_w[i - (uint32_t )15];
uint64_t t7 = ws_w[i - (uint32_t )7];
uint64_t t2 = ws_w[i - (uint32_t )2];
ws_w[i] =
((t2 >> (uint32_t )19 | t2 << (uint32_t )64 - (uint32_t )19)
^ (t2 >> (uint32_t )61 | t2 << (uint32_t )64 - (uint32_t )61) ^ t2 >> (uint32_t )6)
+
t7
+
((t15 >> (uint32_t )1 | t15 << (uint32_t )64 - (uint32_t )1)
^ (t15 >> (uint32_t )8 | t15 << (uint32_t )64 - (uint32_t )8) ^ t15 >> (uint32_t )7)
+ t16;
}
uint64_t hash_0[8] = { 0 };
memcpy(hash_0, hash_w, (uint32_t )8 * sizeof hash_w[0]);
for (uint32_t i = (uint32_t )0; i < (uint32_t )80; i = i + (uint32_t )1)
{
uint64_t a = hash_0[0];
uint64_t b = hash_0[1];
uint64_t c = hash_0[2];
uint64_t d = hash_0[3];
uint64_t e = hash_0[4];
uint64_t f1 = hash_0[5];
uint64_t g = hash_0[6];
uint64_t h = hash_0[7];
uint64_t k_t = k_w[i];
uint64_t ws_t = ws_w[i];
uint64_t
t1 =
h
+
((e >> (uint32_t )14 | e << (uint32_t )64 - (uint32_t )14)
^
(e >> (uint32_t )18 | e << (uint32_t )64 - (uint32_t )18)
^ (e >> (uint32_t )41 | e << (uint32_t )64 - (uint32_t )41))
+ (e & f1 ^ ~e & g)
+ k_t
+ ws_t;
uint64_t
t2 =
((a >> (uint32_t )28 | a << (uint32_t )64 - (uint32_t )28)
^
(a >> (uint32_t )34 | a << (uint32_t )64 - (uint32_t )34)
^ (a >> (uint32_t )39 | a << (uint32_t )64 - (uint32_t )39))
+ (a & b ^ a & c ^ b & c);
uint64_t x1 = t1 + t2;
uint64_t x5 = d + t1;
uint64_t *p1 = hash_0;
uint64_t *p2 = hash_0 + (uint32_t )4;
p1[0] = x1;
p1[1] = a;
p1[2] = b;
p1[3] = c;
p2[0] = x5;
p2[1] = e;
p2[2] = f1;
p2[3] = g;
}
for (uint32_t i = (uint32_t )0; i < (uint32_t )8; i = i + (uint32_t )1)
{
uint64_t uu____871 = hash_w[i];
uint64_t uu____874 = hash_0[i];
uint64_t uu____870 = uu____871 + uu____874;
hash_w[i] = uu____870;
}
uint64_t c0 = counter_w[0];
uint64_t one1 = (uint64_t )(uint32_t )1;
counter_w[0] = c0 + one1;
}
static void Hacl_Hash_SHA2_384_update_multi(uint64_t *state, uint8_t *data, uint32_t n1)
{
for (uint32_t i = (uint32_t )0; i < n1; i = i + (uint32_t )1)
{
uint8_t *b = data + i * (uint32_t )128;
Hacl_Hash_SHA2_384_update(state, b);
}
}
static void Hacl_Hash_SHA2_384_update_last(uint64_t *state, uint8_t *data, uint64_t len)
{
uint8_t blocks[256] = { 0 };
uint32_t nb;
if (len < (uint64_t )112)
nb = (uint32_t )1;
else
nb = (uint32_t )2;
uint8_t *final_blocks;
if (len < (uint64_t )112)
final_blocks = blocks + (uint32_t )128;
else
final_blocks = blocks;
memcpy(final_blocks, data, (uint32_t )len * sizeof data[0]);
uint64_t n1 = state[168];
uint8_t *padding = final_blocks + (uint32_t )len;
FStar_UInt128_t
encodedlen =
FStar_UInt128_shift_left(FStar_UInt128_add(FStar_UInt128_mul_wide(n1,
(uint64_t )(uint32_t )128),
FStar_Int_Cast_Full_uint64_to_uint128(len)),
(uint32_t )3);
uint32_t
pad0len =
((uint32_t )128 - ((uint32_t )len + (uint32_t )16 + (uint32_t )1) % (uint32_t )128)
% (uint32_t )128;
uint8_t *buf1 = padding;
(void )(padding + (uint32_t )1);
uint8_t *buf2 = padding + (uint32_t )1 + pad0len;
buf1[0] = (uint8_t )0x80;
store128_be(buf2, encodedlen);
Hacl_Hash_SHA2_384_update_multi(state, final_blocks, nb);
}
static void Hacl_Hash_SHA2_384_finish(uint64_t *state, uint8_t *hash1)
{
uint64_t *hash_w = state + (uint32_t )160;
Hacl_Hash_Lib_LoadStore_uint64s_to_be_bytes(hash1, hash_w, (uint32_t )6);
}
static void Hacl_Hash_SHA2_384_hash(uint8_t *hash1, uint8_t *input, uint32_t len)
{
KRML_CHECK_SIZE((uint64_t )(uint32_t )0, (uint32_t )169);
uint64_t state[169];
for (uintmax_t _i = 0; _i < (uint32_t )169; ++_i)
state[_i] = (uint64_t )(uint32_t )0;
uint32_t n1 = len / (uint32_t )128;
uint32_t r = len % (uint32_t )128;
uint8_t *input_blocks = input;
uint8_t *input_last = input + n1 * (uint32_t )128;
Hacl_Hash_SHA2_384_init(state);
Hacl_Hash_SHA2_384_update_multi(state, input_blocks, n1);
Hacl_Hash_SHA2_384_update_last(state, input_last, (uint64_t )r);
Hacl_Hash_SHA2_384_finish(state, hash1);
}
uint32_t SHA2_384_size_hash = (uint32_t )48;
uint32_t SHA2_384_size_block = (uint32_t )128;
uint32_t SHA2_384_size_state = (uint32_t )169;
void SHA2_384_init(uint64_t *state)
{
Hacl_Hash_SHA2_384_init(state);
}
void SHA2_384_update(uint64_t *state, uint8_t *data_8)
{
Hacl_Hash_SHA2_384_update(state, data_8);
}
void SHA2_384_update_multi(uint64_t *state, uint8_t *data, uint32_t n1)
{
Hacl_Hash_SHA2_384_update_multi(state, data, n1);
}
void SHA2_384_update_last(uint64_t *state, uint8_t *data, uint64_t len)
{
Hacl_Hash_SHA2_384_update_last(state, data, len);
}
void SHA2_384_finish(uint64_t *state, uint8_t *hash1)
{
Hacl_Hash_SHA2_384_finish(state, hash1);
}
void SHA2_384_hash(uint8_t *hash1, uint8_t *input, uint32_t len)
{
Hacl_Hash_SHA2_384_hash(hash1, input, len);
}
sw/airborne/modules/datalink/hacl-c/SHA2_384.h
+79
View File
@@ -0,0 +1,79 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __SHA2_384_H
#define __SHA2_384_H
#include "testlib.h"
typedef uint8_t Hacl_Hash_Lib_Create_uint8_t;
typedef uint32_t Hacl_Hash_Lib_Create_uint32_t;
typedef uint64_t Hacl_Hash_Lib_Create_uint64_t;
typedef uint8_t Hacl_Hash_Lib_Create_uint8_ht;
typedef uint32_t Hacl_Hash_Lib_Create_uint32_ht;
typedef uint64_t Hacl_Hash_Lib_Create_uint64_ht;
typedef uint8_t *Hacl_Hash_Lib_Create_uint8_p;
typedef uint32_t *Hacl_Hash_Lib_Create_uint32_p;
typedef uint64_t *Hacl_Hash_Lib_Create_uint64_p;
typedef uint8_t *Hacl_Hash_Lib_LoadStore_uint8_p;
typedef uint8_t Hacl_Hash_SHA2_384_uint8_t;
typedef uint32_t Hacl_Hash_SHA2_384_uint32_t;
typedef uint64_t Hacl_Hash_SHA2_384_uint64_t;
typedef uint8_t Hacl_Hash_SHA2_384_uint8_ht;
typedef uint32_t Hacl_Hash_SHA2_384_uint32_ht;
typedef uint64_t Hacl_Hash_SHA2_384_uint64_ht;
typedef FStar_UInt128_t Hacl_Hash_SHA2_384_uint128_ht;
typedef uint64_t *Hacl_Hash_SHA2_384_uint64_p;
typedef uint8_t *Hacl_Hash_SHA2_384_uint8_p;
typedef uint8_t SHA2_384_uint8_t;
typedef uint32_t SHA2_384_uint32_t;
typedef uint64_t SHA2_384_uint64_t;
typedef uint8_t SHA2_384_uint8_ht;
typedef uint64_t SHA2_384_uint64_ht;
typedef uint64_t *SHA2_384_uint64_p;
typedef uint8_t *SHA2_384_uint8_p;
extern uint32_t SHA2_384_size_hash;
extern uint32_t SHA2_384_size_block;
extern uint32_t SHA2_384_size_state;
void SHA2_384_init(uint64_t *state);
void SHA2_384_update(uint64_t *state, uint8_t *data_8);
void SHA2_384_update_multi(uint64_t *state, uint8_t *data, uint32_t n1);
void SHA2_384_update_last(uint64_t *state, uint8_t *data, uint64_t len);
void SHA2_384_finish(uint64_t *state, uint8_t *hash1);
void SHA2_384_hash(uint8_t *hash1, uint8_t *input, uint32_t len);
#endif
sw/airborne/modules/datalink/hacl-c/SHA2_512.c
+368
View File
@@ -0,0 +1,368 @@
#include "SHA2_512.h"
static void
Hacl_Hash_Lib_LoadStore_uint64s_from_be_bytes(uint64_t *output, uint8_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t *x0 = input + (uint32_t )8 * i;
uint64_t inputi = load64_be(x0);
output[i] = inputi;
}
}
static void
Hacl_Hash_Lib_LoadStore_uint64s_to_be_bytes(uint8_t *output, uint64_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint64_t hd1 = input[i];
uint8_t *x0 = output + (uint32_t )8 * i;
store64_be(x0, hd1);
}
}
static void Hacl_Hash_SHA2_512_init(uint64_t *state)
{
(void )(state + (uint32_t )168);
uint64_t *k1 = state;
uint64_t *h_01 = state + (uint32_t )160;
uint64_t *p10 = k1;
uint64_t *p20 = k1 + (uint32_t )16;
uint64_t *p3 = k1 + (uint32_t )32;
uint64_t *p4 = k1 + (uint32_t )48;
uint64_t *p5 = k1 + (uint32_t )64;
uint64_t *p11 = p10;
uint64_t *p21 = p10 + (uint32_t )8;
uint64_t *p12 = p11;
uint64_t *p22 = p11 + (uint32_t )4;
p12[0] = (uint64_t )0x428a2f98d728ae22;
p12[1] = (uint64_t )0x7137449123ef65cd;
p12[2] = (uint64_t )0xb5c0fbcfec4d3b2f;
p12[3] = (uint64_t )0xe9b5dba58189dbbc;
p22[0] = (uint64_t )0x3956c25bf348b538;
p22[1] = (uint64_t )0x59f111f1b605d019;
p22[2] = (uint64_t )0x923f82a4af194f9b;
p22[3] = (uint64_t )0xab1c5ed5da6d8118;
uint64_t *p13 = p21;
uint64_t *p23 = p21 + (uint32_t )4;
p13[0] = (uint64_t )0xd807aa98a3030242;
p13[1] = (uint64_t )0x12835b0145706fbe;
p13[2] = (uint64_t )0x243185be4ee4b28c;
p13[3] = (uint64_t )0x550c7dc3d5ffb4e2;
p23[0] = (uint64_t )0x72be5d74f27b896f;
p23[1] = (uint64_t )0x80deb1fe3b1696b1;
p23[2] = (uint64_t )0x9bdc06a725c71235;
p23[3] = (uint64_t )0xc19bf174cf692694;
uint64_t *p14 = p20;
uint64_t *p24 = p20 + (uint32_t )8;
uint64_t *p15 = p14;
uint64_t *p25 = p14 + (uint32_t )4;
p15[0] = (uint64_t )0xe49b69c19ef14ad2;
p15[1] = (uint64_t )0xefbe4786384f25e3;
p15[2] = (uint64_t )0x0fc19dc68b8cd5b5;
p15[3] = (uint64_t )0x240ca1cc77ac9c65;
p25[0] = (uint64_t )0x2de92c6f592b0275;
p25[1] = (uint64_t )0x4a7484aa6ea6e483;
p25[2] = (uint64_t )0x5cb0a9dcbd41fbd4;
p25[3] = (uint64_t )0x76f988da831153b5;
uint64_t *p16 = p24;
uint64_t *p26 = p24 + (uint32_t )4;
p16[0] = (uint64_t )0x983e5152ee66dfab;
p16[1] = (uint64_t )0xa831c66d2db43210;
p16[2] = (uint64_t )0xb00327c898fb213f;
p16[3] = (uint64_t )0xbf597fc7beef0ee4;
p26[0] = (uint64_t )0xc6e00bf33da88fc2;
p26[1] = (uint64_t )0xd5a79147930aa725;
p26[2] = (uint64_t )0x06ca6351e003826f;
p26[3] = (uint64_t )0x142929670a0e6e70;
uint64_t *p17 = p3;
uint64_t *p27 = p3 + (uint32_t )8;
uint64_t *p18 = p17;
uint64_t *p28 = p17 + (uint32_t )4;
p18[0] = (uint64_t )0x27b70a8546d22ffc;
p18[1] = (uint64_t )0x2e1b21385c26c926;
p18[2] = (uint64_t )0x4d2c6dfc5ac42aed;
p18[3] = (uint64_t )0x53380d139d95b3df;
p28[0] = (uint64_t )0x650a73548baf63de;
p28[1] = (uint64_t )0x766a0abb3c77b2a8;
p28[2] = (uint64_t )0x81c2c92e47edaee6;
p28[3] = (uint64_t )0x92722c851482353b;
uint64_t *p19 = p27;
uint64_t *p29 = p27 + (uint32_t )4;
p19[0] = (uint64_t )0xa2bfe8a14cf10364;
p19[1] = (uint64_t )0xa81a664bbc423001;
p19[2] = (uint64_t )0xc24b8b70d0f89791;
p19[3] = (uint64_t )0xc76c51a30654be30;
p29[0] = (uint64_t )0xd192e819d6ef5218;
p29[1] = (uint64_t )0xd69906245565a910;
p29[2] = (uint64_t )0xf40e35855771202a;
p29[3] = (uint64_t )0x106aa07032bbd1b8;
uint64_t *p110 = p4;
uint64_t *p210 = p4 + (uint32_t )8;
uint64_t *p111 = p110;
uint64_t *p211 = p110 + (uint32_t )4;
p111[0] = (uint64_t )0x19a4c116b8d2d0c8;
p111[1] = (uint64_t )0x1e376c085141ab53;
p111[2] = (uint64_t )0x2748774cdf8eeb99;
p111[3] = (uint64_t )0x34b0bcb5e19b48a8;
p211[0] = (uint64_t )0x391c0cb3c5c95a63;
p211[1] = (uint64_t )0x4ed8aa4ae3418acb;
p211[2] = (uint64_t )0x5b9cca4f7763e373;
p211[3] = (uint64_t )0x682e6ff3d6b2b8a3;
uint64_t *p112 = p210;
uint64_t *p212 = p210 + (uint32_t )4;
p112[0] = (uint64_t )0x748f82ee5defb2fc;
p112[1] = (uint64_t )0x78a5636f43172f60;
p112[2] = (uint64_t )0x84c87814a1f0ab72;
p112[3] = (uint64_t )0x8cc702081a6439ec;
p212[0] = (uint64_t )0x90befffa23631e28;
p212[1] = (uint64_t )0xa4506cebde82bde9;
p212[2] = (uint64_t )0xbef9a3f7b2c67915;
p212[3] = (uint64_t )0xc67178f2e372532b;
uint64_t *p113 = p5;
uint64_t *p213 = p5 + (uint32_t )8;
uint64_t *p1 = p113;
uint64_t *p214 = p113 + (uint32_t )4;
p1[0] = (uint64_t )0xca273eceea26619c;
p1[1] = (uint64_t )0xd186b8c721c0c207;
p1[2] = (uint64_t )0xeada7dd6cde0eb1e;
p1[3] = (uint64_t )0xf57d4f7fee6ed178;
p214[0] = (uint64_t )0x06f067aa72176fba;
p214[1] = (uint64_t )0x0a637dc5a2c898a6;
p214[2] = (uint64_t )0x113f9804bef90dae;
p214[3] = (uint64_t )0x1b710b35131c471b;
uint64_t *p114 = p213;
uint64_t *p215 = p213 + (uint32_t )4;
p114[0] = (uint64_t )0x28db77f523047d84;
p114[1] = (uint64_t )0x32caab7b40c72493;
p114[2] = (uint64_t )0x3c9ebe0a15c9bebc;
p114[3] = (uint64_t )0x431d67c49c100d4c;
p215[0] = (uint64_t )0x4cc5d4becb3e42b6;
p215[1] = (uint64_t )0x597f299cfc657e2a;
p215[2] = (uint64_t )0x5fcb6fab3ad6faec;
p215[3] = (uint64_t )0x6c44198c4a475817;
uint64_t *p115 = h_01;
uint64_t *p2 = h_01 + (uint32_t )4;
p115[0] = (uint64_t )0x6a09e667f3bcc908;
p115[1] = (uint64_t )0xbb67ae8584caa73b;
p115[2] = (uint64_t )0x3c6ef372fe94f82b;
p115[3] = (uint64_t )0xa54ff53a5f1d36f1;
p2[0] = (uint64_t )0x510e527fade682d1;
p2[1] = (uint64_t )0x9b05688c2b3e6c1f;
p2[2] = (uint64_t )0x1f83d9abfb41bd6b;
p2[3] = (uint64_t )0x5be0cd19137e2179;
}
static void Hacl_Hash_SHA2_512_update(uint64_t *state, uint8_t *data)
{
KRML_CHECK_SIZE((uint64_t )(uint32_t )0, (uint32_t )16);
uint64_t data_w[16];
for (uintmax_t _i = 0; _i < (uint32_t )16; ++_i)
data_w[_i] = (uint64_t )(uint32_t )0;
Hacl_Hash_Lib_LoadStore_uint64s_from_be_bytes(data_w, data, (uint32_t )16);
uint64_t *hash_w = state + (uint32_t )160;
uint64_t *ws_w = state + (uint32_t )80;
uint64_t *k_w = state;
uint64_t *counter_w = state + (uint32_t )168;
for (uint32_t i = (uint32_t )0; i < (uint32_t )16; i = i + (uint32_t )1)
{
uint64_t uu____242 = data_w[i];
ws_w[i] = uu____242;
}
for (uint32_t i = (uint32_t )16; i < (uint32_t )80; i = i + (uint32_t )1)
{
uint64_t t16 = ws_w[i - (uint32_t )16];
uint64_t t15 = ws_w[i - (uint32_t )15];
uint64_t t7 = ws_w[i - (uint32_t )7];
uint64_t t2 = ws_w[i - (uint32_t )2];
ws_w[i] =
((t2 >> (uint32_t )19 | t2 << (uint32_t )64 - (uint32_t )19)
^ (t2 >> (uint32_t )61 | t2 << (uint32_t )64 - (uint32_t )61) ^ t2 >> (uint32_t )6)
+
t7
+
((t15 >> (uint32_t )1 | t15 << (uint32_t )64 - (uint32_t )1)
^ (t15 >> (uint32_t )8 | t15 << (uint32_t )64 - (uint32_t )8) ^ t15 >> (uint32_t )7)
+ t16;
}
uint64_t hash_0[8] = { 0 };
memcpy(hash_0, hash_w, (uint32_t )8 * sizeof hash_w[0]);
for (uint32_t i = (uint32_t )0; i < (uint32_t )80; i = i + (uint32_t )1)
{
uint64_t a = hash_0[0];
uint64_t b = hash_0[1];
uint64_t c = hash_0[2];
uint64_t d = hash_0[3];
uint64_t e = hash_0[4];
uint64_t f1 = hash_0[5];
uint64_t g = hash_0[6];
uint64_t h = hash_0[7];
uint64_t k_t = k_w[i];
uint64_t ws_t = ws_w[i];
uint64_t
t1 =
h
+
((e >> (uint32_t )14 | e << (uint32_t )64 - (uint32_t )14)
^
(e >> (uint32_t )18 | e << (uint32_t )64 - (uint32_t )18)
^ (e >> (uint32_t )41 | e << (uint32_t )64 - (uint32_t )41))
+ (e & f1 ^ ~e & g)
+ k_t
+ ws_t;
uint64_t
t2 =
((a >> (uint32_t )28 | a << (uint32_t )64 - (uint32_t )28)
^
(a >> (uint32_t )34 | a << (uint32_t )64 - (uint32_t )34)
^ (a >> (uint32_t )39 | a << (uint32_t )64 - (uint32_t )39))
+ (a & b ^ a & c ^ b & c);
uint64_t x1 = t1 + t2;
uint64_t x5 = d + t1;
uint64_t *p1 = hash_0;
uint64_t *p2 = hash_0 + (uint32_t )4;
p1[0] = x1;
p1[1] = a;
p1[2] = b;
p1[3] = c;
p2[0] = x5;
p2[1] = e;
p2[2] = f1;
p2[3] = g;
}
for (uint32_t i = (uint32_t )0; i < (uint32_t )8; i = i + (uint32_t )1)
{
uint64_t uu____871 = hash_w[i];
uint64_t uu____874 = hash_0[i];
uint64_t uu____870 = uu____871 + uu____874;
hash_w[i] = uu____870;
}
uint64_t c0 = counter_w[0];
uint64_t one1 = (uint64_t )(uint32_t )1;
counter_w[0] = c0 + one1;
}
static void Hacl_Hash_SHA2_512_update_multi(uint64_t *state, uint8_t *data, uint32_t n1)
{
for (uint32_t i = (uint32_t )0; i < n1; i = i + (uint32_t )1)
{
uint8_t *b = data + i * (uint32_t )128;
Hacl_Hash_SHA2_512_update(state, b);
}
}
static void Hacl_Hash_SHA2_512_update_last(uint64_t *state, uint8_t *data, uint64_t len)
{
uint8_t blocks[256] = { 0 };
uint32_t nb;
if (len < (uint64_t )112)
nb = (uint32_t )1;
else
nb = (uint32_t )2;
uint8_t *final_blocks;
if (len < (uint64_t )112)
final_blocks = blocks + (uint32_t )128;
else
final_blocks = blocks;
memcpy(final_blocks, data, (uint32_t )len * sizeof data[0]);
uint64_t n1 = state[168];
uint8_t *padding = final_blocks + (uint32_t )len;
FStar_UInt128_t
encodedlen =
FStar_UInt128_shift_left(FStar_UInt128_add(FStar_UInt128_mul_wide(n1,
(uint64_t )(uint32_t )128),
FStar_Int_Cast_Full_uint64_to_uint128(len)),
(uint32_t )3);
uint32_t
pad0len = ((uint32_t )256 - ((uint32_t )len + (uint32_t )16 + (uint32_t )1)) % (uint32_t )128;
uint8_t *buf1 = padding;
(void )(padding + (uint32_t )1);
uint8_t *buf2 = padding + (uint32_t )1 + pad0len;
buf1[0] = (uint8_t )0x80;
store128_be(buf2, encodedlen);
Hacl_Hash_SHA2_512_update_multi(state, final_blocks, nb);
}
static void Hacl_Hash_SHA2_512_finish(uint64_t *state, uint8_t *hash1)
{
uint64_t *hash_w = state + (uint32_t )160;
Hacl_Hash_Lib_LoadStore_uint64s_to_be_bytes(hash1, hash_w, (uint32_t )8);
}
static void Hacl_Hash_SHA2_512_hash(uint8_t *hash1, uint8_t *input, uint32_t len)
{
KRML_CHECK_SIZE((uint64_t )(uint32_t )0, (uint32_t )169);
uint64_t state[169];
for (uintmax_t _i = 0; _i < (uint32_t )169; ++_i)
state[_i] = (uint64_t )(uint32_t )0;
uint32_t n1 = len / (uint32_t )128;
uint32_t r = len % (uint32_t )128;
uint8_t *input_blocks = input;
uint8_t *input_last = input + n1 * (uint32_t )128;
Hacl_Hash_SHA2_512_init(state);
Hacl_Hash_SHA2_512_update_multi(state, input_blocks, n1);
Hacl_Hash_SHA2_512_update_last(state, input_last, (uint64_t )r);
Hacl_Hash_SHA2_512_finish(state, hash1);
}
uint32_t SHA2_512_size_word = (uint32_t )8;
uint32_t SHA2_512_size_hash_w = (uint32_t )8;
uint32_t SHA2_512_size_block_w = (uint32_t )16;
uint32_t SHA2_512_size_hash = (uint32_t )64;
uint32_t SHA2_512_size_block = (uint32_t )128;
uint32_t SHA2_512_size_k_w = (uint32_t )80;
uint32_t SHA2_512_size_ws_w = (uint32_t )80;
uint32_t SHA2_512_size_whash_w = (uint32_t )8;
uint32_t SHA2_512_size_count_w = (uint32_t )1;
uint32_t SHA2_512_size_len_8 = (uint32_t )16;
uint32_t SHA2_512_size_state = (uint32_t )169;
uint32_t SHA2_512_pos_k_w = (uint32_t )0;
uint32_t SHA2_512_pos_ws_w = (uint32_t )80;
uint32_t SHA2_512_pos_whash_w = (uint32_t )160;
uint32_t SHA2_512_pos_count_w = (uint32_t )168;
void SHA2_512_init(uint64_t *state)
{
Hacl_Hash_SHA2_512_init(state);
}
void SHA2_512_update(uint64_t *state, uint8_t *data)
{
Hacl_Hash_SHA2_512_update(state, data);
}
void SHA2_512_update_multi(uint64_t *state, uint8_t *data, uint32_t n1)
{
Hacl_Hash_SHA2_512_update_multi(state, data, n1);
}
void SHA2_512_update_last(uint64_t *state, uint8_t *data, uint64_t len)
{
Hacl_Hash_SHA2_512_update_last(state, data, len);
}
void SHA2_512_finish(uint64_t *state, uint8_t *hash1)
{
Hacl_Hash_SHA2_512_finish(state, hash1);
}
void SHA2_512_hash(uint8_t *hash1, uint8_t *input, uint32_t len)
{
Hacl_Hash_SHA2_512_hash(hash1, input, len);
}
sw/airborne/modules/datalink/hacl-c/SHA2_512.h
+107
View File
@@ -0,0 +1,107 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __SHA2_512_H
#define __SHA2_512_H
#include "testlib.h"
typedef uint8_t Hacl_Hash_Lib_Create_uint8_t;
typedef uint32_t Hacl_Hash_Lib_Create_uint32_t;
typedef uint64_t Hacl_Hash_Lib_Create_uint64_t;
typedef uint8_t Hacl_Hash_Lib_Create_uint8_ht;
typedef uint32_t Hacl_Hash_Lib_Create_uint32_ht;
typedef uint64_t Hacl_Hash_Lib_Create_uint64_ht;
typedef uint8_t *Hacl_Hash_Lib_Create_uint8_p;
typedef uint32_t *Hacl_Hash_Lib_Create_uint32_p;
typedef uint64_t *Hacl_Hash_Lib_Create_uint64_p;
typedef uint8_t *Hacl_Hash_Lib_LoadStore_uint8_p;
typedef uint8_t Hacl_Hash_SHA2_512_uint8_t;
typedef uint32_t Hacl_Hash_SHA2_512_uint32_t;
typedef uint64_t Hacl_Hash_SHA2_512_uint64_t;
typedef uint8_t Hacl_Hash_SHA2_512_uint8_ht;
typedef uint32_t Hacl_Hash_SHA2_512_uint32_ht;
typedef uint64_t Hacl_Hash_SHA2_512_uint64_ht;
typedef FStar_UInt128_t Hacl_Hash_SHA2_512_uint128_ht;
typedef uint64_t *Hacl_Hash_SHA2_512_uint64_p;
typedef uint8_t *Hacl_Hash_SHA2_512_uint8_p;
typedef uint8_t SHA2_512_uint8_t;
typedef uint32_t SHA2_512_uint32_t;
typedef uint64_t SHA2_512_uint64_t;
typedef uint8_t SHA2_512_uint8_ht;
typedef uint32_t SHA2_512_uint32_ht;
typedef uint64_t SHA2_512_uint64_ht;
typedef FStar_UInt128_t SHA2_512_uint128_ht;
typedef uint64_t *SHA2_512_uint64_p;
typedef uint8_t *SHA2_512_uint8_p;
extern uint32_t SHA2_512_size_word;
extern uint32_t SHA2_512_size_hash_w;
extern uint32_t SHA2_512_size_block_w;
extern uint32_t SHA2_512_size_hash;
extern uint32_t SHA2_512_size_block;
extern uint32_t SHA2_512_size_k_w;
extern uint32_t SHA2_512_size_ws_w;
extern uint32_t SHA2_512_size_whash_w;
extern uint32_t SHA2_512_size_count_w;
extern uint32_t SHA2_512_size_len_8;
extern uint32_t SHA2_512_size_state;
extern uint32_t SHA2_512_pos_k_w;
extern uint32_t SHA2_512_pos_ws_w;
extern uint32_t SHA2_512_pos_whash_w;
extern uint32_t SHA2_512_pos_count_w;
void SHA2_512_init(uint64_t *state);
void SHA2_512_update(uint64_t *state, uint8_t *data);
void SHA2_512_update_multi(uint64_t *state, uint8_t *data, uint32_t n1);
void SHA2_512_update_last(uint64_t *state, uint8_t *data, uint64_t len);
void SHA2_512_finish(uint64_t *state, uint8_t *hash1);
void SHA2_512_hash(uint8_t *hash1, uint8_t *input, uint32_t len);
#endif
sw/airborne/modules/datalink/hacl-c/Salsa20.c
+369
View File
@@ -0,0 +1,369 @@
#include "Salsa20.h"
static void
Hacl_Lib_Create_make_h32_4(uint32_t *b, uint32_t s0, uint32_t s1, uint32_t s2, uint32_t s3)
{
b[0] = s0;
b[1] = s1;
b[2] = s2;
b[3] = s3;
}
static void
Hacl_Lib_Create_make_h32_8(
uint32_t *b,
uint32_t s0,
uint32_t s1,
uint32_t s2,
uint32_t s3,
uint32_t s4,
uint32_t s5,
uint32_t s6,
uint32_t s7
)
{
Hacl_Lib_Create_make_h32_4(b, s0, s1, s2, s3);
Hacl_Lib_Create_make_h32_4(b + (uint32_t )4, s4, s5, s6, s7);
}
static void
Hacl_Lib_Create_make_h32_16(
uint32_t *b,
uint32_t s0,
uint32_t s1,
uint32_t s2,
uint32_t s3,
uint32_t s4,
uint32_t s5,
uint32_t s6,
uint32_t s7,
uint32_t s8,
uint32_t s9,
uint32_t s10,
uint32_t s11,
uint32_t s12,
uint32_t s13,
uint32_t s14,
uint32_t s15
)
{
Hacl_Lib_Create_make_h32_8(b, s0, s1, s2, s3, s4, s5, s6, s7);
Hacl_Lib_Create_make_h32_8(b + (uint32_t )8, s8, s9, s10, s11, s12, s13, s14, s15);
}
static void
Hacl_Lib_LoadStore32_uint32s_from_le_bytes(uint32_t *output, uint8_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t *x0 = input + (uint32_t )4 * i;
uint32_t inputi = load32_le(x0);
output[i] = inputi;
}
}
static void
Hacl_Lib_LoadStore32_uint32s_to_le_bytes(uint8_t *output, uint32_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint32_t hd1 = input[i];
uint8_t *x0 = output + (uint32_t )4 * i;
store32_le(x0, hd1);
}
}
inline static void Hacl_Impl_Salsa20_setup(uint32_t *st, uint8_t *k, uint8_t *n1, uint64_t c)
{
uint32_t tmp[10] = { 0 };
uint32_t *k_ = tmp;
uint32_t *n_ = tmp + (uint32_t )8;
Hacl_Lib_LoadStore32_uint32s_from_le_bytes(k_, k, (uint32_t )8);
Hacl_Lib_LoadStore32_uint32s_from_le_bytes(n_, n1, (uint32_t )2);
uint32_t c0 = (uint32_t )c;
uint32_t c1 = (uint32_t )(c >> (uint32_t )32);
uint32_t k0 = k_[0];
uint32_t k1 = k_[1];
uint32_t k2 = k_[2];
uint32_t k3 = k_[3];
uint32_t k4 = k_[4];
uint32_t k5 = k_[5];
uint32_t k6 = k_[6];
uint32_t k7 = k_[7];
uint32_t n0 = n_[0];
uint32_t n11 = n_[1];
Hacl_Lib_Create_make_h32_16(st,
(uint32_t )0x61707865,
k0,
k1,
k2,
k3,
(uint32_t )0x3320646e,
n0,
n11,
c0,
c1,
(uint32_t )0x79622d32,
k4,
k5,
k6,
k7,
(uint32_t )0x6b206574);
}
inline static void
Hacl_Impl_Salsa20_line(uint32_t *st, uint32_t a, uint32_t b, uint32_t d, uint32_t s)
{
uint32_t sa = st[a];
uint32_t sb = st[b];
uint32_t sd = st[d];
uint32_t sbd = sb + sd;
uint32_t sbds = sbd << s | sbd >> (uint32_t )32 - s;
st[a] = sa ^ sbds;
}
inline static void
Hacl_Impl_Salsa20_quarter_round(uint32_t *st, uint32_t a, uint32_t b, uint32_t c, uint32_t d)
{
Hacl_Impl_Salsa20_line(st, b, a, d, (uint32_t )7);
Hacl_Impl_Salsa20_line(st, c, b, a, (uint32_t )9);
Hacl_Impl_Salsa20_line(st, d, c, b, (uint32_t )13);
Hacl_Impl_Salsa20_line(st, a, d, c, (uint32_t )18);
}
inline static void Hacl_Impl_Salsa20_double_round(uint32_t *st)
{
Hacl_Impl_Salsa20_quarter_round(st, (uint32_t )0, (uint32_t )4, (uint32_t )8, (uint32_t )12);
Hacl_Impl_Salsa20_quarter_round(st, (uint32_t )5, (uint32_t )9, (uint32_t )13, (uint32_t )1);
Hacl_Impl_Salsa20_quarter_round(st, (uint32_t )10, (uint32_t )14, (uint32_t )2, (uint32_t )6);
Hacl_Impl_Salsa20_quarter_round(st, (uint32_t )15, (uint32_t )3, (uint32_t )7, (uint32_t )11);
Hacl_Impl_Salsa20_quarter_round(st, (uint32_t )0, (uint32_t )1, (uint32_t )2, (uint32_t )3);
Hacl_Impl_Salsa20_quarter_round(st, (uint32_t )5, (uint32_t )6, (uint32_t )7, (uint32_t )4);
Hacl_Impl_Salsa20_quarter_round(st, (uint32_t )10, (uint32_t )11, (uint32_t )8, (uint32_t )9);
Hacl_Impl_Salsa20_quarter_round(st,
(uint32_t )15,
(uint32_t )12,
(uint32_t )13,
(uint32_t )14);
}
inline static void Hacl_Impl_Salsa20_rounds(uint32_t *st)
{
for (uint32_t i = (uint32_t )0; i < (uint32_t )10; i = i + (uint32_t )1)
Hacl_Impl_Salsa20_double_round(st);
}
inline static void Hacl_Impl_Salsa20_sum_states(uint32_t *st, uint32_t *st_)
{
for (uint32_t i = (uint32_t )0; i < (uint32_t )16; i = i + (uint32_t )1)
{
uint32_t uu____871 = st[i];
uint32_t uu____874 = st_[i];
uint32_t uu____870 = uu____871 + uu____874;
st[i] = uu____870;
}
}
inline static void Hacl_Impl_Salsa20_copy_state(uint32_t *st, uint32_t *st_)
{
memcpy(st, st_, (uint32_t )16 * sizeof st_[0]);
}
inline static void Hacl_Impl_Salsa20_salsa20_core(uint32_t *k, uint32_t *st, uint64_t ctr)
{
uint32_t c0 = (uint32_t )ctr;
uint32_t c1 = (uint32_t )(ctr >> (uint32_t )32);
st[8] = c0;
st[9] = c1;
Hacl_Impl_Salsa20_copy_state(k, st);
Hacl_Impl_Salsa20_rounds(k);
Hacl_Impl_Salsa20_sum_states(k, st);
}
inline static void
Hacl_Impl_Salsa20_salsa20_block(uint8_t *stream_block, uint32_t *st, uint64_t ctr)
{
uint32_t st_[16] = { 0 };
Hacl_Impl_Salsa20_salsa20_core(st_, st, ctr);
Hacl_Lib_LoadStore32_uint32s_to_le_bytes(stream_block, st_, (uint32_t )16);
}
inline static void Hacl_Impl_Salsa20_init(uint32_t *st, uint8_t *k, uint8_t *n1)
{
Hacl_Impl_Salsa20_setup(st, k, n1, (uint64_t )0);
}
static void
Hacl_Impl_Salsa20_update_last(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint32_t *st,
uint64_t ctr
)
{
uint8_t block[64] = { 0 };
Hacl_Impl_Salsa20_salsa20_block(block, st, ctr);
uint8_t *mask = block;
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t uu____602 = plain[i];
uint8_t uu____605 = mask[i];
uint8_t uu____601 = uu____602 ^ uu____605;
output[i] = uu____601;
}
}
static void
Hacl_Impl_Salsa20_update(uint8_t *output, uint8_t *plain, uint32_t *st, uint64_t ctr)
{
uint32_t b[48] = { 0 };
uint32_t *k = b;
uint32_t *ib = b + (uint32_t )16;
uint32_t *ob = b + (uint32_t )32;
Hacl_Impl_Salsa20_salsa20_core(k, st, ctr);
Hacl_Lib_LoadStore32_uint32s_from_le_bytes(ib, plain, (uint32_t )16);
for (uint32_t i = (uint32_t )0; i < (uint32_t )16; i = i + (uint32_t )1)
{
uint32_t uu____602 = ib[i];
uint32_t uu____605 = k[i];
uint32_t uu____601 = uu____602 ^ uu____605;
ob[i] = uu____601;
}
Hacl_Lib_LoadStore32_uint32s_to_le_bytes(output, ob, (uint32_t )16);
}
static void
Hacl_Impl_Salsa20_salsa20_counter_mode_blocks(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint32_t *st,
uint64_t ctr
)
{
for (uint32_t i = (uint32_t )0; i < len; i = i + (uint32_t )1)
{
uint8_t *b = plain + (uint32_t )64 * i;
uint8_t *o = output + (uint32_t )64 * i;
Hacl_Impl_Salsa20_update(o, b, st, ctr + (uint64_t )i);
}
}
static void
Hacl_Impl_Salsa20_salsa20_counter_mode(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint32_t *st,
uint64_t ctr
)
{
uint32_t blocks_len = len >> (uint32_t )6;
uint32_t part_len = len & (uint32_t )0x3f;
uint8_t *output_ = output;
uint8_t *plain_ = plain;
uint8_t *output__ = output + (uint32_t )64 * blocks_len;
uint8_t *plain__ = plain + (uint32_t )64 * blocks_len;
Hacl_Impl_Salsa20_salsa20_counter_mode_blocks(output_, plain_, blocks_len, st, ctr);
if (part_len > (uint32_t )0)
Hacl_Impl_Salsa20_update_last(output__, plain__, part_len, st, ctr + (uint64_t )blocks_len);
}
static void
Hacl_Impl_Salsa20_salsa20(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint8_t *k,
uint8_t *n1,
uint64_t ctr
)
{
uint32_t buf[16] = { 0 };
uint32_t *st = buf;
Hacl_Impl_Salsa20_init(st, k, n1);
Hacl_Impl_Salsa20_salsa20_counter_mode(output, plain, len, st, ctr);
}
inline static void Hacl_Impl_HSalsa20_setup(uint32_t *st, uint8_t *k, uint8_t *n1)
{
uint32_t tmp[12] = { 0 };
uint32_t *k_ = tmp;
uint32_t *n_ = tmp + (uint32_t )8;
Hacl_Lib_LoadStore32_uint32s_from_le_bytes(k_, k, (uint32_t )8);
Hacl_Lib_LoadStore32_uint32s_from_le_bytes(n_, n1, (uint32_t )4);
uint32_t k0 = k_[0];
uint32_t k1 = k_[1];
uint32_t k2 = k_[2];
uint32_t k3 = k_[3];
uint32_t k4 = k_[4];
uint32_t k5 = k_[5];
uint32_t k6 = k_[6];
uint32_t k7 = k_[7];
uint32_t n0 = n_[0];
uint32_t n11 = n_[1];
uint32_t n2 = n_[2];
uint32_t n3 = n_[3];
Hacl_Lib_Create_make_h32_16(st,
(uint32_t )0x61707865,
k0,
k1,
k2,
k3,
(uint32_t )0x3320646e,
n0,
n11,
n2,
n3,
(uint32_t )0x79622d32,
k4,
k5,
k6,
k7,
(uint32_t )0x6b206574);
}
static void
Hacl_Impl_HSalsa20_crypto_core_hsalsa20(uint8_t *output, uint8_t *nonce, uint8_t *key)
{
uint32_t tmp[24] = { 0 };
uint32_t *st = tmp;
uint32_t *hs = tmp + (uint32_t )16;
Hacl_Impl_HSalsa20_setup(st, key, nonce);
Hacl_Impl_Salsa20_rounds(st);
uint32_t hs0 = st[0];
uint32_t hs1 = st[5];
uint32_t hs2 = st[10];
uint32_t hs3 = st[15];
uint32_t hs4 = st[6];
uint32_t hs5 = st[7];
uint32_t hs6 = st[8];
uint32_t hs7 = st[9];
Hacl_Lib_Create_make_h32_8(hs, hs0, hs1, hs2, hs3, hs4, hs5, hs6, hs7);
Hacl_Lib_LoadStore32_uint32s_to_le_bytes(output, hs, (uint32_t )8);
}
void *Salsa20_op_String_Access(FStar_Monotonic_HyperStack_mem h, uint8_t *b)
{
return (void *)(uint8_t )0;
}
void
Salsa20_salsa20(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint8_t *k,
uint8_t *n1,
uint64_t ctr
)
{
Hacl_Impl_Salsa20_salsa20(output, plain, len, k, n1, ctr);
}
void Salsa20_hsalsa20(uint8_t *output, uint8_t *key, uint8_t *nonce)
{
Hacl_Impl_HSalsa20_crypto_core_hsalsa20(output, nonce, key);
}
sw/airborne/modules/datalink/hacl-c/Salsa20.h
+64
View File
@@ -0,0 +1,64 @@
/* This file was auto-generated by KreMLin! */
#include "kremlib.h"
#ifndef __Salsa20_H
#define __Salsa20_H
#include "testlib.h"
typedef uint32_t Hacl_Impl_Xor_Lemmas_u32;
typedef uint8_t Hacl_Impl_Xor_Lemmas_u8;
typedef uint32_t Hacl_Lib_Create_h32;
typedef uint8_t *Hacl_Lib_LoadStore32_uint8_p;
typedef uint32_t Hacl_Impl_Salsa20_u32;
typedef uint32_t Hacl_Impl_Salsa20_h32;
typedef uint8_t *Hacl_Impl_Salsa20_uint8_p;
typedef uint32_t *Hacl_Impl_Salsa20_state;
typedef uint32_t Hacl_Impl_Salsa20_idx;
typedef struct
{
void *k;
void *n;
}
Hacl_Impl_Salsa20_log_t_;
typedef void *Hacl_Impl_Salsa20_log_t;
typedef uint32_t Hacl_Impl_HSalsa20_h32;
typedef uint32_t Hacl_Impl_HSalsa20_u32;
typedef uint8_t *Hacl_Impl_HSalsa20_uint8_p;
typedef uint32_t *Hacl_Impl_HSalsa20_state;
typedef uint8_t *Salsa20_uint8_p;
typedef uint32_t Salsa20_uint32_t;
void *Salsa20_op_String_Access(FStar_Monotonic_HyperStack_mem h, uint8_t *b);
typedef uint32_t *Salsa20_state;
void
Salsa20_salsa20(
uint8_t *output,
uint8_t *plain,
uint32_t len,
uint8_t *k,
uint8_t *n1,
uint64_t ctr
);
void Salsa20_hsalsa20(uint8_t *output, uint8_t *key, uint8_t *nonce);
#endif
sw/airborne/modules/datalink/hacl-c/gcc_compat.h
+18
View File
@@ -0,0 +1,18 @@
#ifndef __GCC_COMPAT_H
#define __GCC_COMPAT_H
#ifndef _MSC_VER
// Use the gcc predefined macros if on a platform/architectures that set them. Otherwise define them to be empty.
#ifndef __cdecl
#define __cdecl
#endif
#ifndef __stdcall
#define __stdcall
#endif
#ifndef __fastcall
#define __fastcall
#endif
#endif
#endif // __GCC_COMPAT_H
sw/airborne/modules/datalink/hacl-c/kremlib.c
+52
View File
@@ -0,0 +1,52 @@
#include "kremlib.h"
#include <stdlib.h>
#ifdef KREMLIB_EMBEDDED_TARGET /* bare-metal targets */
int exit_success = 0;
int exit_failure = 1;
void print_string(const char *s __attribute__((unused))) {}
void print_bytes(uint8_t *b, uint32_t len __attribute__((unused))) {}
#else /* any other platform */
int exit_success = EXIT_SUCCESS;
int exit_failure = EXIT_FAILURE;
void print_string(const char *s) {
printf("%s", s);
}
void print_bytes(uint8_t *b, uint32_t len) {
for (uint32_t i = 0; i < len; i++){
printf("%02x", b[i]);
}
printf("\n");
}
#endif
void FStar_Buffer_recall(void *x) {}
bool Prims_op_GreaterThanOrEqual(Prims_int x, Prims_int y) { KRML_EXIT; }
bool Prims_op_LessThanOrEqual(Prims_int x, Prims_int y) { KRML_EXIT; }
bool Prims_op_GreaterThan(Prims_int x, Prims_int y) { KRML_EXIT; }
bool Prims_op_LessThan(Prims_int x, Prims_int y) { KRML_EXIT; }
Prims_int Prims_pow2(Prims_int x) { KRML_EXIT; }
Prims_int Prims_op_Multiply(Prims_int x, Prims_int y) { KRML_EXIT; }
Prims_int Prims_op_Addition(Prims_int x, Prims_int y) { KRML_EXIT; }
Prims_int Prims_op_Subtraction(Prims_int x, Prims_int y) { KRML_EXIT; }
Prims_int Prims_op_Division(Prims_int x, Prims_int y) { KRML_EXIT; }
Prims_int Prims_op_Modulus(Prims_int x, Prims_int y) { KRML_EXIT; }
void *Prims_magic(void *_) { KRML_EXIT; }
void *Prims_admit(void *_) { KRML_EXIT; }
void *Prims____Cons___tl(void *_) { KRML_EXIT; }
bool FStar_HyperStack_is_eternal_color(Prims_int x0) { KRML_EXIT; }
FStar_Seq_Base_seq FStar_Seq_Base_append(FStar_Seq_Base_seq x, FStar_Seq_Base_seq y) { KRML_EXIT; }
FStar_Seq_Base_seq FStar_Seq_Base_slice(FStar_Seq_Base_seq x, FStar_Seq_Base_seq y, Prims_nat z) {
KRML_EXIT;
}
Prims_int FStar_UInt32_v(uint32_t x) { return (void *)0; }
FStar_UInt32_t FStar_UInt32_uint_to_t(Prims_nat x) { KRML_EXIT; }
sw/airborne/modules/datalink/hacl-c/kremlib.h
+578
View File
File diff suppressed because it is too large Load Diff
sw/airborne/modules/datalink/hacl-c/testlib.c
+59
View File
@@ -0,0 +1,59 @@
#include "testlib.h"
void TestLib_compare_and_print(const char *txt, uint8_t *reference,
uint8_t *output, int size) {
char *str = malloc(2 * size + 1);
char *str_ref = malloc(2 * size + 1);
for (int i = 0; i < size; ++i) {
sprintf(str + 2 * i, "%02x", output[i]);
sprintf(str_ref + 2 * i, "%02x", reference[i]);
}
str[2 * size] = '\0';
str_ref[2 * size] = '\0';
printf("[test] expected output %s is %s\n", txt, str_ref);
printf("[test] computed output %s is %s\n", txt, str);
for (int i = 0; i < size; ++i) {
if (output[i] != reference[i]) {
fprintf(stderr, "[test] reference %s and expected %s differ at byte %d\n",
txt, txt, i);
exit(EXIT_FAILURE);
}
}
printf("[test] %s is a success\n", txt);
free(str);
free(str_ref);
}
void TestLib_touch(int32_t x) {}
void TestLib_check(int32_t x, int32_t y) {
if (x != y) {
printf("Test check failure: %" PRId32 " != %" PRId32 "\n", x, y);
exit(253);
}
}
void *TestLib_unsafe_malloc(size_t size) {
void *memblob = malloc(size);
if (memblob == NULL) {
printf(" WARNING : malloc failed in tests !\n");
exit(EXIT_FAILURE);
}
return memblob;
}
void TestLib_print_clock_diff(clock_t t1, clock_t t2) {
printf("User time: %f\n", ((double)t2 - t1) / CLOCKS_PER_SEC);
}
void TestLib_perr(unsigned int err_code) {
printf("Got error code %u.\n", err_code);
}
void TestLib_print_cycles_per_round(TestLib_cycles c1, TestLib_cycles c2, uint32_t rounds) {
printf("[perf] cpu cycles per round (averaged over %d) is %f\n", rounds,
(float)(c2 - c1) / rounds);
}
sw/airborne/modules/datalink/hacl-c/testlib.h
+79
View File
@@ -0,0 +1,79 @@
#ifndef __TESTLIB_H
#define __TESTLIB_H
#include <inttypes.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <time.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <unistd.h>
#include <fcntl.h>
// This file has a hand-written .h file so that test files written in C (e.g.
// main-Poly1305.c) can use the functions from this file too (e.g.
// [compare_and_print]).
// Functions for F*-written tests, exposed via TestLib.fsti
void TestLib_touch(int32_t);
void TestLib_check(int32_t, int32_t);
// These functions are also called by HACL
void TestLib_compare_and_print(const char *txt, uint8_t *reference,
uint8_t *output, int size);
void *TestLib_unsafe_malloc(size_t size);
void TestLib_print_clock_diff(clock_t t1, clock_t t2);
void TestLib_perr(unsigned int err_code);
#define TestLib_uint8_p_null NULL
#define TestLib_uint32_p_null NULL
#define TestLib_uint64_p_null NULL
typedef unsigned long long TestLib_cycles, cycles;
#if defined(__COMPCERT__)
static __inline__ TestLib_cycles TestLib_cpucycles(void) {
return 0;
}
static __inline__ TestLib_cycles TestLib_cpucycles_begin(void)
{
return 0;
}
static __inline__ TestLib_cycles TestLib_cpucycles_end(void)
{
return 0;
}
#else
#ifndef _MSC_VER
static __inline__ TestLib_cycles TestLib_cpucycles(void) {
unsigned hi, lo;
__asm__ __volatile__("rdtsc" : "=a"(lo), "=d"(hi));
return ((unsigned long long)lo) | (((unsigned long long)hi) << 32);
}
static __inline__ TestLib_cycles TestLib_cpucycles_begin(void)
{
unsigned hi, lo;
__asm__ __volatile__ ("CPUID\n\t" "RDTSC\n\t" "mov %%edx, %0\n\t" "mov %%eax, %1\n\t": "=r" (hi), "=r" (lo):: "%rax", "%rbx", "%rcx", "%rdx");
return ( (uint64_t)lo)|( ((uint64_t)hi)<<32 );
}
static __inline__ TestLib_cycles TestLib_cpucycles_end(void)
{
unsigned hi, lo;
__asm__ __volatile__ ("RDTSCP\n\t" "mov %%edx, %0\n\t" "mov %%eax, %1\n\t" "CPUID\n\t": "=r" (hi), "=r" (lo):: "%rax", "%rbx", "%rcx", "%rdx");
return ( (uint64_t)lo)|( ((uint64_t)hi)<<32 );
}
#endif
#endif
void TestLib_print_cycles_per_round(TestLib_cycles c1, TestLib_cycles c2, uint32_t rounds);
#endif
sw/airborne/modules/datalink/spprz_dl.c
+40
View File
@@ -0,0 +1,40 @@
/*
* Copyright (C) 2017 Michal Podhradsky <michal.podhradsky@aggiemail.usu.edu>
*
* This file is part of paparazzi.
*
* paparazzi is free software; you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation; either version 2, or (at your option)
* any later version.
*
* paparazzi is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with paparazzi; see the file COPYING. If not, see
* <http://www.gnu.org/licenses/>.
*
*/
/** \file modules/datalink/spprz_dl.c
* \brief Datalink using secure PPRZ protocol
*/
#include "modules/datalink/spprz_dl.h"
#include "subsystems/datalink/datalink.h"
struct spprz_transport spprz_tp;
void spprz_dl_init(void)
{
spprz_transport_init(&spprz_tp);
}
void spprz_dl_event(void)
{
spprz_check_and_parse(&DOWNLINK_DEVICE.device, &spprz_tp, dl_buffer, &dl_msg_available);
DlCheckAndParse(&DOWNLINK_DEVICE.device, &spprz_tp.trans_tx, dl_buffer, &dl_msg_available);
}
sw/airborne/modules/datalink/spprz_dl.h
+49
View File
@@ -0,0 +1,49 @@
/*
* Copyright (C) 2017 Michal Podhradsky <michal.podhradsky@aggiemail.usu.edu>
*
* This file is part of paparazzi.
*
* paparazzi is free software; you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation; either version 2, or (at your option)
* any later version.
*
* paparazzi is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with paparazzi; see the file COPYING. If not, see
* <http://www.gnu.org/licenses/>.
*
*/
/** \file modules/datalink/spprz_dl.h
* \brief Datalink using secure PPRZ protocol
*/
#ifndef SPPRZ_DL_H
#define SPPRZ_DL_H
#include "pprzlink/secure_pprz_transport.h"
#include "mcu_periph/uart.h"
#if USE_USB_SERIAL
#include "mcu_periph/usb_serial.h"
#endif
#if USE_UDP
#include "mcu_periph/udp.h"
#endif
/** PPRZ transport structure */
extern struct spprz_transport spprz_tp;
/** Init function */
extern void spprz_dl_init(void);
/** Datalink Event */
extern void spprz_dl_event(void);
#endif /* SPPRZ_DL_H */