Merge branch 'main' into aes-ctr32

.github/workflows/dist.yml

@@ -32,17 +32,17 @@ jobs:
         if: matrix.os == 'macos-latest'
         run: |
           sudo rm -Rf /Library/Developer/CommandLineTools/SDKs/*
-          sudo xcode-select -s /Applications/Xcode_13.4.app
+          sudo xcode-select -s /Applications/Xcode_15.3.app
           CROSS_CI="aarch64-apple-darwin" .ci/script.sh
       - name: iOS aarch64
         if: matrix.os == 'macos-latest'
         run: |
           sudo rm -Rf /Library/Developer/CommandLineTools/SDKs/*
-          sudo xcode-select -s /Applications/Xcode_13.4.app
+          sudo xcode-select -s /Applications/Xcode_15.3.app
           CROSS_CI="aarch64-apple-ios" .ci/script.sh
       - name: iOS x64 simulator
         if: matrix.os == 'macos-latest'
         run: |
           sudo rm -Rf /Library/Developer/CommandLineTools/SDKs/*
-          sudo xcode-select -s /Applications/Xcode_13.4.app
+          sudo xcode-select -s /Applications/Xcode_15.3.app
           CROSS_CI="x86_64-apple-ios-simulator" .ci/script.sh

Makefile

@@ -701,7 +701,9 @@ INTRINSIC_FLAGS = \
   -add-include 'Hacl_MAC_Poly1305_Simd256:"libintvector.h"' \
   \
   -add-include 'Hacl_AES_128_CTR32_NI:"libintvector.h"' \
-  -add-include 'Hacl_AES_256_CTR32_NI:"libintvector.h"'
+  -add-include 'Hacl_AES_256_CTR32_NI:"libintvector.h"' \
+  \
+  -add-include 'Hacl_Hash_SHA3_Simd256:"libintvector.h"'
 
 # Disabled for distributions that don't include code based on intrinsics.
 INTRINSIC_INT_FLAGS = \
@@ -741,6 +743,7 @@ BUNDLE_FLAGS	=\
   $(BLAKE2_BUNDLE) \
   $(HMAC_BUNDLE) \
   $(SHA3_BUNDLE) \
+  $(SHA3_SIMD256_BUNDLE) \
   $(HASH_BUNDLE) \
   $(E_HASH_BUNDLE) \
   $(SHA2MB_BUNDLE) \
@@ -911,7 +914,7 @@ dist/test/c/%.c: $(ALL_KRML_FILES)
 	$(KRML) -silent \
 	  -tmpdir $(dir $@) -skip-compilation \
 	  -header $(HACL_HOME)/dist/LICENSE.txt \
-	  -no-prefix $(subst _,.,$*) \
+	  -no-prefix $(subst Hacl_Test_,Hacl.Test.,$*) \
           -library Hacl.P256,Hacl.K256.*,Hacl.Impl.*,EverCrypt.* \
 	  -add-include '"internal/Hacl_Hash_SHA2.h"' \
 	  -static-header Hacl.Impl.SHA2.Generic \

Makefile.common

@@ -160,8 +160,8 @@ CURVE_BUNDLE=-bundle Hacl.Curve25519_64=Hacl.Impl.Curve25519.Field64.Vale \
 # First, match the Blake2 stuff
 BLAKE2_BUNDLE_BASE= \
   -bundle Hacl.Impl.Blake2.Constants -static-header Hacl.Impl.Blake2.Constants \
-  -bundle 'Hacl.Streaming.Blake2b_32=Hacl.Blake2b_32,Hacl.Hash.Blake2b_32,Hacl.Impl.Blake2.\*,Hacl.Hash.Core.Blake2[rename=Hacl_Hash_Blake2b,rename-prefix]' \
-  -bundle 'Hacl.Streaming.Blake2s_32=Hacl.Blake2s_32,Hacl.Hash.Blake2s_32,Hacl.Impl.Blake2.\*,Hacl.Hash.Core.Blake2[rename=Hacl_Hash_Blake2s,rename-prefix]'
+  -bundle 'Hacl.Streaming.Blake2b_32=Hacl.Blake2b_32,Hacl.Hash.Blake2b_32,Hacl.Impl.Blake2.\*,Hacl.Hash.Core.Blake2,Hacl.Streaming.Blake2.Params,Hacl.Streaming.Blake2.Common[rename=Hacl_Hash_Blake2b,rename-prefix]' \
+  -bundle 'Hacl.Streaming.Blake2s_32=Hacl.Blake2s_32,Hacl.Hash.Blake2s_32[rename=Hacl_Hash_Blake2s,rename-prefix]'
 BLAKE2_BUNDLE= $(BLAKE2_BUNDLE_BASE) \
   -bundle Hacl.Streaming.Blake2b_256=Hacl.Blake2b_256,Hacl.Hash.Blake2b_256[rename=Hacl_Hash_Blake2b_Simd256,rename-prefix] \
   -bundle Hacl.Streaming.Blake2s_128=Hacl.Blake2s_128,Hacl.Hash.Blake2s_128[rename=Hacl_Hash_Blake2s_Simd128,rename-prefix]
@@ -190,7 +190,8 @@ HASH_BUNDLE= \
 # therefore Hacl.Impl.SHA3 cannot be put on the right-hand side of the bundle
 # (which would eliminate internal helpers not used otherwise, such as absorb or
 # squeeze)
-SHA3_BUNDLE=-bundle Hacl.Streaming.Keccak+Hacl.SHA3+Hacl.Impl.SHA3=Hacl.Hash.SHA3[rename=Hacl_Hash_SHA3,rename-prefix]
+SHA3_BUNDLE=-bundle Hacl.Streaming.Keccak+Hacl.Hash.SHA3.Scalar=Hacl.Hash.SHA3,Hacl.Impl.SHA3.Vec[rename=Hacl_Hash_SHA3,rename-prefix]
+SHA3_SIMD256_BUNDLE=-bundle Hacl.Hash.SHA3.Simd256=Hacl.Impl.SHA3.Vec
 CHACHA20_BUNDLE=-bundle Hacl.Chacha20=Hacl.Impl.Chacha20,Hacl.Impl.Chacha20.*
 SALSA20_BUNDLE=-bundle Hacl.Salsa20=Hacl.Impl.Salsa20,Hacl.Impl.Salsa20.*,Hacl.Impl.HSalsa20
 CHACHAPOLY_BUNDLE=-bundle Hacl.Impl.Chacha20Poly1305 \

README.md

@@ -9,12 +9,20 @@ The code for all of these algorithms is formally verified using the
 safety, functional correctness, and secret independence (resistance to
 some types of timing side-channels).
 
-**Documentation**: More detailed documentation on the library and our verification method
-can be found at [hacl-star.github.io](https://hacl-star.github.io).
+## Status
+
+*Warning*: This is the research home of HACL\*. If you are looking for
+documentation, releases, language bindings and code that can be satisfactorily
+integrated into a production project, please check out [HACL
+packages](https://github.com/cryspen/hacl-packages/).
 
 The code in this repository is divided into three closely-related sub-projects,
 all developed as part of [Project Everest](https://project-everest.github.io/).
 
+We are actively developing and integrating our code on the
+[main](https://github.com/project-everest/hacl-star/tree/main/)
+branch, which tracks F\*'s `master` branch.
+
 ## HACL\*
 
 [HACL\*](code/) is a formally verified library
@@ -47,18 +55,6 @@ depending on processor support and the target execution environment
 (*multiplexing*). Furthermore, EverCrypt offers an (*agile*) API that makes it
 simple to switch between algorithms (e.g., from SHA2 to SHA3).
 
-## Status
-
-*Warning*: This is a research project. Although some of our code is currently used in popular products like Mozilla Firefox and Wireguard,
-we highly recommend that users consult with the HACL\* maintainers before using this code in production systems.
-
-We are actively developing and integrating our code on the
-[master](https://github.com/project-everest/hacl-star/tree/master/)
-branch, which tracks F\*'s `master` branch. Ongoing developments on new
-cryptographic primitives happen in the [dev](https://github.com/project-everest/hacl-star/tree/dev/)
-branch, which runs a little ahead of master. You can find a current snapshot
-of our C and assembly code in the [dist](dist/) directory; stable releases of the full library
-can be found in the [releases](https://github.com/project-everest/hacl-star/releases) page.
 
 ## License
 
@@ -71,4 +67,3 @@ Contact the maintainers if you have other licensing requirements.
 This repository contains contributions from many students and researchers at INRIA, Microsoft Research, and Carnegie Mellon University,
 and it is under active development. The primary authors of each verified algorithm are noted in the corresponding AUTHORS.md file.
 For questions and comments, or if you want to contribute to the project, contact the current maintainers at [email protected].
-

code/blake2/Hacl.Blake2b_256.fst

@@ -13,6 +13,9 @@ let update_block : Impl.blake2_update_block_st Spec.Blake2B Core.M256 =
 let init : Impl.blake2_init_st Spec.Blake2B Core.M256 =
   Impl.blake2_init #Spec.Blake2B #Core.M256
 
+let init_with_params : Impl.blake2_init_with_params_st Spec.Blake2B Core.M256 =
+  Impl.blake2_init_with_params #Spec.Blake2B #Core.M256
+
 let update_key : Impl.blake2_update_key_st Spec.Blake2B Core.M256 =
   Impl.blake2_update_key #Spec.Blake2B #Core.M256 update_block
 

code/blake2/Hacl.Blake2b_32.fst

@@ -12,6 +12,9 @@ let update_block : Impl.blake2_update_block_st Spec.Blake2B Core.M32 =
 let init : Impl.blake2_init_st Spec.Blake2B Core.M32 =
   Impl.blake2_init #Spec.Blake2B #Core.M32
 
+let init_with_params : Impl.blake2_init_with_params_st Spec.Blake2B Core.M32 =
+  Impl.blake2_init_with_params #Spec.Blake2B #Core.M32
+
 let update_key : Impl.blake2_update_key_st Spec.Blake2B Core.M32 =
   Impl.blake2_update_key #Spec.Blake2B #Core.M32 update_block
 

code/blake2/Hacl.Blake2s_128.fst

@@ -13,6 +13,9 @@ let update_block : Impl.blake2_update_block_st Spec.Blake2S Core.M128 =
 let init : Impl.blake2_init_st Spec.Blake2S Core.M128 =
   Impl.blake2_init #Spec.Blake2S #Core.M128
 
+let init_with_params : Impl.blake2_init_with_params_st Spec.Blake2S Core.M128 =
+  Impl.blake2_init_with_params #Spec.Blake2S #Core.M128
+
 let update_key : Impl.blake2_update_key_st Spec.Blake2S Core.M128 =
   Impl.blake2_update_key #Spec.Blake2S #Core.M128 update_block
 

code/blake2/Hacl.Blake2s_32.fst

@@ -13,6 +13,9 @@ let update_block : Impl.blake2_update_block_st Spec.Blake2S Core.M32 =
 let init : Impl.blake2_init_st Spec.Blake2S Core.M32 =
   Impl.blake2_init #Spec.Blake2S #Core.M32
 
+let init_with_params : Impl.blake2_init_with_params_st Spec.Blake2S Core.M32 =
+  Impl.blake2_init_with_params #Spec.Blake2S #Core.M32
+
 let update_key : Impl.blake2_update_key_st Spec.Blake2S Core.M32 =
   Impl.blake2_update_key #Spec.Blake2S #Core.M32 update_block
 

code/blake2/Hacl.Impl.Blake2.Core.fst

@@ -31,27 +31,16 @@ let row_v #a #m h r =
 
 let row_v_lemma #a #m h0 h1 r1 r2 = ()
 
-let create_default_params a salt personal =
-  match a with
-  | Spec.Blake2S -> {
-      digest_length = u8 32;
-      key_length = u8 0;
+let alloca_default_params a =
+  let salt = create (salt_len a) (u8 0) in
+  let personal = create (personal_len a) (u8 0) in
+  {
+      digest_length = (match a with Spec.Blake2B -> 64uy | Spec.Blake2S -> 32uy);
+      key_length = 0uy;
       fanout = u8 1;
       depth = u8 1;
       leaf_length = u32 0;
-      node_offset = u32 0;
-      xof_length = u16 0;
-      node_depth = u8 0;
-      inner_length = u8 0;
-      salt; personal } <: blake2s_params
-  | Spec.Blake2B -> {
-      digest_length = u8 64;
-      key_length = u8 0;
-      fanout = u8 1;
-      depth = u8 1;
-      leaf_length = u32 0;
-      node_offset = u32 0;
-      xof_length = u32 0;
+      node_offset = u64 0;
       node_depth = u8 0;
       inner_length = u8 0;
       salt; personal }

code/blake2/Hacl.Impl.Blake2.Core.fsti

@@ -66,165 +66,49 @@ let personal_len (a:Spec.alg) : size_t =
   | Spec.Blake2B -> 16ul
 
 noeq
-type blake2s_params = {
-  digest_length: uint8;
-  key_length: uint8;
+inline_for_extraction // projectors
+type blake2_params (a:Spec.alg) = {
+  digest_length: digest_length: UInt8.t { 1 <= UInt8.v digest_length /\ UInt8.v digest_length <= Spec.max_output a };
+  key_length: key_length: UInt8.t { UInt8.v key_length <= Spec.max_key a };
   fanout: uint8;
   depth: uint8;
   leaf_length: uint32;
-  node_offset: uint32;
-  xof_length: uint16;
+  node_offset: Spec.node_offset_t a;
   node_depth: uint8;
   inner_length: uint8;
-  salt: lbuffer uint8 8ul;
-  personal: lbuffer uint8 8ul;
+  salt: lbuffer uint8 (salt_len a);
+  personal: lbuffer uint8 (personal_len a);
 }
 
-inline_for_extraction noextract
-let get_blake2s_salt (p: blake2s_params) = p.salt
-
-inline_for_extraction noextract
-let get_blake2s_personal (p: blake2s_params) = p.personal
-
-inline_for_extraction noextract
-let set_blake2s_digest_length
-  (p: blake2s_params)
-  (nn: size_t{1 <= v nn /\ v nn <= Spec.max_output Spec.Blake2S})
-  : blake2s_params =
-  {p with digest_length = to_u8 nn}
-
-inline_for_extraction noextract
-let set_blake2s_key_length
-  (p: blake2s_params)
-  (kk: size_t{v kk <= Spec.max_key Spec.Blake2S})
-  : blake2s_params =
-  {p with key_length = to_u8 kk}
-
-let blake2s_params_inv (h: mem) (p: blake2s_params): GTot prop =
-  live h p.salt /\ live h p.personal
-
-let blake2s_params_loc (p: blake2s_params) =
-  loc p.salt `union` loc p.personal
-
-let blake2s_params_v (h: mem) (p: blake2s_params): GTot Spec.blake2s_params =
-  Spec.Mkblake2s_params
-    p.digest_length
-    p.key_length
-    p.fanout
-    p.depth
-    p.leaf_length
-    p.node_offset
-    p.xof_length
-    p.node_depth
-    p.inner_length
-    (as_seq h p.salt)
-    (as_seq h p.personal)
-
-noeq
-type blake2b_params = {
-  digest_length: uint8;
-  key_length: uint8;
-  fanout: uint8;
-  depth: uint8;
-  leaf_length: uint32;
-  node_offset: uint32;
-  xof_length: uint32;
-  node_depth: uint8;
-  inner_length: uint8;
-  // Blake2b also contains 14 reserved bytes here, but they seem
-  // unused and to only contain zeros, hence we do not expose them
-  salt: lbuffer uint8 16ul;
-  personal: lbuffer uint8 16ul;
-}
-
-let blake2b_params_inv (h: mem) (p: blake2b_params): GTot prop =
-  live h p.salt /\ live h p.personal
+let blake2_params_inv (#a: Spec.alg) (h: mem) (p: blake2_params a): GTot prop =
+  live h p.salt /\ live h p.personal /\ LowStar.Buffer.loc_disjoint (loc_addr_of_buffer p.salt) (loc_addr_of_buffer p.personal)
 
-let blake2b_params_loc (p: blake2b_params) =
-  loc p.salt `union` loc p.personal
+let blake2_params_loc (#a: Spec.alg) (p: blake2_params a) =
+  loc_addr_of_buffer p.salt `union` loc_addr_of_buffer p.personal
 
-let blake2b_params_v (h: mem) (p: blake2b_params): GTot Spec.blake2b_params =
-  Spec.Mkblake2b_params
+let blake2_params_v (#a: Spec.alg) (h: mem) (p: blake2_params a): GTot (Spec.blake2_params a) =
+  Spec.Mkblake2_params
     p.digest_length
     p.key_length
     p.fanout
     p.depth
     p.leaf_length
     p.node_offset
-    p.xof_length
     p.node_depth
     p.inner_length
     (as_seq h p.salt)
     (as_seq h p.personal)
 
-noextract inline_for_extraction
-let blake2_params (a:Spec.alg) =
-  match a with
-  | Spec.Blake2S -> blake2s_params
-  | Spec.Blake2B -> blake2b_params
-
-inline_for_extraction noextract
-let set_digest_length (#a: Spec.alg)
-  (p: blake2_params a)
-  (nn: size_t{1 <= v nn /\ v nn <= Spec.max_output a})
-  : blake2_params a =
-  match a with
-  | Spec.Blake2S -> set_blake2s_digest_length p nn
-  | Spec.Blake2B -> {p with digest_length = to_u8 nn}
-
 inline_for_extraction noextract
-let set_key_length (#a: Spec.alg)
-  (p: blake2_params a)
-  (kk: size_t{v kk <= Spec.max_key a})
-  : blake2_params a =
-  match a with
-  | Spec.Blake2S -> set_blake2s_key_length p kk
-  | Spec.Blake2B -> {p with key_length = to_u8 kk}
-
-inline_for_extraction noextract
-let get_salt (#a: Spec.alg) (p: blake2_params a) : lbuffer uint8 (salt_len a) =
-  match a with
-  | Spec.Blake2S -> get_blake2s_salt p
-  | Spec.Blake2B -> p.salt
-
-inline_for_extraction noextract
-let get_personal (#a: Spec.alg) (p: blake2_params a) : lbuffer uint8 (personal_len a) =
-  match a with
-  | Spec.Blake2S -> get_blake2s_personal p
-  | Spec.Blake2B -> p.personal
-
-noextract inline_for_extraction
-let blake2_params_inv (#a:Spec.alg) (h: mem) (p: blake2_params a) =
-  match a with
-  | Spec.Blake2S -> blake2s_params_inv h p
-  | Spec.Blake2B -> blake2b_params_inv h p
-
-noextract inline_for_extraction
-let blake2_params_loc (#a:Spec.alg) (p: blake2_params a) =
-  match a with
-  | Spec.Blake2S -> blake2s_params_loc p
-  | Spec.Blake2B -> blake2b_params_loc p
-
-noextract inline_for_extraction
-let blake2_params_v (#a:Spec.alg) (h: mem) (p: blake2_params a) : GTot (Spec.blake2_params a) =
-  match a with
-  | Spec.Blake2S -> blake2s_params_v h p
-  | Spec.Blake2B -> blake2b_params_v h p
-
-noextract inline_for_extraction
-val create_default_params: a:Spec.alg ->
-  salt: lbuffer uint8 (salt_len a) ->
-  personal: lbuffer uint8 (personal_len a) ->
-  Stack (blake2_params a)
-    (requires fun h -> live h salt /\ live h personal /\
-      as_seq h salt == Seq.create (Spec.salt_length a) (u8 0) /\
-      as_seq h personal == Seq.create (Spec.personal_length a) (u8 0)
-    )
-    (ensures (fun h0 p h1 ->
-      h0 == h1 /\
-      blake2_params_loc p == loc salt `union` loc personal /\
-      blake2_params_inv h1 p /\
-      blake2_params_v h1 p == Spec.blake2_default_params a))
+val alloca_default_params: a: Spec.alg -> StackInline (blake2_params a)
+  (requires (fun _ -> True))
+  (ensures (fun h0 s h1 ->
+    blake2_params_inv h1 s /\
+    blake2_params_v h1 s == Spec.blake2_default_params a /\
+    LowStar.Buffer.(modifies loc_none h0 h1) /\
+    LowStar.Buffer.fresh_loc (blake2_params_loc s) h0 h1 /\
+    LowStar.Buffer.(loc_includes (loc_region_only true (FStar.HyperStack.get_tip h1))
+        (blake2_params_loc s))))
 
 noextract inline_for_extraction
 unfold let state_p (a:Spec.alg) (m:m_spec) =
@@ -395,7 +279,6 @@ val alloc_state: a:Spec.alg -> m:m_spec ->
 				live h1 r))
 
 
-
 noextract inline_for_extraction
 val copy_state: #a:Spec.alg -> #m:m_spec -> st2:state_p a m -> st1:state_p a m ->
 	  Stack unit