s2n-bignum update 2024-12-10 #2050
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
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
The new function p521_jscalarmul[_alt] is the NIST P-521 analog of the corresponding P-256 and P-384 functions: it does scalar multiplication of a point on the P-521 curve, where both input and output points are in Jacobian representation. But in contrast to the P-256 and P-284 functions, Montgomery form is *not* used. This update also fixes a few miscellaneous issues in tests and improves the specs of some other P-521 functions by fixing the nominal size parameter in "modular_decode". (It is actually not semantically relevant, being there to maintain the analog with "montgomery_decode".) s2n-bignum original commit: awslabs/s2n-bignum@c241557
s2n-bignum original commit: awslabs/s2n-bignum@f22ee62
The new function bignum_inv_p521 computes modular inverses modulo the NIST P-521 prime, the Mersenne prime 2^521 - 1. Its overall structure is similar to those of the existing bignum_inv_p256 and bignum_inv_p384 functions, just customized for a different, and longer, prime. s2n-bignum original commit: awslabs/s2n-bignum@11c5ef5
The previous versions used copies of the point operations that each inlined multiple copies of the field operations. This made the code size somewhat extravagant and the verification time long. The new versions use unified field multiplication and squaring, called everywhere as subroutines. s2n-bignum original commit: awslabs/s2n-bignum@54f11bf
Toplevel P-521 operations s2n-bignum original commit: awslabs/s2n-bignum@6122bb8
This patch updates the `p521_jadd`,`p521_jdouble` operations of Arm to use the NEON field operations. Performance improvement on GV2: - p521_jadd: 2095.9 ns -> 1793.8 (17%) - p521_jdouble: 1047.8 ns -> 857.2 (22%) Also, this fixes Makefile to correctly describe dependencies of p384_montjscalarmul. s2n-bignum original commit: awslabs/s2n-bignum@1f745d6
The speedup is around 20%. ``` p521_jscalarmul : 798224.6 ns each (var 0.0%, corr -0.07) = 1253 ops/sec -> p521_jscalarmul : 662859.9 ns each (var 0.0%, corr 0.05) = 1509 ops/sec ``` s2n-bignum original commit: awslabs/s2n-bignum@6a89082
s2n-bignum original commit: awslabs/s2n-bignum@f90f6d1
s2n-bignum original commit: awslabs/s2n-bignum@e205f0a
Update Arm `p521_jadd`/`jdouble` to use the neon field operations s2n-bignum original commit: awslabs/s2n-bignum@4bbd348
Minor typographical fixes s2n-bignum original commit: awslabs/s2n-bignum@b4eec0f
This is a patch that fixes p384_montjadd and p384_montjscalarmul (which has p384_montjadd inlined) to avoid memory access to stack pointer + negative offset in the middle of the function. This is because when a process is interrupted, in principle, context switching to a handler may overwrite data under the stack pointer: https://forum.osdev.org/viewtopic.php?t=21720 This also caused valgrind from AWS-LC side to fail. This is porting the patch of @dkostic: aws@65808f8 .. and also updates the proof according to it. Also, this adds valgrind to the test so that it can print such cases. s2n-bignum original commit: awslabs/s2n-bignum@99ff4f8
Avoid access to stack pointer + negative offset in p384_montjadd s2n-bignum original commit: awslabs/s2n-bignum@395365c
s2n-bignum original commit: awslabs/s2n-bignum@97cdfef
Rename equivalence tactics and introduce a few for convenience s2n-bignum original commit: awslabs/s2n-bignum@a866499
Codecov ReportAll modified and coverable lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## main #2050 +/- ##
=======================================
Coverage 78.76% 78.77%
=======================================
Files 598 598
Lines 103676 103676
Branches 14744 14744
=======================================
+ Hits 81665 81667 +2
Misses 21357 21357
+ Partials 654 652 -2 ☔ View full report in Codecov by Sentry. |
torben-hansen
approved these changes
Dec 10, 2024
samuel40791765
approved these changes
Dec 10, 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.
Issues:
N/A
Description of changes:
s2n-bignum update 2024-12-10
Call-outs:
Point out areas that need special attention or support during the review process. Discuss architecture or design changes.
Testing:
How is this change tested (unit tests, fuzz tests, etc.)? Are there any testing steps to be verified by the reviewer?
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.