s2n-bignum update 2024-12-05 #2037
Closed
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
Update sematests CI to run the ARM simulator
Also clean up and correct the pre-existing x86 IMUL formalization, removing historical relics and fixing the mixed-up length for single-operand IMUL with short operands.
This corrects the count masking for several 32-bit shift operations, none of them actually used in s2n-bignum but nevertheless accepted by the decoding setup. There are a few other tweaks as well that are not functionally necessary but make the simulation smoother. In particular BSWAP now just uses the standard HOL Light "word_bytereverse" operation instead of a local variant.
This patch updates the functions used by RSA signing to avoid using assembler macros because the `delocate` utility in BoringSSL cannot parse them. Also, the offsets in load/store instructions are simplified so that `delocate` can understand them as well. Also, the labels having overlapping names are renamed so that aws-lc can compile them without duplicate symbol found errors.
Avoid using assembler macros and rename labels in the functions for RSA
Add support for UZP2, XTN
The function bignum_inv_p25519 computes the modular inverse of its input modulo the specific modulus 2^255-19 (the characteristic of the underlying field for curve25519), for any 256-bit input coprime to that modulus, i.e. not divisible by it. It is generally somewhat faster than calling the generic function bignum_modinv (typically about a 1.5X performance ratio on x86), as well as involving less state setup.
Add NEON versions of functions for RSA 2048 and 4096
This patch adds a new build project to CI. This is supposed to run a random simulator for x86 that @jargh has implemented. I will make a follow-up PR that invokes it after this new CI is incorporated smoothly. At the moment, this build only runs an empty Makefile target `sematest`.
Add s2n-bignum-x86-sematests build project to CI
Adding SHA256 and SHA512 intrinsics Fixing accidental replacement of simulations function Commenting out SHA512 simulator instructions Fixing bitpatterns for SHA256SU1 and SHA256H
Adding support for SHA256 and SHA512 intrinsics
This patch makes bignum_emontredc_8n's proof equal to its neon version, by moving `8 divides val k` out from the postcondition. Also, some assembly' specs are updated to use `MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI`. And this patch includes these minor non-functional changes as well: - Multiplication functions' auxiliary lemma definitions are removed - A copyright text is added to `simulator.ml` and `bignum_mul_8_16_neon.S`.
Make bignum_emontredc_8n's spec equal to its neon version
This patch adds the x86 formal semantics simulator that is written by @jargh to the corresponding directory, and updates Makefile to run it. With this patch, the `s2n-bignum-x86-sematests` CI must run this script for 30 minutes.
Upload x86 simulator and link it to s2n-bignum-x86-sematests
The function bignum_mod_m25519_4 reduces a 4-digit (256-bit) number modulo the full group order (i.e. 8 * the standard basepoint order).
The function bignum_mod_n25519_4 reduces a 4-digit (256-bit) number modulo the standard basepoint order (1/8 of the overall group order).
Add two ARM instructions and add print_log flags
Additional ARM SIMD instructions used in ML-KEM code
The command line is fixed to have '-' as the final positional argument of `as` for Mac OS X (ARM). Another update is that it removes the object file used for checking x18 because otherwise it makes the next `make` commandline successfully proceed even if x18 check failed before.
This patch compiles proofs using native OCaml compiler, and updates `make proofs` to run the newly created `*.native` executable files. The new `tools/build-proof.sh` script builds a specific `.ml` proof file. It inlines all loads/needs in the `.ml` file using HOL Light's `inline_load.ml`. Then, it collects all specifications in the original `.ml` file using already existing `tools/collect-specs.sh`, and adds a print statement at the end of the file, to make its standard output pass the proof checker script. It also adds timer and prints the running time of the proof. Then it is compiled with `ocamlopt.byte`. Building all proofs can be done with `make build_proofs`. This uses a lot of memory, so compared to the previous version `-j` number given to `make` must be reduced. This also makes the prerequisite lists tidier using the '*.native' items. Each '.native' file is considered as depending on the '.o' file.
Check usage of the x18 register in Arm
This resolves failures that appear when cd may print something.
Use native OCaml compiler to build & run proofs
This patch prevents negative constant immediates in loads and stores like `ldp _, _, [_, -16]` from introducing a constant that is a result of underflow, e.g., `18446744073709551600`. Instead, `-16` is represented as `word_sub _ (word 16)`. In addition, this canonicalizes `word_sub (word_add baseptr ofs) ofs2)` to `word_add baseptr (word_sub ofs ofs2)` whenever possible because this makes symbolic analysis on memory instructions with negative constants easier because the base pointers appear clearly after this canonicalization.
Avoid underflow of negative constant immediates in load/stores
This patch updates `NONOVERLAPPING_TAC` to successfully deal with subtractions. An example that can be now resolved with it is as follows: ``` g `nonoverlapping (x:int64,k) (y:int64,k2) /\ 4 <= i /\ i < k ==> nonoverlapping (word_add x (word_sub (word i) (word 4)), 4) (y,k2)`;; e(REWRITE_TAC[NONOVERLAPPING_CLAUSES]);; e(STRIP_TAC);; e(NONOVERLAPPING_TAC);; ``` To achieve this, this patch (1) updates the normalizer to convert `word_sub (word x) (word y)` to `x - y` if `y <= x`, and (2) makes `cmp` eventually rely on `prove_le` rather than quickly raising a failure. Invoking `prove_le` can be quite expensive though; Therefore this patch also has an implication which is making `NONOVERLAPPING_TAC` a step toward being even more 'automatic' while being more expensive. Orthogonally, this patch updates the assembly simplifier tactic to recognize assumptions of the form `.. |- x = x` and filter them out because this can cause infinite loops in its following ASM_REWRITE tactics.
This reimplements the `PURE_DECODE_CONV` with the Compute module of HOL Light. To use the latest `*_COMPUTE_CONV` functions, this bumps the version of HOL Light to the latest one. :) The main part of this patch was prototyped by @monadius.
Use Compute to evaluate Arm's decode function
This patch enables cosimulation of SHA512 intrinsics.
…t.sh This also fixes the grep command of run-proof.sh . `grep -r` must take a directory name, but it was giving the output log file name. In the case of the proof CI, it is being double-checked by printing the list of proven specifications, so this missing check was somewhat benign.
Enable SHA512 intrinsics from Arm simulator
* Add instructions EOR3, RAX1, BCAX, and XAR * Enable simulation test for SHA3 instructions * Fixing syntax error * Add to operation clauses * Fixing a missing semicolon * More syntax fixing --------- Co-authored-by: Yan Peng <[email protected]>
Update NONOVERLAPPING_TAC to successfully process subtractions
This patch natively compiles simulators for speed and runs them. Resolves awslabs/s2n-bignum#161 .
Compile simulators for speed
This patch adds tutorial for Arm. The examples are copied from my repository (https://github.com/aqjune/hol-light-materials/). :)
Add tutorial for Arm
|
Closing, no idea why this pulls in bunch of files we haven't asked for. |
Codecov ReportAll modified and coverable lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## main #2037 +/- ##
==========================================
- Coverage 78.67% 78.66% -0.01%
==========================================
Files 598 598
Lines 103350 103350
Branches 14693 14692 -1
==========================================
- Hits 81308 81304 -4
- Misses 21389 21395 +6
+ Partials 653 651 -2 ☔ View full report in Codecov by Sentry. |
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:
Pull in the latest s2n-bignum changes as of 2024-12-05.
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.