Import AES-CTR32 modules from pnmadelaine_aes branch and add NI proofs #919

mamonet · 2024-03-09T17:23:11Z

This PR imports AES-CTR32 modules from pnmadelaine_aes branch and adds proofs for NI functions.

…ctions

github-actions · 2024-03-09T17:23:36Z

[CI] Important!
The code in dist/gcc-compatible, dist/msvc-compatible, and dist/wasm
is tested on cryspen/hacl-packages.
dist is not automatically re-generated, be sure to do it manually.
(A fresh snapshot can also be downloaded from CI by going to the "artifacts" section of your run.)
Then check the following tests before merging this PR.
Always check the latest run, it corresponds to the most recent version of this branch.
All jobs are expected to be successful.
In some cases manual intervention is needed. Please ping the hacl-packages maintainers.

Build, Test, Benchmark: Build on Linux (x86, x64), Windows (x86, x64), MacOS (x64, arm64), s390x, Android (arm64) and test on Linux (x86, x64), Windows (x86, x64), MacOS (x64).
Performance Regression Tests: Navigate to the terminal output in “Run benchmarks”. The comparison with the main branch will be at the bottom. The run fails if the performance regresses too much.
OCaml bindings: Build & Tests
JS bindings: Build & Tests
Rust bindings: Build & Tests

msprotz

Can you show us the C code, too?

This is only when the CPU has NI support, correct?

Makefile.common

dist/Makefile.tmpl

msprotz

Various tidbits to be fixed. I would really like some thorough testing to make sure this is producing the correct results, with a variety of test cases, on arm and x64. The fact that the arguments to the (unverified) macro glue were in the wrong order makes me... slightly nervous

I would also like to see the incremental API being tested out in the C file.

msprotz · 2024-04-16T16:50:18Z

code/aes/Hacl.AES_128.CTR32.NI.fst

+let skey = skey Spec.AES128
+
+[@ CInline ]
+val create_ctx: unit ->


if this is stackinline, it needs to be marked inline_for_extraction noextract

and as a corollary, it can only be used by verified clients; you might want to consider adding a malloc function to allocate a context on the heap

Right, I replaced create_ctx with functions that allocate and free buffer on the heap.

you'll still need the variant that allocates on the stack when you write aes-gcm and want to allocate aes state on the caller's stack

Restored and marked as inline_for_extraction noextract.

great, FYI, we've been calling the functions alloca in other modules, so please use that name for consistency

(when it allocates state on the stack)

code/aes/Hacl.AES_128.CTR32.NI.fst

code/aes/Hacl.Impl.AES.Core.fst

msprotz · 2024-04-16T17:01:09Z

code/aes/Hacl.Impl.AES.Generic.fst

+    nonce_to_bytes m n == state.block /\
+    keyx_to_bytes m a kex == state.key_ex)))
+
+let aes_init #m #a ctx key nonce =


I take it that a toolchain supports either building both variants, or none at all?

code/aes/Makefile

dist/configure

msprotz · 2024-04-16T17:04:41Z

specs/Spec.AES.fst

+    st0.block ctr0 msg
+
+let aes_ctr32_decrypt_bytes_LE v key nonce ctr0 msg =
+  aes_ctr32_encrypt_bytes_LE v key nonce ctr0 msg


where is the proof that encrypt (decrypt x) == x?

that proof should be applied for aes_ctr32_decrypt_bytes_LE function?

yes -- it should be pretty trivial in this case but it's a good "sanity check" to make sure you can prove that?

Vale has no such lemma, in fact Vale doesn't have decryption function for AES/GCTR spec. See https://github.com/hacl-star/hacl-star/blob/main/vale/specs/crypto/Vale.AES.AES_s.fst
https://github.com/hacl-star/hacl-star/blob/main/vale/specs/crypto/Vale.AES.GCTR_s.fst
GCM uses the forward version of AES cipher for encryption and decryption, so I think it's good to have aes_ctr32_decrypt unlike Vale but a lemma for encrypt (decrypt x) == x is to verify the spec itself and not the implementation.

tests/aes128-ctr32-ni-test.c

mamonet · 2024-04-17T16:11:28Z

The fact that the arguments to the (unverified) macro glue were in the wrong order makes me... slightly nervous

The order of arguments were flipped in the implementation side of F* code, but it doesn't meet the argument order in spec. To make the order consistent, I could either change the order for impl and spec or in libintvector.h I went for the later.

code/aes/.gitignore

code/aes/AUTHORS.md

msprotz

Overall this looks good, and I think we're nearly there!

My final requests before we merge this.

Please refresh the C code.
Please fix the naming convention -- @pnmadelaine spent a great deal of time making sure we have something consistent, so let's keep it neat and tidy.
Please write API documentation using CComment syntax (see the bignum files for an example of how to do that, and what would be considered a good style)
Please fix any merge conflicts with main so that we can merge this soon.

Congrats on another good PR and looking forward to merging soon.

msprotz · 2024-05-06T22:24:27Z

code/aes/Hacl.AES.CoreNI.Lemmas.fst

+    (BV.logxor_vec (to_vec128 (to_elem x)) (to_vec128 (to_elem y)))
+    (Seq.append (Seq.append (Seq.append (Seq.append (Seq.append
+      (Seq.append (Seq.append (Seq.append (Seq.append (Seq.append
+      (Seq.append (Seq.append (Seq.append (Seq.append (Seq.append


would any of these benefit from using FStar.BigOps for readability? this is quite extreme

msprotz · 2024-05-06T22:25:37Z

code/aes/Hacl.AES_128.CTR32.NI.fst

+
+
+[@ CInline ]
+val aes128_ctr_decrypt:


@pnmadelaine can you review this naming convention? I thought with your big PR, we were now trying to avoid redundant prefixes, such as aes128_ or state_

msprotz · 2024-05-06T22:27:37Z

dist/gcc-compatible/Hacl_AES_128_CTR32_NI.h

+
+#include "libintvector.h"
+
+typedef Lib_IntVector_Intrinsics_vec128 *Hacl_AES_128_CTR32_NI_aes_ctx;


I do not see state_malloc?

I updated C files in gcc-compatible/
I also renamed state_malloc/free to context_malloc/free

msprotz · 2024-05-06T22:28:15Z

dist/gcc-compatible/Hacl_AES_256_CTR32_NI.h

+
+typedef uint8_t *Hacl_AES_256_CTR32_NI_skey;
+
+void


same here, where is malloc/free?

Import AES-CTR32 modules from pnmadelaine_aes branch and prove NI fun…

1650f22

…ctions

This was referenced Mar 9, 2024

Verify AES Generic module cryspen/hacl-packages#450

Closed

Verify high-level AES-CTR32 functions for NI and BitSlice cryspen/hacl-packages#451

Closed

mamonet added 2 commits March 16, 2024 19:12

Remove AES BitSlice bits

c0e63f5

Remove AES BitSlice tests

4c93478

mamonet marked this pull request as ready for review March 16, 2024 17:21

mamonet requested a review from a team as a code owner March 16, 2024 17:21

Delete Lib.Sliceable and Lib.Transposition64x8 modules

e10b733

msprotz reviewed Mar 27, 2024

View reviewed changes

Makefile.common Show resolved Hide resolved

dist/Makefile.tmpl Outdated Show resolved Hide resolved

mamonet added 5 commits April 8, 2024 19:17

Upload extracted AES-CTR32 files

af3dd67

Support AES instructions in libintvector.h for ARM

6e2212f

Set proper flags for AES_NI support

883803b

Fix aes_enc and aes_enc_last

5e137a9

Propely build tests/aes128-ctr32-ni-test.c

980e840

msprotz reviewed Apr 16, 2024

View reviewed changes

mamonet added 4 commits April 16, 2024 19:07

Properly set AES_CTR32_BUNDLE

7b64da5

Use helper functions for AES nonce and keys

3d5fad3

Remove aes_key_block function

cd4a73b

Return result from main function in aes128-ctr32-ni-test.c

b73c86a

mamonet added 3 commits April 17, 2024 18:35

Restore create_ctx for AES-CTR32 modules

6755bbf

Rename AES create_ctx to state_alloca

f259fa2

Utilize functions from test_helpers.h in aes ni test

59558e4

msprotz reviewed Apr 18, 2024

View reviewed changes

code/aes/.gitignore Outdated Show resolved Hide resolved

msprotz reviewed Apr 18, 2024

View reviewed changes

code/aes/AUTHORS.md Outdated Show resolved Hide resolved

Remove code/aes/.gitignore

dcf15eb

franziskuskiefer mentioned this pull request Apr 29, 2024

Merge AES-CTR32 into HACL* cryspen/hacl-packages#455

Open

2 tasks

karthikbhargavan added 2 commits April 29, 2024 13:57

updated authors

60f4dee

Merge branch 'main' into aes-ctr32

2a3688e

franziskuskiefer linked an issue Apr 30, 2024 that may be closed by this pull request

Merge AES-CTR32 into HACL* cryspen/hacl-packages#455

Open

2 tasks

franziskuskiefer requested a review from msprotz May 6, 2024 07:52

msprotz reviewed May 6, 2024

View reviewed changes

mamonet and others added 5 commits May 29, 2024 19:18

Document AES-CTR32 library

1be011e

Move fmul_inner function to Hacl.AES.Round.Constant.fst

b6568ae

Fix AES_CTR32_BUNDLE and update C files in gcc-compatible/

f5a7543

Rename AES-CTR32 high-level functions

1c57c38

Merge branch 'main' into aes-ctr32

f129833

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Import AES-CTR32 modules from pnmadelaine_aes branch and add NI proofs #919

Import AES-CTR32 modules from pnmadelaine_aes branch and add NI proofs #919

mamonet commented Mar 9, 2024 •

edited

github-actions bot commented Mar 9, 2024 •

edited

msprotz left a comment

msprotz left a comment •

edited

msprotz Apr 16, 2024

msprotz Apr 16, 2024

mamonet Apr 17, 2024

msprotz Apr 17, 2024

mamonet Apr 17, 2024

msprotz Apr 17, 2024

msprotz Apr 17, 2024

msprotz Apr 16, 2024

msprotz Apr 16, 2024

mamonet Apr 17, 2024

msprotz Apr 18, 2024

mamonet Apr 19, 2024

mamonet commented Apr 17, 2024 •

edited

msprotz left a comment

msprotz May 6, 2024

msprotz May 6, 2024

msprotz May 6, 2024

mamonet May 29, 2024

msprotz May 6, 2024

mamonet May 29, 2024


		#include "libintvector.h"

		typedef Lib_IntVector_Intrinsics_vec128 *Hacl_AES_128_CTR32_NI_aes_ctx;

Import AES-CTR32 modules from pnmadelaine_aes branch and add NI proofs #919

Are you sure you want to change the base?

Import AES-CTR32 modules from pnmadelaine_aes branch and add NI proofs #919

Conversation

mamonet commented Mar 9, 2024 • edited

github-actions bot commented Mar 9, 2024 • edited

msprotz left a comment

Choose a reason for hiding this comment

msprotz left a comment • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mamonet commented Apr 17, 2024 • edited

msprotz left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mamonet commented Mar 9, 2024 •

edited

github-actions bot commented Mar 9, 2024 •

edited

msprotz left a comment •

edited

mamonet commented Apr 17, 2024 •

edited