Update s2n-bignum subtree #1865
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
s2n-bignum original commit: awslabs/s2n-bignum@36a214d
Add NEON versions of functions for RSA 2048 and 4096 s2n-bignum original commit: awslabs/s2n-bignum@ec076f9
s2n-bignum original commit: awslabs/s2n-bignum@04f64a0
s2n-bignum original commit: awslabs/s2n-bignum@047e403
Adding support for SHA256 and SHA512 intrinsics s2n-bignum original commit: awslabs/s2n-bignum@e6024ae
s2n-bignum original commit: awslabs/s2n-bignum@c7dbd1f
s2n-bignum original commit: awslabs/s2n-bignum@367283c
s2n-bignum original commit: awslabs/s2n-bignum@b2bf71c
This patch adds constant-time table-lookup functions (`bignum_copy_row_from_table*`) and their proofs. This patch only contains its AArch64 version, and the x86 version will follow later. The failure of proving its x86 version seems to be related to handling negative offsets, and (if this is right) this can be avoided by simply proving positive offsets. I will record this as a Github issue with a promise that the x86 scalar version will be provided after the RSA related things are finished. This patch contains four table-lookup functions: 1. `bignum_copy_row_from_table`: a lookup for a generic table size 2. `bignum_copy_row_from_table_8n_neon`: a Neon version for a table whose width is a multiple of 8 3. `bignum_copy_row_from_table_16_neon`: Neon implementation of a table whose width is 16*64=1024 bits 4. `bignum_copy_row_from_table_32_neon`: Neon implementation of a table whose width is 32*64=2048 bits The last two versions are initially written by Hanno Becker. To successfully compile and run `test` and `benchmark` in x86, the scalar `bignum_copy_row_from_table` function is processed as a way similar to Neon functions. s2n-bignum original commit: awslabs/s2n-bignum@f1ad23c
Add bignum_copy_row_from_table and its Neon-variants for AArch64 s2n-bignum original commit: awslabs/s2n-bignum@50aa85b
s2n-bignum original commit: awslabs/s2n-bignum@74d34c3
This implements the point compression encoding to a byte array from https://datatracker.ietf.org/doc/html/rfc8032#section-5.1.2 as function "edwards25519_encode". It assumes the input is a point (x,y) on the edwards25519 curve, with coordinates reduced mod p_25519 = 2^255 - 19, and does not check any of that. s2n-bignum original commit: awslabs/s2n-bignum@67430be
s2n-bignum original commit: awslabs/s2n-bignum@b49b4f9
This implements point decoding from a 256-bit little-endian byte sequence to a point (x,y) on the edwards25519 curve as specified in https://datatracker.ietf.org/doc/html/rfc8032#section-5.1.3 The function returns 0 for success and 1 for failure, the latter meaning that the input is not the encoding of any edwards25519 point. s2n-bignum original commit: awslabs/s2n-bignum@97f7493
The function bignum_mod_n25519 performs reduction of an input of any size (k digits) modulo the order of the curve25519/edwards25519 basepoint, n_25519 = 2^252 + 27742317777372353535851937790883648493. It generalizes bignum_mod_n25519_4, which is the special case of 4-digit (256-bit) inputs. s2n-bignum original commit: awslabs/s2n-bignum@e23fd30
The functions bignum_madd_n25519 and bignum_madd_n25519_alt perform multiply-add modulo the order of the curve25519/edwards25519 basepoint, n_25519 = 2^252 + 27742317777372353535851937790883648493, i.e. z := (x * y + c) mod n_25519 where all variables are 256 bits. s2n-bignum original commit: awslabs/s2n-bignum@7fc5883
s2n-bignum original commit: awslabs/s2n-bignum@2c8e273
This replaces the inlined variant of "bignum_modinv" with code from "bignum_inv_p25519" in all "curve25519_" functions returning an affine point and hence using modular inverse. There are also a few consequential changes related to the slightly different amount of temporary storage needed by this function. s2n-bignum original commit: awslabs/s2n-bignum@777d574
…ck_no Document that x25519 function does not implement zero-check s2n-bignum original commit: awslabs/s2n-bignum@5c4b15a
s2n-bignum original commit: awslabs/s2n-bignum@73ec55a
This replaces the inlined variant of "bignum_modinv" with code from "bignum_inv_p25519" in all "edwards25519_scalarmul*" functions. Again, there are consequential changes related to the slightly different amount of temporary storage needed by bignum_inv_p25519. s2n-bignum original commit: awslabs/s2n-bignum@7e7b18e
Ed25519 support and related updates s2n-bignum original commit: awslabs/s2n-bignum@db8409d
s2n-bignum original commit: awslabs/s2n-bignum@58a6bdf
Add BFM, BIC, FCSEL, INS, SUB, TRN1, TRN2, USHR, ZIP2 to ARM model s2n-bignum original commit: awslabs/s2n-bignum@f1caaf1
In general, BOUNDER_RULE now directly handles operations over Z and N, assuming an outer real_of_int / real_of_num cast into R (this is also automated in the tactic form BOUNDER_TAC). In particular, this change can greatly improve bounds for terms involving integer or natural number division and remainder (DIV, div, MOD and rem) as well as cutoff subtraction over N. There is also now support for conditionals, though the condition is not used as extra context, simply being the basis for a case split. This update rolls in various trivial typographic fixes in comments. s2n-bignum original commit: awslabs/s2n-bignum@ccefa2a
s2n-bignum original commit: awslabs/s2n-bignum@e6ef86f
…5519 Avoid duplicate labels in ed25519 x86 implementation s2n-bignum original commit: awslabs/s2n-bignum@f629458
s2n-bignum original commit: awslabs/s2n-bignum@c1fbdb5
64-bit SIMD regs in ARM model, better BOUNDER_RULE, slow-ARM field optimizations s2n-bignum original commit: awslabs/s2n-bignum@06781d2
s2n-bignum original commit: awslabs/s2n-bignum@286d596
s2n-bignum original commit: awslabs/s2n-bignum@96086bb
P-256 scalar multiplication and related tweaks s2n-bignum original commit: awslabs/s2n-bignum@2237fe8
P-256 precomputed point scalar multiplication s2n-bignum original commit: awslabs/s2n-bignum@37c69f1
The new function bignum_montinv_p256 is a "Montgomery domain" variant
of the existing modular inverse function bignum_inv_p256, which seems
often to be better suited to the generally Montgomery-centric field
operations supplied by s2n-bignum for P-256. Given an input x it
returns a z such that x * z == 2^512 (mod p_256), or zero in cases
when x is in {0,p_256}. This does indeed correspond to inversion in
the Montgomery domain because if x == 2^256 * X and z == 2^256 * Z
(both mod p_256) then the congruence x * z == 2^512 (mod p_256) means
that X * Z == 1 (mod p_256). The code is in fact almost identical to
bignum_inv_p256, changing only the starting value for the iterations,
and the proof is very similar.
s2n-bignum original commit: awslabs/s2n-bignum@c07aee5
The new function p256_montjscalarmul[_alt] is analogous to the existing p256_scalarmul[_alt], doing scalar multiplication n * P for a point P on the NIST P-256 curve and a scalar n. This variant, however, uses the Jacobian representation for both input and output points, with the coordinates in Montgomery form. As such, it is approximately the same as the "middle" of p256_scalarmul, excluding the mappings from and back to affine form; it may make a more convenient building-block for other operations. s2n-bignum original commit: awslabs/s2n-bignum@0a8a754
Add global assumptions paragraph s2n-bignum original commit: awslabs/s2n-bignum@d61796f
Update Arm cosimulator to check that opcodes appear, add x86_att test to CI s2n-bignum original commit: awslabs/s2n-bignum@3eb104f
s2n-bignum original commit: awslabs/s2n-bignum@c6da080
Add hybrid `p256_montjadd` and `p256_montjdouble` for Arm, slow multipliers s2n-bignum original commit: awslabs/s2n-bignum@7ff619c
s2n-bignum original commit: awslabs/s2n-bignum@9824dd0
This inherits the performance improvements to p256_montjadd and p256_montjdouble by analogy with the updates to p256_scalarmul. The arm/Makefile is also tweaked to attempt to reflect more accurately the dependencies of individual ".correct" files. s2n-bignum original commit: awslabs/s2n-bignum@4451534
The new function p384_montjscalarmul[_alt] is the NIST P-384 analog of the corresponding P-256 function. It does scalar multiplication of a point on the P-384 curve, where both input and output points are in the Jacobian representation with coordinates in Montgomery form. s2n-bignum original commit: awslabs/s2n-bignum@2bbaf04
As pointed out by June Lee in the code review, the various forms of the new function p384_montjscalarmul[_alt] all had the same typo in the comment banner of the code, where the Jacobian points were shown as size 12 instead of 3*6 = 18. The actual C header files in include/s2n-bignum*.h were already correct. s2n-bignum original commit: awslabs/s2n-bignum@eacef33
Extra P-256 functions for AWS-LC integration, popcount, basic P-384 scalar mul s2n-bignum original commit: awslabs/s2n-bignum@08bf556
The new function bignum_inv_p384 is similar to the existing function bignum_inv_p256, with intermediate results longer (6-7 words in place of 4-5) and different Montgomery reduction, this time to work for the NIST P-384 prime p_384 = 2^384 - 2^128 - 2^96 + 2^32 - 1. s2n-bignum original commit: awslabs/s2n-bignum@c97c521
The new function bignum_montinv_p384 is a "Montgomery domain" variant
of the existing modular inverse function bignum_inv_p384, which seems
often to be better suited to the generally Montgomery-centric field
operations supplied by s2n-bignum for P-384. Given an input x it
returns a z such that x * z == 2^768 (mod p_384), or zero in cases
when x is in {0,p_384}. This does indeed correspond to inversion in
the Montgomery domain because if x == 2^384 * X and z == 2^384 * Z
(both mod p_384) then the congruence x * z == 2^768 (mod p_384) means
that X * Z == 1 (mod p_384). The code is in fact almost identical to
bignum_inv_p384, changing only the starting value for the iterations,
and the proof is very similar.
s2n-bignum original commit: awslabs/s2n-bignum@95b4d64
For some new functions that we want to integrate into AWS-LC, this satisfies the BoringSSL / AWS-LC delocator by (1) making the labels unique and (2) avoiding .rep / .endr (the assembler repetition construct), which is replaced by C macro blocks. s2n-bignum original commit: awslabs/s2n-bignum@9aa8155
Changing #(I) to #(1*I) in the new macro blocks makes it happy, and is semantically trivial. s2n-bignum original commit: awslabs/s2n-bignum@4207da6
s2n-bignum original commit: awslabs/s2n-bignum@9019f26
P-384 field inverses and delocator-pacifying tweaks s2n-bignum original commit: awslabs/s2n-bignum@d85c6b5
This patch updates the p384 point operations to use the field operations optimized using NEON and the SLOTHY optimizer. The performance improvement is around 9%. ``` p384_montjdouble : 591.7 ns each (var 0.1%, corr -0.02) = 1690105 ops/sec p384_montjadd : 1143.6 ns each (var 0.1%, corr 0.04) = 874447 ops/sec p384_montjscalarmul : 329982.3 ns each (var 0.0%, corr 0.09) = 3030 ops/sec => p384_montjdouble : 543.2 ns each (var 0.1%, corr 0.02) = 1840798 ops/sec p384_montjadd : 1044.5 ns each (var 0.1%, corr -0.09) = 957396 ops/sec p384_montjscalarmul : 303017.8 ns each (var 0.0%, corr 0.04) = 3300 ops/sec ``` This patch also includes the following updates: - Add `arm/proofs/utils` and factor out the OCaml codes that are parameters to the equivalence checking tactics as files in the directory. - Update EQUIV_STEP_TAC to take additional arguments that describe dead value information of the registers in the programs. The information describes which registers contain dead values after each program location. EQUIV_STEP_TAC uses this information to clean assumptions that will not be used later during simulation. - A few tactics for equivalence checking to shorten repeatedly appearing proof patterns and a few updates in arm.ml for better error messages - Bug fixes in actions_merger.ml - Add a user-defined custom cache to ORTHOGONAL_COMPONENTS_CONV. This is useful for equiv checking because the memory invariants that appear in assumptions have a typical form (the byte64). - And many other improvements for speed s2n-bignum original commit: awslabs/s2n-bignum@0af76bc
Adopt the Arm SIMD-optimized p384 fields to point operations s2n-bignum original commit: awslabs/s2n-bignum@6248d16
Codecov ReportAll modified and coverable lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## main #1865 +/- ##
==========================================
- Coverage 78.46% 78.46% -0.01%
==========================================
Files 585 585
Lines 99457 99457
Branches 14236 14237 +1
==========================================
- Hits 78038 78034 -4
- Misses 20784 20787 +3
- Partials 635 636 +1 ☔ View full report in Codecov by Sentry. |
andrewhop
approved these changes
Sep 20, 2024
dkostic
approved these changes
Sep 20, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description of changes:
The list that tracks which files from s2n-bignum are used in AWS-LC was not complete. The list used for this PR:
I dunno why this pulls in +84 commits. But since it's only a license change, I'm going to simply squash when merging...
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license and the ISC license.