aws · manastasova · Mar 24, 2026
@@ -1,5 +1,5 @@
 name: s2n-bignum-imported
 source: awslabs/s2n-bignum.git
-commit: 2b5350cf955a32d2f7aced172f7bd28dd85a8587
+commit: 3bfe68deb9fbdaf23be0a927c362a87a799adc28
 target: main
-imported-at: 2025-09-05T04:04:05+0000
+imported-at: 2026-03-24T00:00:39+0000
@@ -54,18 +54,138 @@ GITHUB_COMMIT=$(cd ${TMP} >/dev/null; git rev-parse HEAD)
 echo "Cloned s2n-bignum folder"
 ls -la ${TMP}
 
-echo "Remove source code from s2n-bignum that is not needed..."
-code_not_needed=("benchmarks" "codebuild" "common" "tests" "tools" "x86" "arm/proofs")
-for code in "${code_not_needed[@]}"; do
-  rm -rf ${TMP}/${code}
-done
-
-echo "Cloned s2n-bignum folder after removing unneeded source code..."
-ls -la ${TMP}
+# ---------------------------------------------------------------------------
+# Allowlist of files to import.
+#
+# Only files actually compiled by aws-lc (referenced in
+# crypto/fipsmodule/CMakeLists.txt) plus headers and legal files are imported.
+# ---------------------------------------------------------------------------
+
+# Assembly files compiled on both x86_64 (x86_att/) and aarch64 (arm/).
+# Paths are relative to the architecture directory.
+COMMON_ASM_FILES=(
+  # p256
+  p256/p256_montjscalarmul.S
+  p256/p256_montjscalarmul_alt.S
+  p256/bignum_montinv_p256.S
+  # p384
+  p384/bignum_add_p384.S
+  p384/bignum_sub_p384.S
+  p384/bignum_neg_p384.S
+  p384/bignum_tomont_p384.S
+  p384/bignum_deamont_p384.S
+  p384/bignum_montmul_p384.S
+  p384/bignum_montmul_p384_alt.S
+  p384/bignum_montsqr_p384.S
+  p384/bignum_montsqr_p384_alt.S
+  p384/bignum_nonzero_6.S
+  p384/bignum_littleendian_6.S
+  p384/p384_montjdouble.S
+  p384/p384_montjdouble_alt.S
+  p384/p384_montjscalarmul.S
+  p384/p384_montjscalarmul_alt.S
+  p384/bignum_montinv_p384.S
+  # p521
+  p521/bignum_add_p521.S
+  p521/bignum_sub_p521.S
+  p521/bignum_neg_p521.S
+  p521/bignum_mul_p521.S
+  p521/bignum_mul_p521_alt.S
+  p521/bignum_sqr_p521.S
+  p521/bignum_sqr_p521_alt.S
+  p521/bignum_tolebytes_p521.S
+  p521/bignum_fromlebytes_p521.S
+  p521/p521_jdouble.S
+  p521/p521_jdouble_alt.S
+  p521/p521_jscalarmul.S
+  p521/p521_jscalarmul_alt.S
+  p521/bignum_inv_p521.S
+  # curve25519
+  curve25519/bignum_mod_n25519.S
+  curve25519/bignum_neg_p25519.S
+  curve25519/bignum_madd_n25519.S
+  curve25519/bignum_madd_n25519_alt.S
+  curve25519/edwards25519_decode.S
+  curve25519/edwards25519_decode_alt.S
+  curve25519/edwards25519_encode.S
+  curve25519/edwards25519_scalarmulbase.S
+  curve25519/edwards25519_scalarmulbase_alt.S
+  curve25519/edwards25519_scalarmuldouble.S
+  curve25519/edwards25519_scalarmuldouble_alt.S
+  # sha3
+  sha3/sha3_keccak_f1600.S
+)
+
+# Assembly files compiled only on x86_64.
+X86_ONLY_ASM_FILES=(
+  p384/bignum_tomont_p384_alt.S
+  p384/bignum_deamont_p384_alt.S
+  curve25519/curve25519_x25519.S
+  curve25519/curve25519_x25519_alt.S
+  curve25519/curve25519_x25519base.S
+  curve25519/curve25519_x25519base_alt.S
+)
+
+# Assembly files compiled only on aarch64.
+ARM_ONLY_ASM_FILES=(
+  curve25519/curve25519_x25519_byte.S
+  curve25519/curve25519_x25519_byte_alt.S
+  curve25519/curve25519_x25519base_byte.S
+  curve25519/curve25519_x25519base_byte_alt.S
+  fastmul/bignum_kmul_16_32.S
+  fastmul/bignum_kmul_32_64.S
+  fastmul/bignum_ksqr_16_32.S
+  fastmul/bignum_ksqr_32_64.S
+  fastmul/bignum_emontredc_8n.S
+  generic/bignum_ge.S
+  generic/bignum_mul.S
+  generic/bignum_optsub.S
+  generic/bignum_sqr.S
+  generic/bignum_copy_row_from_table.S
+  generic/bignum_copy_row_from_table_8n.S
+  generic/bignum_copy_row_from_table_16.S
+  generic/bignum_copy_row_from_table_32.S
+  sha3/sha3_keccak_f1600_alt.S
+  sha3/sha3_keccak2_f1600.S
+  sha3/sha3_keccak4_f1600_alt.S
+  sha3/sha3_keccak4_f1600_alt2.S
+)
 
 echo "Copy source code ..."
 mkdir ${SRC}
-cp -rH ${TMP}/* ${SRC}
+
+# Copy headers, legal files, and documentation
+mkdir -p ${SRC}/include
+cp -H ${TMP}/include/s2n-bignum.h ${TMP}/include/s2n-bignum-c89.h \
+     ${TMP}/include/_internal_s2n_bignum.h ${TMP}/include/_internal_s2n_bignum_arm.h \
+     ${TMP}/include/_internal_s2n_bignum_x86.h ${TMP}/include/_internal_s2n_bignum_x86_att.h \
+     ${SRC}/include/
+cp -H ${TMP}/LICENSE ${TMP}/NOTICE ${TMP}/README.md ${TMP}/SOUNDNESS.md ${TMP}/non_ct_functions.txt ${SRC}/
+mkdir -p ${SRC}/doc
+cp -H ${TMP}/doc/s2n_bignum_soundness.md ${TMP}/doc/s2n_bignum_soundness.svg ${SRC}/doc/
+mkdir -p ${SRC}/x86_att
+cp -H ${TMP}/x86_att/README.md ${SRC}/x86_att/README.md
+
+# Copy assembly files using the allowlists above.
+# Helper: copy a single .S file from TMP to SRC, creating parent dirs as needed.
+copy_asm() {
+  local relpath="$1"
+  mkdir -p "${SRC}/$(dirname "${relpath}")"
+  cp -H "${TMP}/${relpath}" "${SRC}/${relpath}"
+}
+
+for f in "${COMMON_ASM_FILES[@]}"; do
+  copy_asm "x86_att/${f}"
+  copy_asm "arm/${f}"
+done
+
+for f in "${X86_ONLY_ASM_FILES[@]}"; do
+  copy_asm "x86_att/${f}"
+done
+
+for f in "${ARM_ONLY_ASM_FILES[@]}"; do
+  copy_asm "arm/${f}"
+done
 
 echo "Copied s2n-bignum source code..."
 ls -la ${SRC}

@@ -11,9 +11,11 @@ tuned for highest performance both by hand and using automatic optimization
 techniques such as the [SLOTHY](https://github.com/slothy-optimizer/slothy)
 superoptimizer, and each function is accompanied by a machine-checked formal
 proof in [HOL-Light](https://hol-light.github.io/) that its mathematical
-result is correct, based on a formal model of the underlying machine. Each
-function is moreover written in a constant-time style to avoid timing
-side-channels.
+result is correct, based on a formal model of the underlying machine.
+Moreover, each function is written in a constant-time style to avoid timing
+side-channels. For a detailed analysis of the formal verification process, the
+assumptions made, and the correspondence of formal models with reality, please
+refer to the [s2n-bignum soundness review](SOUNDNESS.md).
 
 For the SHA-3 and ML-KEM code currently part of s2n-bignum, some of the
 comments in the main part of this README do not apply exactly. See the section