Skip to content

Add signing hooks for observing signature attempts and implementing restartable signing#1237

Open
hanno-becker wants to merge 9 commits into
mainfrom
sign_hooks
Open

Add signing hooks for observing signature attempts and implementing restartable signing#1237
hanno-becker wants to merge 9 commits into
mainfrom
sign_hooks

Conversation

@hanno-becker

@hanno-becker hanno-becker commented Jun 28, 2026

Copy link
Copy Markdown
Contributor
sign: Add configurable signing hooks (resume/attempt/finish)

The runtime of ML-DSA signatures is theoretically unbounded. Even the
bound of max 814 signature attempts -- approved by NIST as lowering the
chance of signing failure below 2^{-256} -- leaves a performance
distribution whose peak percentiles can be unacceptable for constrained
systems with strict timing requirements.

The library already provides MLD_CONFIG_MAX_SIGNING_ATTEMPTS to cap the
number of signing attempts. However, FIPS 204 forbids lowering that bound
below 814, rendering the option non-compliant in constrained environments.

As a remedy, this commit introduces three optional 'signing hooks' around
the core rejection-sampling loop, keyed by the attempt counter (the loop
iteration; the spec counter is kappa = attempt*MLDSA_L):

- `attempt = sign_resume()`: Return the attempt to resume the operation
  from. `0` for an initial / non-restartable signing operation.
- `sign_attempt(attempt)`: Called before each attempt. Returns 0 to
  proceed, or non-zero to pause: signing then returns MLD_ERR_SIGNING_PAUSED
  with `attempt` as the resume point.
- `sign_finish(attempt)`: Called on success with the succeeding attempt.

Together, resume + attempt make signing _restartable_: a caller can pause
after a bounded number of attempts and later resume from the recorded
attempt, bounding per-call runtime while keeping a FIPS-compliant overall
bound and reproducing the same signature as an uninterrupted run.

This only works if the consumer drives the deterministic internal API: the
randomized API would choose a fresh seed on each (re-)start, so the resume
hook requires MLD_CONFIG_NO_RANDOMIZED_API and is incompatible with
MLD_CONFIG_KEYGEN_PCT (whose one-shot internal signature cannot be resumed).
The attempt and finish hooks also serve standalone uses with any API, e.g.
logging or benchmarking the per-signature attempt distribution.

Pausing is independent of MLD_CONFIG_MAX_SIGNING_ATTEMPTS, the upper bound on
the total number of attempts (>= 814 for FIPS 204 compliance) after which
signing gives up with the distinct error MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED; it
must not be lowered as a restart mechanism.

sign_{resume|attempt|finish} can be implemented on mutable globals or on a
context, so they are introduced under the existing MLD_CONFIG_CONTEXT_PARAMETER
wrapper, which lets functions be called with or without an
application-specific context pointer.

Concretely, this commit:

- Adds independent MLD_CONFIG_SIGN_HOOK_{RESUME,ATTEMPT,FINISH} options. When
  set, the integration provides, respectively:

  - `attempt = mld_sign_hook_resume([ctx])`: provide initial/resume attempt
  - `mld_sign_hook_attempt(attempt [, ctx])`: per-attempt hook; pause via
    non-zero return
  - `mld_sign_hook_finish(attempt [, ctx])`: note the succeeding attempt

  The unset dummies leave the default build (and its proofs) unchanged.

- Adds the MLD_ERR_SIGNING_PAUSED error code returned when the attempt hook
  pauses signing.

- Adds CBMC proofs for the three hooks and threads them through the existing
  signing proofs.

- Adds test/src/test_sign_hook.c (a new `sign_hook` test), which checks that
  restartable signing -- single-step and with random attempts-per-call --
  reproduces one-shot signing exactly, and gathers an attempts-per-signature
  distribution that it checks against the expected geometric mean per
  parameter set.


@hanno-becker hanno-becker changed the title Sign hooks Add signing hooks for observing signature attempts and implementing restartable signing Jun 28, 2026
@hanno-becker hanno-becker changed the title Add signing hooks for observing signature attempts and implementing restartable signing [WIP] Add signing hooks for observing signature attempts and implementing restartable signing Jun 28, 2026
@oqs-bot

oqs-bot commented Jun 28, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44, REDUCE-RAM)

Full Results (209 proofs)
Proof Status Current Previous Change
**TOTAL** 1400s 1364s +2.6%
polyvec_matrix_pointwise_montgomery_yvec 141s 149s -5%
poly_pointwise_montgomery_c 113s 112s +1%
mld_invntt_layer 98s 105s -7%
polyveck_chknorm 66s 67s -1%
sign_verify_internal 50s 49s +2%
mld_ntt_layer 41s 41s +0%
fqmul 40s 39s +3%
mld_ntt_butterfly_block 22s 23s -4%
keccakf1600x4_permute_native 20s 22s -9%
mld_attempt_signature_generation 20s 19s +5%
poly_ntt_c 18s 21s -14%
rej_uniform_c 17s 16s +6%
mld_check_pct 16s 15s +7%
polyeta_unpack 15s 14s +7%
poly_chknorm_c 14s 11s +27%
compute_pack_t0_t1 12s 12s +0%
poly_uniform_eta_4x 12s 12s +0%
polyt0_unpack 12s 12s +0%
polyveck_decompose 11s 7s +57%
polyvecl_chknorm 11s 11s +0%
poly_invntt_tomont_c 10s 11s -9%
polyvec_matrix_pointwise_montgomery_row 9s 6s +50%
polyz_unpack_c 9s 8s +12%
rej_uniform_native_x86_64 9s - new
keccak_absorb_once_x4 8s 8s +0%
poly_power2round 8s 4s +100%
rej_uniform 8s 8s +0%
sign_keypair_internal 8s 4s +100%
poly_add 7s 7s +0%
poly_decompose_c 7s 5s +40%
polyz_unpack 7s 3s +133%
mld_compute_pack_z 6s 6s +0%
mld_keccakf1600_permute_c 6s 7s -14%
poly_uniform_gamma1_4x 6s 5s +20%
polyveck_reduce 6s 4s +50%
polyvecl_unpack_eta 6s 4s +50%
sign_pk_from_sk 6s 5s +20%
sign_signature_internal 6s 4s +50%
keccak_absorb 5s 3s +67%
keccak_init 5s 3s +67%
mld_ct_get_optblocker_u8 5s 2s +150%
mld_h 5s 4s +25%
mld_keccakf1600x4_extract_bytes_c 5s 4s +25%
mld_polymat_expand_entry 5s 2s +150%
nttunpack_native_x86_64 5s 4s +25%
pack_sig_z 5s 2s +150%
pointwise_native_aarch64 5s 2s +150%
poly_caddq 5s 4s +25%
poly_caddq_native_x86_64 5s 4s +25%
poly_challenge 5s 6s -17%
poly_reduce 5s 4s +25%
poly_sub 5s 3s +67%
poly_use_hint_native_aarch64 5s 3s +67%
polyt0_pack 5s 4s +25%
polyvecl_pointwise_acc_montgomery 5s 3s +67%
polyw1_pack_32 5s 3s +67%
rej_eta_native 5s 3s +67%
rej_uniform_native 5s 5s +0%
caddq 4s 6s -33%
decompose 4s 3s +33%
keccak_squeezeblocks_x4 4s 3s +33%
keccakf1600_extract_bytes (big endian) 4s 4s +0%
keccakf1600x4_extract_bytes_native 4s 4s +0%
mld_ct_get_optblocker_i64 4s 4s +0%
mld_sample_s1_s2 4s 1s +300%
mld_value_barrier_i64 4s 3s +33%
mld_value_barrier_u32 4s 1s +300%
mld_value_barrier_u8 4s 4s +0%
pointwise_acc_native_x86_64 4s 4s +0%
poly_chknorm_native 4s 4s +0%
poly_decompose_32_native_aarch64 4s 4s +0%
poly_decompose_native_x86_64 4s 2s +100%
poly_ntt_native 4s 3s +33%
poly_pointwise_montgomery 4s 3s +33%
poly_uniform_eta 4s 2s +100%
polyt1_pack 4s 3s +33%
polyvec_matrix_expand 4s 3s +33%
polyvec_matrix_expand_serial 4s 4s +0%
polyveck_invntt_tomont 4s 5s -20%
polyvecl_pointwise_acc_montgomery_native 4s 3s +33%
polyz_unpack_19_native_aarch64 4s 4s +0%
power2round 4s 2s +100%
rej_eta 4s 5s -20%
rej_uniform_eta_native_aarch64 4s 3s +33%
rej_uniform_native_aarch64 4s 3s +33%
shake128x4_absorb_once 4s 2s +100%
shake256_squeeze 4s 2s +100%
sign_keypair 4s 5s -20%
sign_signature_pre_hash_internal 4s 4s +0%
sk_t0hat_get_poly 4s 1s +300%
unpack_sk 4s 3s +33%
unpack_sk_s1hat 4s 3s +33%
fqscale 3s 2s +50%
intt_native_x86_64 3s 2s +50%
keccak_f1600_x1_native_aarch64 3s 3s +0%
keccak_f1600_x1_native_aarch64_v84a 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 3s 3s +0%
keccak_finalize 3s 2s +50%
keccakf1600_xor_bytes (big endian) 3s 6s -50%
keccakf1600x4_permute 3s 4s -25%
keccakf1600x4_xor_bytes 3s 3s +0%
make_hint 3s 3s +0%
mld_ct_cmask_neg_i32 3s 2s +50%
mld_ct_cmask_nonzero_u8 3s 2s +50%
mld_keccakf1600_extract_bytes 3s 2s +50%
mld_prepare_domain_separation_prefix 3s 3s +0%
mld_sample_s1_s2_serial 3s 4s -25%
mld_sign_attempt 3s - new
mld_sign_finish 3s - new
montgomery_reduce 3s 2s +50%
ntt_native_aarch64 3s 4s -25%
ntt_native_x86_64 3s 3s +0%
pack_sig_c 3s 5s -40%
pack_sig_h 3s 4s -25%
pack_sk_rho_key_tr_s2 3s 5s -40%
pack_sk_s1 3s 3s +0%
pointwise_acc_native_aarch64 3s 6s -50%
pointwise_native_x86_64 3s 4s -25%
poly_caddq_c 3s 3s +0%
poly_chknorm 3s 3s +0%
poly_chknorm_native_aarch64 3s 2s +50%
poly_decompose_native 3s 2s +50%
poly_invntt_tomont 3s 2s +50%
poly_invntt_tomont_native 3s 3s +0%
poly_permute_bitrev_to_custom_optional 3s 5s -40%
poly_pointwise_montgomery_native 3s 2s +50%
poly_shiftl 3s 4s -25%
poly_uniform 3s 3s +0%
poly_use_hint_c 3s 5s -40%
poly_use_hint_native 3s 3s +0%
poly_use_hint_native_x86_64 3s - new
polyt1_unpack 3s 2s +50%
polyveck_caddq 3s 3s +0%
polyveck_ntt 3s 2s +50%
polyveck_unpack_eta 3s 2s +50%
polyvecl_pack_eta 3s 2s +50%
polyvecl_pointwise_acc_montgomery_c 3s 4s -25%
polyvecl_uniform_gamma1 3s 2s +50%
polyw1_pack 3s 4s -25%
polyz_unpack_native 3s 3s +0%
reduce32 3s 3s +0%
rej_eta_c 3s 4s -25%
shake128_release 3s 2s +50%
shake256_absorb 3s 2s +50%
shake256_init 3s 4s -25%
sig_unpack_hints 3s 2s +50%
sign_signature 3s 6s -50%
sign_signature_pre_hash_shake256 3s 4s -25%
sign_verify_extmu 3s 5s -40%
sign_verify_pre_hash_internal 3s 5s -40%
sign_verify_pre_hash_shake256 3s 5s -40%
unpack_pk_t1 3s 3s +0%
unpack_sk_s2hat 3s 4s -25%
unpack_sk_t0hat 3s 2s +50%
yvec_init 3s 1s +200%
intt_native_aarch64 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 2s 2s +0%
keccak_f1600_x4_native_avx2 2s 2s +0%
keccak_squeeze 2s 2s +0%
keccakf1600_permute 2s 2s +0%
keccakf1600_permute_native 2s 3s -33%
mld_ct_abs_i32 2s 3s -33%
mld_ct_cmask_nonzero_u32 2s 3s -33%
mld_ct_get_optblocker_u32 2s 2s +0%
mld_ct_sel_int32 2s 3s -33%
mld_keccakf1600x4_xor_bytes_c 2s 4s -50%
mld_sign_resume 2s - new
poly_caddq_native 2s 3s -33%
poly_caddq_native_aarch64 2s 3s -33%
poly_decompose 2s 2s +0%
poly_decompose_88_native_aarch64 2s 3s -33%
poly_ntt 2s 3s -33%
poly_permute_bitrev_to_custom_optional_native 2s 3s -33%
poly_uniform_4x 2s 3s -33%
poly_uniform_gamma1 2s 3s -33%
poly_use_hint 2s 2s +0%
polyeta_pack 2s 3s -33%
polyveck_pack_eta 2s 4s -50%
polyveck_pack_w1 2s 3s -33%
polyvecl_ntt 2s 3s -33%
polyvecl_unpack_z 2s 3s -33%
polyw1_pack_88 2s 2s +0%
polyz_pack 2s 2s +0%
polyz_unpack_17_native_aarch64 2s 2s +0%
polyz_unpack_native_x86_64 2s 3s -33%
shake128_absorb 2s 3s -33%
shake256 2s 1s +100%
shake256_release 2s 1s +100%
shake256x4_squeezeblocks 2s 2s +0%
sign_signature_extmu 2s 4s -50%
sign_verify 2s 4s -50%
sk_s2hat_get_poly 2s 5s -60%
sys_check_capability 2s 2s +0%
use_hint 2s 2s +0%
keccakf1600_xor_bytes 1s 3s -67%
keccakf1600x4_extract_bytes 1s 2s -50%
keccakf1600x4_xor_bytes_native 1s 5s -80%
mld_ct_memcmp 1s 1s +0%
poly_chknorm_native_x86_64 1s 2s -50%
polyvecl_uniform_gamma1_serial 1s 2s -50%
shake128_finalize 1s 3s -67%
shake128_init 1s 2s -50%
shake128_squeeze 1s 2s -50%
shake128x4_squeezeblocks 1s 2s -50%
shake256_finalize 1s 2s -50%
shake256x4_absorb_once 1s 1s +0%
sk_s1hat_get_poly 1s 2s -50%
yvec_get_poly 1s 3s -67%

@oqs-bot

oqs-bot commented Jun 28, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

Full Results (209 proofs)
Proof Status Current Previous Change
**TOTAL** 1815s 1784s +1.7%
polyvecl_pointwise_acc_montgomery_c 208s 210s -1%
sign_verify_internal 168s 177s -5%
poly_pointwise_montgomery_c 126s 125s +1%
polyvec_matrix_expand 108s 110s -2%
mld_invntt_layer 103s 109s -6%
mld_attempt_signature_generation 63s 63s +0%
sign_signature_internal 61s 55s +11%
mld_ntt_layer 45s 41s +10%
fqmul 42s 40s +5%
polyvec_matrix_expand_serial 29s 27s +7%
keccakf1600x4_permute_native 24s 23s +4%
mld_ntt_butterfly_block 23s 24s -4%
polyvec_matrix_pointwise_montgomery_yvec 20s 18s +11%
poly_ntt_c 19s 19s +0%
compute_pack_t0_t1 17s 13s +31%
poly_chknorm_c 15s 15s +0%
polyt0_unpack 15s 16s -6%
mld_check_pct 14s 14s +0%
poly_uniform_eta_4x 14s 14s +0%
polyveck_decompose 14s 12s +17%
rej_uniform 14s 18s -22%
rej_uniform_c 14s 14s +0%
poly_uniform_4x 13s 13s +0%
poly_invntt_tomont_c 11s 11s +0%
polyz_unpack_c 11s 13s -15%
keccak_absorb_once_x4 9s 8s +12%
mld_keccakf1600_permute_c 8s 6s +33%
pointwise_acc_native_aarch64 8s 6s +33%
polyveck_ntt 8s 7s +14%
rej_uniform_native_x86_64 8s - new
mld_compute_pack_z 7s 7s +0%
poly_add 7s 9s -22%
poly_decompose_c 7s 5s +40%
polyveck_caddq 7s 6s +17%
polyveck_invntt_tomont 7s 8s -12%
rej_uniform_native 7s 4s +75%
sign_pk_from_sk 7s 6s +17%
poly_invntt_tomont_native 6s 2s +200%
shake256_release 6s 2s +200%
sign_signature 6s 6s +0%
sign_signature_pre_hash_internal 6s 3s +100%
keccak_absorb 5s 3s +67%
mld_h 5s 2s +150%
mld_polymat_expand_entry 5s 4s +25%
mld_value_barrier_i64 5s 2s +150%
pointwise_acc_native_x86_64 5s 8s -38%
poly_decompose_32_native_aarch64 5s 3s +67%
poly_invntt_tomont 5s 3s +67%
poly_ntt 5s 2s +150%
poly_power2round 5s 4s +25%
poly_uniform_gamma1 5s 3s +67%
poly_use_hint_c 5s 5s +0%
polyeta_unpack 5s 8s -38%
polyz_unpack_native 5s 4s +25%
rej_uniform_native_aarch64 5s 3s +67%
sign_keypair 5s 3s +67%
sign_signature_pre_hash_shake256 5s 3s +67%
sign_verify_extmu 5s 3s +67%
sign_verify_pre_hash_internal 5s 5s +0%
sign_verify_pre_hash_shake256 5s 5s +0%
sk_s1hat_get_poly 5s 6s -17%
yvec_init 5s 3s +67%
caddq 4s 3s +33%
intt_native_x86_64 4s 3s +33%
keccak_squeezeblocks_x4 4s 5s -20%
keccakf1600_extract_bytes (big endian) 4s 2s +100%
keccakf1600_permute_native 4s 3s +33%
keccakf1600x4_xor_bytes_native 4s 3s +33%
mld_sample_s1_s2 4s 6s -33%
mld_sign_attempt 4s - new
mld_sign_resume 4s - new
ntt_native_x86_64 4s 2s +100%
poly_caddq_native_x86_64 4s 3s +33%
poly_challenge 4s 6s -33%
poly_chknorm_native_x86_64 4s 3s +33%
poly_decompose 4s 2s +100%
poly_pointwise_montgomery_native 4s 3s +33%
poly_shiftl 4s 3s +33%
poly_uniform 4s 4s +0%
poly_use_hint_native 4s 2s +100%
polyeta_pack 4s 3s +33%
polyt1_unpack 4s 5s -20%
polyveck_chknorm 4s 6s -33%
polyveck_pack_w1 4s 3s +33%
polyveck_unpack_eta 4s 6s -33%
polyvecl_chknorm 4s 7s -43%
polyvecl_ntt 4s 4s +0%
polyvecl_pointwise_acc_montgomery_native 4s 2s +100%
polyvecl_uniform_gamma1 4s 2s +100%
polyvecl_uniform_gamma1_serial 4s 3s +33%
rej_eta 4s 2s +100%
shake128_squeeze 4s 2s +100%
shake128x4_absorb_once 4s 3s +33%
unpack_pk_t1 4s 5s -20%
unpack_sk_s1hat 4s 2s +100%
unpack_sk_t0hat 4s 5s -20%
decompose 3s 1s +200%
fqscale 3s 3s +0%
keccak_f1600_x1_native_aarch64 3s 2s +50%
keccak_f1600_x1_native_aarch64_v84a 3s 3s +0%
keccak_f1600_x4_native_aarch64_v84a 3s 4s -25%
keccak_squeeze 3s 4s -25%
keccakf1600_xor_bytes 3s 2s +50%
keccakf1600x4_extract_bytes_native 3s 4s -25%
keccakf1600x4_permute 3s 4s -25%
make_hint 3s 2s +50%
mld_ct_cmask_nonzero_u32 3s 4s -25%
mld_ct_cmask_nonzero_u8 3s 3s +0%
mld_ct_get_optblocker_i64 3s 2s +50%
mld_ct_get_optblocker_u8 3s 2s +50%
mld_ct_memcmp 3s 2s +50%
mld_ct_sel_int32 3s 3s +0%
mld_keccakf1600x4_extract_bytes_c 3s 3s +0%
mld_prepare_domain_separation_prefix 3s 2s +50%
mld_sample_s1_s2_serial 3s 4s -25%
montgomery_reduce 3s 4s -25%
ntt_native_aarch64 3s 2s +50%
pack_sig_c 3s 5s -40%
pack_sig_h 3s 5s -40%
pack_sig_z 3s 2s +50%
pack_sk_s1 3s 5s -40%
poly_caddq_native 3s 2s +50%
poly_caddq_native_aarch64 3s 2s +50%
poly_chknorm_native_aarch64 3s 3s +0%
poly_decompose_88_native_aarch64 3s 1s +200%
poly_decompose_native_x86_64 3s 3s +0%
poly_reduce 3s 3s +0%
poly_sub 3s 3s +0%
poly_uniform_eta 3s 4s -25%
polyt1_pack 3s 3s +0%
polyveck_reduce 3s 4s -25%
polyvecl_unpack_eta 3s 3s +0%
polyvecl_unpack_z 3s 3s +0%
polyw1_pack 3s 4s -25%
polyw1_pack_88 3s 2s +50%
polyz_unpack 3s 3s +0%
rej_eta_c 3s 5s -40%
rej_eta_native 3s 3s +0%
rej_uniform_eta_native_aarch64 3s 4s -25%
shake128_init 3s 2s +50%
shake128_release 3s 3s +0%
shake256_absorb 3s 2s +50%
shake256x4_absorb_once 3s 3s +0%
sig_unpack_hints 3s 2s +50%
sign_keypair_internal 3s 5s -40%
sign_verify 3s 3s +0%
sk_s2hat_get_poly 3s 2s +50%
unpack_sk_s2hat 3s 4s -25%
yvec_get_poly 3s 3s +0%
intt_native_aarch64 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 2s 2s +0%
keccak_f1600_x4_native_avx2 2s 2s +0%
keccakf1600_permute 2s 2s +0%
keccakf1600x4_extract_bytes 2s 4s -50%
mld_ct_abs_i32 2s 2s +0%
mld_ct_cmask_neg_i32 2s 2s +0%
mld_ct_get_optblocker_u32 2s 3s -33%
mld_keccakf1600_extract_bytes 2s 1s +100%
mld_keccakf1600x4_xor_bytes_c 2s 2s +0%
mld_sign_finish 2s - new
mld_value_barrier_u8 2s 3s -33%
nttunpack_native_x86_64 2s 3s -33%
pack_sk_rho_key_tr_s2 2s 2s +0%
pointwise_native_aarch64 2s 5s -60%
pointwise_native_x86_64 2s 3s -33%
poly_caddq 2s 2s +0%
poly_caddq_c 2s 2s +0%
poly_chknorm 2s 4s -50%
poly_chknorm_native 2s 2s +0%
poly_ntt_native 2s 4s -50%
poly_permute_bitrev_to_custom_optional 2s 2s +0%
poly_permute_bitrev_to_custom_optional_native 2s 4s -50%
poly_uniform_gamma1_4x 2s 4s -50%
poly_use_hint 2s 3s -33%
poly_use_hint_native_aarch64 2s 3s -33%
poly_use_hint_native_x86_64 2s - new
polyvec_matrix_pointwise_montgomery_row 2s 1s +100%
polyveck_pack_eta 2s 4s -50%
polyvecl_pack_eta 2s 3s -33%
polyvecl_pointwise_acc_montgomery 2s 3s -33%
polyz_pack 2s 3s -33%
polyz_unpack_17_native_aarch64 2s 3s -33%
polyz_unpack_19_native_aarch64 2s 3s -33%
polyz_unpack_native_x86_64 2s 3s -33%
power2round 2s 1s +100%
reduce32 2s 3s -33%
shake128_absorb 2s 2s +0%
shake128_finalize 2s 1s +100%
shake128x4_squeezeblocks 2s 3s -33%
shake256 2s 2s +0%
shake256_finalize 2s 1s +100%
shake256_squeeze 2s 3s -33%
shake256x4_squeezeblocks 2s 2s +0%
sign_signature_extmu 2s 2s +0%
sk_t0hat_get_poly 2s 2s +0%
sys_check_capability 2s 4s -50%
unpack_sk 2s 3s -33%
use_hint 2s 2s +0%
keccak_finalize 1s 2s -50%
keccak_init 1s 1s +0%
keccakf1600_xor_bytes (big endian) 1s 2s -50%
keccakf1600x4_xor_bytes 1s 1s +0%
mld_value_barrier_u32 1s 3s -67%
poly_decompose_native 1s 3s -67%
poly_pointwise_montgomery 1s 3s -67%
polyt0_pack 1s 3s -67%
polyw1_pack_32 1s 4s -75%
shake256_init 1s 2s -50%

@oqs-bot

oqs-bot commented Jun 28, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

Full Results (209 proofs)
Proof Status Current Previous Change
**TOTAL** 1625s 1514s +7.3%
polyvecl_pointwise_acc_montgomery_c 152s 131s +16%
poly_pointwise_montgomery_c 128s 114s +12%
sign_verify_internal 124s 114s +9%
mld_invntt_layer 114s 107s +7%
mld_attempt_signature_generation 60s 58s +3%
compute_pack_t0_t1 51s 50s +2%
mld_ntt_layer 45s 42s +7%
fqmul 40s 39s +3%
polyvec_matrix_expand 28s 28s +0%
sign_signature_internal 27s 26s +4%
keccakf1600x4_permute_native 23s 22s +5%
mld_ntt_butterfly_block 21s 23s -9%
poly_ntt_c 19s 19s +0%
polyvec_matrix_pointwise_montgomery_yvec 17s 15s +13%
polyeta_unpack 16s 14s +14%
polyt0_unpack 16s 15s +7%
rej_uniform 16s 18s -11%
rej_uniform_c 16s 15s +7%
poly_chknorm_c 15s 17s -12%
poly_invntt_tomont_c 15s 11s +36%
poly_uniform_4x 13s 14s -7%
mld_check_pct 12s 14s -14%
poly_uniform_eta_4x 12s 11s +9%
polyvecl_chknorm 10s 10s +0%
polyz_unpack_c 10s 11s -9%
rej_uniform_native_x86_64 10s - new
polyvec_matrix_expand_serial 9s 8s +12%
keccak_absorb_once_x4 8s 9s -11%
mld_compute_pack_z 8s 7s +14%
pointwise_acc_native_x86_64 8s 7s +14%
poly_decompose_32_native_aarch64 8s 2s +300%
poly_add 7s 7s +0%
mld_keccakf1600_permute_c 6s 8s -25%
mld_prepare_domain_separation_prefix 6s 4s +50%
poly_chknorm_native 6s 4s +50%
poly_decompose_native_x86_64 6s 3s +100%
poly_power2round 6s 4s +50%
poly_uniform 6s 6s +0%
polyt1_unpack 6s 5s +20%
polyveck_chknorm 6s 5s +20%
power2round 6s 3s +100%
rej_uniform_native 6s 4s +50%
keccak_squeeze 5s 1s +400%
mld_h 5s 4s +25%
mld_polymat_expand_entry 5s 3s +67%
poly_caddq_native_aarch64 5s 4s +25%
poly_challenge 5s 3s +67%
poly_decompose_c 5s 4s +25%
poly_uniform_eta 5s 5s +0%
polyveck_invntt_tomont 5s 5s +0%
polyvecl_ntt 5s 2s +150%
polyw1_pack 5s 3s +67%
polyw1_pack_32 5s 2s +150%
polyz_pack 5s 2s +150%
polyz_unpack_17_native_aarch64 5s 5s +0%
polyz_unpack_native_x86_64 5s 3s +67%
sign_keypair 5s 4s +25%
sign_signature_pre_hash_shake256 5s 3s +67%
sign_verify 5s 4s +25%
sign_verify_pre_hash_shake256 5s 5s +0%
sk_s1hat_get_poly 5s 3s +67%
caddq 4s 2s +100%
intt_native_x86_64 4s 4s +0%
keccak_f1600_x1_native_aarch64_v84a 4s 3s +33%
keccakf1600_extract_bytes (big endian) 4s 2s +100%
keccakf1600x4_xor_bytes 4s 2s +100%
mld_ct_cmask_neg_i32 4s 3s +33%
mld_ct_get_optblocker_u8 4s 1s +300%
mld_ct_memcmp 4s 3s +33%
mld_sample_s1_s2 4s 4s +0%
mld_sign_resume 4s - new
pack_sig_c 4s 2s +100%
pack_sk_rho_key_tr_s2 4s 3s +33%
pointwise_acc_native_aarch64 4s 4s +0%
pointwise_native_x86_64 4s 4s +0%
poly_caddq_c 4s 2s +100%
poly_chknorm_native_aarch64 4s 4s +0%
poly_decompose_native 4s 3s +33%
poly_ntt 4s 3s +33%
poly_reduce 4s 3s +33%
poly_use_hint_c 4s 3s +33%
polyt0_pack 4s 2s +100%
polyveck_caddq 4s 3s +33%
polyveck_decompose 4s 4s +0%
polyveck_ntt 4s 5s -20%
polyveck_reduce 4s 5s -20%
polyveck_unpack_eta 4s 2s +100%
polyvecl_pointwise_acc_montgomery_native 4s 2s +100%
reduce32 4s 2s +100%
rej_uniform_eta_native_aarch64 4s 2s +100%
rej_uniform_native_aarch64 4s 5s -20%
sig_unpack_hints 4s 2s +100%
sign_pk_from_sk 4s 5s -20%
sign_verify_pre_hash_internal 4s 3s +33%
unpack_sk_s1hat 4s 1s +300%
unpack_sk_t0hat 4s 3s +33%
decompose 3s 2s +50%
intt_native_aarch64 3s 9s -67%
keccak_absorb 3s 5s -40%
keccak_f1600_x4_native_aarch64_v84a 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 3s 1s +200%
keccak_squeezeblocks_x4 3s 4s -25%
keccakf1600_permute_native 3s 3s +0%
keccakf1600x4_extract_bytes_native 3s 3s +0%
keccakf1600x4_permute 3s 4s -25%
make_hint 3s 3s +0%
mld_ct_cmask_nonzero_u32 3s 2s +50%
mld_ct_get_optblocker_i64 3s 4s -25%
mld_keccakf1600x4_xor_bytes_c 3s 2s +50%
mld_sample_s1_s2_serial 3s 3s +0%
mld_sign_finish 3s - new
mld_value_barrier_i64 3s 2s +50%
montgomery_reduce 3s 3s +0%
ntt_native_x86_64 3s 3s +0%
pack_sk_s1 3s 2s +50%
poly_caddq_native 3s 5s -40%
poly_caddq_native_x86_64 3s 4s -25%
poly_decompose 3s 3s +0%
poly_decompose_88_native_aarch64 3s 4s -25%
poly_invntt_tomont 3s 4s -25%
poly_invntt_tomont_native 3s 4s -25%
poly_permute_bitrev_to_custom_optional_native 3s 4s -25%
poly_pointwise_montgomery 3s 3s +0%
poly_shiftl 3s 3s +0%
poly_sub 3s 3s +0%
poly_uniform_gamma1_4x 3s 5s -40%
poly_use_hint_native 3s 4s -25%
poly_use_hint_native_aarch64 3s 2s +50%
poly_use_hint_native_x86_64 3s - new
polyeta_pack 3s 3s +0%
polyvec_matrix_pointwise_montgomery_row 3s 2s +50%
polyveck_pack_eta 3s 2s +50%
polyvecl_pack_eta 3s 3s +0%
polyvecl_unpack_z 3s 2s +50%
polyw1_pack_88 3s 1s +200%
rej_eta 3s 3s +0%
rej_eta_c 3s 4s -25%
rej_eta_native 3s 6s -50%
shake256 3s 1s +200%
shake256_release 3s 2s +50%
shake256x4_absorb_once 3s 3s +0%
shake256x4_squeezeblocks 3s 4s -25%
sign_keypair_internal 3s 4s -25%
sign_signature 3s 3s +0%
sign_signature_extmu 3s 4s -25%
sk_s2hat_get_poly 3s 2s +50%
unpack_pk_t1 3s 5s -40%
unpack_sk 3s 3s +0%
yvec_get_poly 3s 3s +0%
fqscale 2s 3s -33%
keccak_f1600_x1_native_aarch64 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 2s 3s -33%
keccak_f1600_x4_native_avx2 2s 3s -33%
keccak_finalize 2s 3s -33%
keccakf1600_permute 2s 2s +0%
keccakf1600_xor_bytes 2s 1s +100%
keccakf1600_xor_bytes (big endian) 2s 4s -50%
keccakf1600x4_extract_bytes 2s 2s +0%
keccakf1600x4_xor_bytes_native 2s 3s -33%
mld_ct_cmask_nonzero_u8 2s 2s +0%
mld_keccakf1600x4_extract_bytes_c 2s 2s +0%
mld_sign_attempt 2s - new
mld_value_barrier_u8 2s 3s -33%
ntt_native_aarch64 2s 3s -33%
nttunpack_native_x86_64 2s 1s +100%
pack_sig_h 2s 3s -33%
pack_sig_z 2s 4s -50%
pointwise_native_aarch64 2s 5s -60%
poly_caddq 2s 2s +0%
poly_chknorm 2s 4s -50%
poly_chknorm_native_x86_64 2s 2s +0%
poly_ntt_native 2s 5s -60%
poly_permute_bitrev_to_custom_optional 2s 2s +0%
poly_pointwise_montgomery_native 2s 2s +0%
poly_uniform_gamma1 2s 4s -50%
poly_use_hint 2s 4s -50%
polyt1_pack 2s 4s -50%
polyveck_pack_w1 2s 1s +100%
polyvecl_pointwise_acc_montgomery 2s 4s -50%
polyvecl_uniform_gamma1 2s 3s -33%
polyvecl_uniform_gamma1_serial 2s 2s +0%
polyvecl_unpack_eta 2s 2s +0%
polyz_unpack 2s 3s -33%
polyz_unpack_19_native_aarch64 2s 5s -60%
polyz_unpack_native 2s 2s +0%
shake128_absorb 2s 2s +0%
shake128_finalize 2s 2s +0%
shake128_init 2s 3s -33%
shake128_release 2s 1s +100%
shake128_squeeze 2s 1s +100%
shake128x4_absorb_once 2s 3s -33%
shake256_absorb 2s 3s -33%
shake256_finalize 2s 2s +0%
shake256_init 2s 3s -33%
shake256_squeeze 2s 2s +0%
sign_signature_pre_hash_internal 2s 6s -67%
sign_verify_extmu 2s 3s -33%
sk_t0hat_get_poly 2s 2s +0%
sys_check_capability 2s 4s -50%
unpack_sk_s2hat 2s 4s -50%
use_hint 2s 2s +0%
yvec_init 2s 3s -33%
keccak_init 1s 3s -67%
mld_ct_abs_i32 1s 2s -50%
mld_ct_get_optblocker_u32 1s 1s +0%
mld_ct_sel_int32 1s 2s -50%
mld_keccakf1600_extract_bytes 1s 2s -50%
mld_value_barrier_u32 1s 2s -50%
shake128x4_squeezeblocks 1s 1s +0%

@oqs-bot

oqs-bot commented Jun 28, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof Status Current Previous Change
sign_signature_internal ⚠️ 113s 42s +169%
Full Results (209 proofs)
Proof Status Current Previous Change
**TOTAL** 2187s 2151s +1.7%
polyvecl_pointwise_acc_montgomery_c 357s 353s +1%
polyvec_matrix_expand 311s 324s -4%
poly_pointwise_montgomery_c 129s 144s -10%
mld_invntt_layer 117s 115s +2%
sign_signature_internal ⚠️ 113s 42s +169%
sign_verify_internal 98s 97s +1%
mld_attempt_signature_generation 55s 55s +0%
mld_ntt_layer 44s 45s -2%
fqmul 42s 43s -2%
polyvec_matrix_expand_serial 37s 38s -3%
mld_ntt_butterfly_block 23s 24s -4%
keccakf1600x4_permute_native 22s 23s -4%
poly_ntt_c 21s 21s +0%
compute_pack_t0_t1 20s 19s +5%
polyvec_matrix_pointwise_montgomery_yvec 18s 18s +0%
poly_chknorm_c 17s 15s +13%
polyeta_unpack 17s 17s +0%
polyt0_unpack 16s 14s +14%
mld_check_pct 15s 16s -6%
rej_uniform 15s 15s +0%
poly_uniform_4x 13s 13s +0%
poly_uniform_eta_4x 13s 11s +18%
rej_uniform_c 13s 19s -32%
mld_compute_pack_z 12s 8s +50%
keccak_absorb_once_x4 11s 9s +22%
poly_invntt_tomont_c 11s 12s -8%
polyveck_caddq 11s 8s +38%
polyveck_ntt 10s 11s -9%
rej_uniform_native_x86_64 10s - new
pointwise_acc_native_x86_64 9s 6s +50%
polyveck_decompose 9s 13s -31%
mld_keccakf1600_permute_c 8s 7s +14%
pointwise_acc_native_aarch64 8s 6s +33%
polyvecl_ntt 8s 7s +14%
poly_challenge 7s 5s +40%
sign_verify_pre_hash_internal 7s 3s +133%
mld_sample_s1_s2 6s 6s +0%
pointwise_native_x86_64 6s 2s +200%
poly_chknorm 6s 3s +100%
poly_pointwise_montgomery 6s 4s +50%
polyveck_invntt_tomont 6s 9s -33%
polyvecl_chknorm 6s 7s -14%
rej_uniform_native 6s 8s -25%
sign_signature_pre_hash_internal 6s 5s +20%
mld_sample_s1_s2_serial 5s 8s -38%
mld_sign_attempt 5s - new
poly_add 5s 6s -17%
poly_ntt 5s 3s +67%
poly_permute_bitrev_to_custom_optional 5s 3s +67%
polyvecl_uniform_gamma1 5s 2s +150%
sign_keypair 5s 4s +25%
sign_keypair_internal 5s 6s -17%
sign_signature_pre_hash_shake256 5s 6s -17%
unpack_sk_t0hat 5s 7s -29%
intt_native_aarch64 4s 3s +33%
intt_native_x86_64 4s 3s +33%
keccak_f1600_x1_native_aarch64 4s 1s +300%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 4s 4s +0%
keccakf1600x4_permute 4s 3s +33%
mld_prepare_domain_separation_prefix 4s 4s +0%
mld_sign_finish 4s - new
mld_sign_resume 4s - new
ntt_native_aarch64 4s 6s -33%
ntt_native_x86_64 4s 2s +100%
pack_sk_s1 4s 1s +300%
pointwise_native_aarch64 4s 5s -20%
poly_caddq_c 4s 3s +33%
poly_caddq_native 4s 4s +0%
poly_chknorm_native_aarch64 4s 4s +0%
poly_decompose_c 4s 5s -20%
poly_uniform 4s 4s +0%
poly_uniform_eta 4s 4s +0%
poly_use_hint 4s 1s +300%
poly_use_hint_native_x86_64 4s - new
polyeta_pack 4s 4s +0%
polyt1_unpack 4s 4s +0%
polyveck_pack_eta 4s 6s -33%
polyveck_pack_w1 4s 3s +33%
polyvecl_unpack_eta 4s 5s -20%
polyw1_pack 4s 4s +0%
polyz_pack 4s 5s -20%
polyz_unpack_19_native_aarch64 4s 4s +0%
polyz_unpack_native 4s 4s +0%
power2round 4s 4s +0%
rej_eta_c 4s 5s -20%
rej_eta_native 4s 6s -33%
rej_uniform_native_aarch64 4s 2s +100%
sign_pk_from_sk 4s 6s -33%
sign_signature 4s 5s -20%
sign_signature_extmu 4s 4s +0%
sign_verify 4s 5s -20%
sk_s2hat_get_poly 4s 3s +33%
sys_check_capability 4s 3s +33%
unpack_pk_t1 4s 1s +300%
unpack_sk 4s 5s -20%
unpack_sk_s1hat 4s 2s +100%
fqscale 3s 3s +0%
keccak_absorb 3s 3s +0%
keccak_f1600_x4_native_aarch64_v84a 3s 4s -25%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 3s 3s +0%
keccak_f1600_x4_native_avx2 3s 2s +50%
keccak_finalize 3s 1s +200%
keccak_squeeze 3s 2s +50%
keccakf1600_extract_bytes (big endian) 3s 3s +0%
keccakf1600_xor_bytes 3s 3s +0%
keccakf1600x4_xor_bytes 3s 3s +0%
make_hint 3s 3s +0%
mld_ct_cmask_neg_i32 3s 4s -25%
mld_ct_sel_int32 3s 3s +0%
mld_h 3s 3s +0%
mld_keccakf1600x4_extract_bytes_c 3s 2s +50%
mld_keccakf1600x4_xor_bytes_c 3s 4s -25%
mld_polymat_expand_entry 3s 3s +0%
mld_value_barrier_i64 3s 1s +200%
mld_value_barrier_u32 3s 2s +50%
mld_value_barrier_u8 3s 3s +0%
pack_sig_c 3s 4s -25%
pack_sig_h 3s 4s -25%
pack_sk_rho_key_tr_s2 3s 3s +0%
poly_caddq_native_x86_64 3s 2s +50%
poly_chknorm_native_x86_64 3s 2s +50%
poly_decompose_32_native_aarch64 3s 5s -40%
poly_decompose_88_native_aarch64 3s 2s +50%
poly_decompose_native_x86_64 3s 2s +50%
poly_pointwise_montgomery_native 3s 5s -40%
poly_reduce 3s 2s +50%
poly_shiftl 3s 4s -25%
poly_sub 3s 3s +0%
poly_uniform_gamma1 3s 4s -25%
poly_uniform_gamma1_4x 3s 3s +0%
poly_use_hint_c 3s 2s +50%
poly_use_hint_native 3s 3s +0%
poly_use_hint_native_aarch64 3s 2s +50%
polyt0_pack 3s 4s -25%
polyveck_reduce 3s 3s +0%
polyveck_unpack_eta 3s 4s -25%
polyvecl_pack_eta 3s 3s +0%
polyvecl_pointwise_acc_montgomery_native 3s 3s +0%
polyvecl_uniform_gamma1_serial 3s 4s -25%
polyw1_pack_32 3s 4s -25%
polyw1_pack_88 3s 3s +0%
polyz_unpack_c 3s 3s +0%
rej_eta 3s 4s -25%
shake128_absorb 3s 4s -25%
shake128_finalize 3s 2s +50%
shake128_init 3s 1s +200%
shake128x4_squeezeblocks 3s 3s +0%
shake256 3s 2s +50%
shake256x4_squeezeblocks 3s 1s +200%
sig_unpack_hints 3s 3s +0%
sign_verify_extmu 3s 3s +0%
sign_verify_pre_hash_shake256 3s 3s +0%
sk_s1hat_get_poly 3s 3s +0%
unpack_sk_s2hat 3s 3s +0%
use_hint 3s 3s +0%
yvec_get_poly 3s 4s -25%
caddq 2s 4s -50%
decompose 2s 3s -33%
keccak_f1600_x1_native_aarch64_v84a 2s 1s +100%
keccak_init 2s 3s -33%
keccak_squeezeblocks_x4 2s 4s -50%
keccakf1600_permute_native 2s 4s -50%
keccakf1600_xor_bytes (big endian) 2s 2s +0%
keccakf1600x4_extract_bytes 2s 2s +0%
keccakf1600x4_xor_bytes_native 2s 3s -33%
mld_ct_abs_i32 2s 3s -33%
mld_ct_cmask_nonzero_u32 2s 2s +0%
mld_ct_cmask_nonzero_u8 2s 3s -33%
mld_ct_get_optblocker_u8 2s 3s -33%
mld_ct_memcmp 2s 3s -33%
mld_keccakf1600_extract_bytes 2s 4s -50%
montgomery_reduce 2s 3s -33%
nttunpack_native_x86_64 2s 3s -33%
pack_sig_z 2s 5s -60%
poly_caddq 2s 2s +0%
poly_caddq_native_aarch64 2s 3s -33%
poly_chknorm_native 2s 4s -50%
poly_decompose_native 2s 2s +0%
poly_invntt_tomont 2s 1s +100%
poly_permute_bitrev_to_custom_optional_native 2s 5s -60%
poly_power2round 2s 3s -33%
polyt1_pack 2s 3s -33%
polyvec_matrix_pointwise_montgomery_row 2s 3s -33%
polyveck_chknorm 2s 3s -33%
polyvecl_pointwise_acc_montgomery 2s 5s -60%
polyvecl_unpack_z 2s 4s -50%
polyz_unpack 2s 2s +0%
polyz_unpack_17_native_aarch64 2s 3s -33%
polyz_unpack_native_x86_64 2s 3s -33%
reduce32 2s 3s -33%
rej_uniform_eta_native_aarch64 2s 5s -60%
shake128_release 2s 4s -50%
shake128_squeeze 2s 2s +0%
shake256_absorb 2s 2s +0%
shake256_finalize 2s 2s +0%
shake256_init 2s 2s +0%
shake256_release 2s 3s -33%
keccakf1600_permute 1s 3s -67%
keccakf1600x4_extract_bytes_native 1s 2s -50%
mld_ct_get_optblocker_i64 1s 3s -67%
mld_ct_get_optblocker_u32 1s 2s -50%
poly_decompose 1s 3s -67%
poly_invntt_tomont_native 1s 5s -80%
poly_ntt_native 1s 3s -67%
shake128x4_absorb_once 1s 5s -80%
shake256_squeeze 1s 2s -50%
shake256x4_absorb_once 1s 2s -50%
sk_t0hat_get_poly 1s 4s -75%
yvec_init 1s 4s -75%

@hanno-becker hanno-becker force-pushed the sign_hooks branch 3 times, most recently from ba5df63 to 004fcc0 Compare June 29, 2026 04:43
@oqs-bot

oqs-bot commented Jun 29, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65, REDUCE-RAM)

Full Results (209 proofs)
Proof Status Current Previous Change
**TOTAL** 1504s 1482s +1.5%
polyvec_matrix_pointwise_montgomery_yvec 200s 201s -0%
poly_pointwise_montgomery_c 115s 116s -1%
mld_invntt_layer 103s 108s -5%
sign_verify_internal 68s 71s -4%
mld_ntt_layer 46s 43s +7%
fqmul 41s 40s +2%
polyvecl_chknorm 40s 43s -7%
polyveck_chknorm 36s 36s +0%
mld_attempt_signature_generation 33s 31s +6%
keccakf1600x4_permute_native 24s 22s +9%
mld_ntt_butterfly_block 22s 25s -12%
poly_ntt_c 21s 22s -5%
rej_uniform_c 17s 16s +6%
mld_check_pct 13s 12s +8%
poly_chknorm_c 12s 13s -8%
poly_uniform_eta_4x 12s 13s -8%
polyveck_decompose 12s 14s -14%
polyt0_unpack 11s 13s -15%
poly_add 10s 7s +43%
keccak_absorb_once_x4 9s 10s -10%
poly_decompose_c 9s 8s +12%
poly_invntt_tomont_c 9s 10s -10%
compute_pack_t0_t1 8s 7s +14%
polyvec_matrix_pointwise_montgomery_row 8s 8s +0%
polyveck_reduce 8s 6s +33%
rej_uniform 8s 7s +14%
rej_uniform_native_x86_64 8s - new
mld_keccakf1600_permute_c 7s 7s +0%
polyz_unpack_c 7s 9s -22%
sign_pk_from_sk 7s 5s +40%
mld_compute_pack_z 6s 5s +20%
pointwise_acc_native_x86_64 6s 5s +20%
poly_power2round 6s 7s -14%
poly_reduce 6s 4s +50%
poly_uniform 6s 2s +200%
polyveck_caddq 6s 7s -14%
polyveck_pack_w1 6s 4s +50%
polyz_unpack_19_native_aarch64 6s 5s +20%
mld_ct_get_optblocker_u8 5s 4s +25%
mld_sample_s1_s2 5s 6s -17%
mld_sample_s1_s2_serial 5s 3s +67%
nttunpack_native_x86_64 5s 3s +67%
poly_caddq_native 5s 4s +25%
poly_decompose_native_x86_64 5s 2s +150%
poly_invntt_tomont 5s 5s +0%
poly_uniform_4x 5s 4s +25%
poly_uniform_gamma1 5s 3s +67%
polyveck_invntt_tomont 5s 7s -29%
polyveck_pack_eta 5s 3s +67%
polyvecl_ntt 5s 7s -29%
polyvecl_pointwise_acc_montgomery_native 5s 3s +67%
polyvecl_uniform_gamma1_serial 5s 1s +400%
polyvecl_unpack_eta 5s 2s +150%
rej_uniform_native 5s 4s +25%
shake128_release 5s 2s +150%
shake256_squeeze 5s 4s +25%
sign_signature_extmu 5s 4s +25%
sign_signature_internal 5s 6s -17%
sign_signature_pre_hash_shake256 5s 7s -29%
sign_verify 5s 6s -17%
sign_verify_pre_hash_internal 5s 5s +0%
fqscale 4s 3s +33%
keccak_squeeze 4s 2s +100%
keccakf1600_xor_bytes 4s 4s +0%
keccakf1600x4_extract_bytes 4s 4s +0%
ntt_native_x86_64 4s 5s -20%
pointwise_acc_native_aarch64 4s 6s -33%
poly_caddq_native_aarch64 4s 2s +100%
poly_chknorm_native 4s 4s +0%
poly_chknorm_native_aarch64 4s 2s +100%
poly_chknorm_native_x86_64 4s 4s +0%
poly_decompose_native 4s 5s -20%
poly_invntt_tomont_native 4s 5s -20%
poly_ntt_native 4s 2s +100%
poly_sub 4s 4s +0%
poly_uniform_eta 4s 5s -20%
poly_uniform_gamma1_4x 4s 3s +33%
poly_use_hint_native_aarch64 4s 4s +0%
polyvec_matrix_expand 4s 6s -33%
polyvec_matrix_expand_serial 4s 3s +33%
polyw1_pack 4s 3s +33%
polyw1_pack_88 4s 3s +33%
polyz_unpack 4s 3s +33%
polyz_unpack_native 4s 3s +33%
polyz_unpack_native_x86_64 4s 3s +33%
rej_uniform_native_aarch64 4s 5s -20%
shake128_absorb 4s 2s +100%
shake256x4_squeezeblocks 4s 2s +100%
sign_keypair 4s 4s +0%
sign_keypair_internal 4s 3s +33%
sign_signature 4s 5s -20%
sign_signature_pre_hash_internal 4s 3s +33%
sk_s1hat_get_poly 4s 3s +33%
unpack_pk_t1 4s 2s +100%
unpack_sk_s1hat 4s 1s +300%
unpack_sk_s2hat 4s 3s +33%
caddq 3s 2s +50%
keccak_absorb 3s 3s +0%
keccak_f1600_x1_native_aarch64 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 3s 3s +0%
keccak_squeezeblocks_x4 3s 4s -25%
keccakf1600_extract_bytes (big endian) 3s 3s +0%
keccakf1600x4_extract_bytes_native 3s 1s +200%
keccakf1600x4_permute 3s 1s +200%
keccakf1600x4_xor_bytes_native 3s 2s +50%
mld_ct_abs_i32 3s 6s -50%
mld_ct_cmask_nonzero_u8 3s 2s +50%
mld_h 3s 3s +0%
mld_keccakf1600x4_extract_bytes_c 3s 2s +50%
mld_keccakf1600x4_xor_bytes_c 3s 2s +50%
mld_polymat_expand_entry 3s 3s +0%
mld_sign_attempt 3s - new
mld_sign_finish 3s - new
mld_value_barrier_i64 3s 2s +50%
mld_value_barrier_u32 3s 4s -25%
pack_sig_c 3s 3s +0%
pack_sig_h 3s 2s +50%
pack_sig_z 3s 1s +200%
pack_sk_rho_key_tr_s2 3s 2s +50%
pointwise_native_aarch64 3s 3s +0%
pointwise_native_x86_64 3s 2s +50%
poly_caddq 3s 3s +0%
poly_caddq_c 3s 5s -40%
poly_caddq_native_x86_64 3s 1s +200%
poly_challenge 3s 5s -40%
poly_chknorm 3s 3s +0%
poly_ntt 3s 2s +50%
poly_permute_bitrev_to_custom_optional 3s 3s +0%
poly_permute_bitrev_to_custom_optional_native 3s 3s +0%
poly_use_hint 3s 3s +0%
poly_use_hint_native_x86_64 3s - new
polyeta_pack 3s 1s +200%
polyeta_unpack 3s 4s -25%
polyt1_pack 3s 3s +0%
polyveck_ntt 3s 4s -25%
polyveck_unpack_eta 3s 3s +0%
polyvecl_pack_eta 3s 2s +50%
polyvecl_pointwise_acc_montgomery_c 3s 3s +0%
polyvecl_unpack_z 3s 1s +200%
polyz_pack 3s 3s +0%
polyz_unpack_17_native_aarch64 3s 2s +50%
rej_eta 3s 5s -40%
rej_eta_c 3s 4s -25%
rej_eta_native 3s 3s +0%
rej_uniform_eta_native_aarch64 3s 5s -40%
shake128_finalize 3s 2s +50%
shake128_init 3s 6s -50%
shake128x4_absorb_once 3s 2s +50%
shake128x4_squeezeblocks 3s 2s +50%
shake256_absorb 3s 4s -25%
sig_unpack_hints 3s 1s +200%
sign_verify_extmu 3s 2s +50%
sk_s2hat_get_poly 3s 1s +200%
sys_check_capability 3s 1s +200%
use_hint 3s 2s +50%
yvec_get_poly 3s 3s +0%
yvec_init 3s 5s -40%
decompose 2s 4s -50%
intt_native_aarch64 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a 2s 2s +0%
keccak_f1600_x4_native_avx2 2s 2s +0%
keccak_finalize 2s 2s +0%
keccakf1600_permute 2s 4s -50%
keccakf1600_permute_native 2s 2s +0%
keccakf1600_xor_bytes (big endian) 2s 2s +0%
keccakf1600x4_xor_bytes 2s 2s +0%
make_hint 2s 3s -33%
mld_ct_cmask_neg_i32 2s 3s -33%
mld_ct_cmask_nonzero_u32 2s 3s -33%
mld_ct_memcmp 2s 4s -50%
mld_ct_sel_int32 2s 2s +0%
mld_prepare_domain_separation_prefix 2s 4s -50%
mld_sign_resume 2s - new
mld_value_barrier_u8 2s 1s +100%
montgomery_reduce 2s 1s +100%
pack_sk_s1 2s 3s -33%
poly_decompose 2s 2s +0%
poly_decompose_32_native_aarch64 2s 4s -50%
poly_decompose_88_native_aarch64 2s 2s +0%
poly_pointwise_montgomery 2s 2s +0%
poly_pointwise_montgomery_native 2s 4s -50%
poly_shiftl 2s 3s -33%
poly_use_hint_c 2s 2s +0%
poly_use_hint_native 2s 7s -71%
polyt0_pack 2s 5s -60%
polyt1_unpack 2s 3s -33%
polyvecl_uniform_gamma1 2s 4s -50%
polyw1_pack_32 2s 2s +0%
power2round 2s 2s +0%
reduce32 2s 2s +0%
shake128_squeeze 2s 3s -33%
shake256 2s 2s +0%
shake256_finalize 2s 1s +100%
shake256_init 2s 4s -50%
shake256x4_absorb_once 2s 2s +0%
sign_verify_pre_hash_shake256 2s 6s -67%
sk_t0hat_get_poly 2s 1s +100%
unpack_sk 2s 3s -33%
unpack_sk_t0hat 2s 4s -50%
intt_native_x86_64 1s 4s -75%
keccak_f1600_x4_native_aarch64_v84a 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 1s 3s -67%
keccak_init 1s 4s -75%
mld_ct_get_optblocker_i64 1s 1s +0%
mld_ct_get_optblocker_u32 1s 3s -67%
mld_keccakf1600_extract_bytes 1s 2s -50%
ntt_native_aarch64 1s 3s -67%
polyvecl_pointwise_acc_montgomery 1s 3s -67%
shake256_release 1s 3s -67%

@oqs-bot

oqs-bot commented Jun 29, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87, REDUCE-RAM)

Full Results (209 proofs)
Proof Status Current Previous Change
**TOTAL** 1395s 1436s -2.9%
polyvec_matrix_pointwise_montgomery_yvec 175s 196s -11%
poly_pointwise_montgomery_c 113s 125s -10%
mld_invntt_layer 101s 111s -9%
mld_ntt_layer 43s 44s -2%
sign_verify_internal 43s 47s -9%
fqmul 39s 39s +0%
mld_attempt_signature_generation 34s 34s +0%
polyvecl_chknorm 32s 38s -16%
keccakf1600x4_permute_native 23s 25s -8%
mld_ntt_butterfly_block 20s 23s -13%
poly_ntt_c 19s 19s +0%
mld_check_pct 16s 15s +7%
polyeta_unpack 15s 13s +15%
rej_uniform_c 15s 18s -17%
poly_uniform_eta_4x 13s 12s +8%
polyveck_decompose 13s 12s +8%
poly_chknorm_c 12s 13s -8%
poly_invntt_tomont_c 12s 9s +33%
compute_pack_t0_t1 11s 12s -8%
polyt0_unpack 11s 14s -21%
polyvec_matrix_pointwise_montgomery_row 11s 13s -15%
keccak_absorb_once_x4 9s 8s +12%
mld_keccakf1600_permute_c 9s 8s +12%
polyveck_chknorm 9s 9s +0%
polyvecl_ntt 9s 8s +12%
pointwise_acc_native_x86_64 8s 8s +0%
polyveck_caddq 8s 8s +0%
polyz_unpack_c 8s 7s +14%
rej_uniform_native_x86_64 8s - new
pointwise_acc_native_aarch64 7s 5s +40%
polyveck_reduce 7s 6s +17%
rej_uniform 7s 7s +0%
intt_native_x86_64 6s 4s +50%
mld_compute_pack_z 6s 6s +0%
mld_sample_s1_s2 6s 8s -25%
mld_sample_s1_s2_serial 6s 6s +0%
nttunpack_native_x86_64 6s 3s +100%
poly_chknorm_native_x86_64 6s 2s +200%
poly_decompose_c 6s 6s +0%
keccak_squeeze 5s 5s +0%
mld_ct_cmask_nonzero_u32 5s 5s +0%
mld_prepare_domain_separation_prefix 5s 3s +67%
pointwise_native_x86_64 5s 5s +0%
poly_add 5s 8s -38%
poly_caddq_c 5s 3s +67%
poly_challenge 5s 4s +25%
poly_power2round 5s 7s -29%
poly_reduce 5s 4s +25%
polyveck_invntt_tomont 5s 4s +25%
rej_uniform_native 5s 5s +0%
sig_unpack_hints 5s 4s +25%
sign_pk_from_sk 5s 6s -17%
sign_verify_pre_hash_shake256 5s 7s -29%
sk_s2hat_get_poly 5s 2s +150%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 4s 2s +100%
keccak_squeezeblocks_x4 4s 4s +0%
keccakf1600_permute_native 4s 3s +33%
mld_ct_cmask_nonzero_u8 4s 2s +100%
mld_ct_sel_int32 4s 2s +100%
mld_h 4s 2s +100%
mld_sign_resume 4s - new
ntt_native_x86_64 4s 2s +100%
pack_sig_h 4s 3s +33%
pack_sk_s1 4s 2s +100%
poly_ntt_native 4s 4s +0%
poly_uniform 4s 4s +0%
poly_uniform_eta 4s 5s -20%
poly_uniform_gamma1 4s 3s +33%
poly_use_hint 4s 4s +0%
poly_use_hint_native_aarch64 4s 3s +33%
polyt0_pack 4s 3s +33%
polyveck_ntt 4s 3s +33%
polyvecl_uniform_gamma1 4s 3s +33%
polyvecl_uniform_gamma1_serial 4s 2s +100%
polyz_unpack_17_native_aarch64 4s 4s +0%
rej_eta_c 4s 4s +0%
rej_eta_native 4s 4s +0%
shake128_init 4s 2s +100%
shake256_absorb 4s 3s +33%
shake256_release 4s 5s -20%
shake256x4_squeezeblocks 4s 4s +0%
sign_keypair 4s 4s +0%
sign_signature_internal 4s 3s +33%
sign_verify 4s 2s +100%
sys_check_capability 4s 2s +100%
unpack_sk_s1hat 4s 3s +33%
fqscale 3s 1s +200%
intt_native_aarch64 3s 4s -25%
keccak_absorb 3s 4s -25%
keccak_finalize 3s 1s +200%
keccakf1600_extract_bytes (big endian) 3s 3s +0%
keccakf1600_xor_bytes (big endian) 3s 2s +50%
mld_ct_abs_i32 3s 1s +200%
mld_ct_cmask_neg_i32 3s 2s +50%
mld_keccakf1600x4_extract_bytes_c 3s 3s +0%
mld_sign_attempt 3s - new
mld_sign_finish 3s - new
pack_sig_c 3s 2s +50%
pack_sig_z 3s 3s +0%
pointwise_native_aarch64 3s 4s -25%
poly_caddq_native 3s 3s +0%
poly_caddq_native_aarch64 3s 3s +0%
poly_caddq_native_x86_64 3s 3s +0%
poly_chknorm_native 3s 1s +200%
poly_chknorm_native_aarch64 3s 5s -40%
poly_decompose 3s 2s +50%
poly_decompose_32_native_aarch64 3s 3s +0%
poly_decompose_88_native_aarch64 3s 2s +50%
poly_decompose_native 3s 2s +50%
poly_decompose_native_x86_64 3s 3s +0%
poly_invntt_tomont 3s 4s -25%
poly_invntt_tomont_native 3s 2s +50%
poly_ntt 3s 2s +50%
poly_permute_bitrev_to_custom_optional 3s 2s +50%
poly_permute_bitrev_to_custom_optional_native 3s 3s +0%
poly_sub 3s 5s -40%
poly_uniform_4x 3s 3s +0%
poly_use_hint_native 3s 1s +200%
polyt1_pack 3s 5s -40%
polyvec_matrix_expand 3s 3s +0%
polyveck_pack_eta 3s 5s -40%
polyvecl_pointwise_acc_montgomery_native 3s 2s +50%
polyvecl_unpack_eta 3s 3s +0%
polyvecl_unpack_z 3s 3s +0%
polyw1_pack 3s 2s +50%
polyw1_pack_88 3s 2s +50%
polyz_pack 3s 4s -25%
polyz_unpack 3s 3s +0%
polyz_unpack_19_native_aarch64 3s 5s -40%
polyz_unpack_native 3s 1s +200%
polyz_unpack_native_x86_64 3s 3s +0%
rej_eta 3s 2s +50%
rej_uniform_native_aarch64 3s 3s +0%
shake128_finalize 3s 2s +50%
shake128_release 3s 3s +0%
shake128_squeeze 3s 1s +200%
shake128x4_squeezeblocks 3s 1s +200%
shake256_squeeze 3s 2s +50%
shake256x4_absorb_once 3s 5s -40%
sign_signature_extmu 3s 4s -25%
sign_signature_pre_hash_internal 3s 2s +50%
sign_signature_pre_hash_shake256 3s 3s +0%
sign_verify_extmu 3s 4s -25%
sign_verify_pre_hash_internal 3s 3s +0%
unpack_sk 3s 4s -25%
caddq 2s 3s -33%
decompose 2s 2s +0%
keccak_f1600_x1_native_aarch64 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a 2s 1s +100%
keccak_f1600_x4_native_avx2 2s 3s -33%
keccakf1600_permute 2s 2s +0%
keccakf1600_xor_bytes 2s 1s +100%
keccakf1600x4_extract_bytes 2s 1s +100%
keccakf1600x4_extract_bytes_native 2s 4s -50%
keccakf1600x4_permute 2s 2s +0%
keccakf1600x4_xor_bytes 2s 1s +100%
keccakf1600x4_xor_bytes_native 2s 2s +0%
make_hint 2s 2s +0%
mld_ct_get_optblocker_i64 2s 2s +0%
mld_ct_get_optblocker_u32 2s 2s +0%
mld_ct_get_optblocker_u8 2s 3s -33%
mld_polymat_expand_entry 2s 4s -50%
mld_value_barrier_u32 2s 3s -33%
mld_value_barrier_u8 2s 2s +0%
montgomery_reduce 2s 2s +0%
ntt_native_aarch64 2s 4s -50%
pack_sk_rho_key_tr_s2 2s 2s +0%
poly_caddq 2s 5s -60%
poly_pointwise_montgomery 2s 3s -33%
poly_pointwise_montgomery_native 2s 3s -33%
poly_use_hint_c 2s 4s -50%
polyeta_pack 2s 3s -33%
polyt1_unpack 2s 3s -33%
polyveck_pack_w1 2s 3s -33%
polyveck_unpack_eta 2s 3s -33%
polyvecl_pack_eta 2s 2s +0%
polyvecl_pointwise_acc_montgomery 2s 2s +0%
polyw1_pack_32 2s 3s -33%
power2round 2s 3s -33%
reduce32 2s 3s -33%
rej_uniform_eta_native_aarch64 2s 3s -33%
shake128_absorb 2s 2s +0%
shake128x4_absorb_once 2s 4s -50%
shake256 2s 3s -33%
shake256_finalize 2s 3s -33%
shake256_init 2s 3s -33%
sign_keypair_internal 2s 6s -67%
sign_signature 2s 4s -50%
sk_s1hat_get_poly 2s 3s -33%
unpack_sk_s2hat 2s 3s -33%
use_hint 2s 3s -33%
yvec_get_poly 2s 2s +0%
yvec_init 2s 4s -50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 1s 2s -50%
keccak_init 1s 1s +0%
mld_ct_memcmp 1s 1s +0%
mld_keccakf1600_extract_bytes 1s 1s +0%
mld_keccakf1600x4_xor_bytes_c 1s 1s +0%
mld_value_barrier_i64 1s 2s -50%
poly_chknorm 1s 4s -75%
poly_shiftl 1s 4s -75%
poly_uniform_gamma1_4x 1s 3s -67%
poly_use_hint_native_x86_64 1s - new
polyvec_matrix_expand_serial 1s 3s -67%
polyvecl_pointwise_acc_montgomery_c 1s 2s -50%
sk_t0hat_get_poly 1s 3s -67%
unpack_pk_t1 1s 2s -50%
unpack_sk_t0hat 1s 4s -75%

@hanno-becker hanno-becker force-pushed the sign_hooks branch 8 times, most recently from b2ef39d to 4acce0a Compare June 29, 2026 10:33
@hanno-becker hanno-becker changed the title [WIP] Add signing hooks for observing signature attempts and implementing restartable signing Add signing hooks for observing signature attempts and implementing restartable signing Jun 29, 2026
@hanno-becker hanno-becker force-pushed the sign_hooks branch 9 times, most recently from ec79a2c to 9686b66 Compare July 1, 2026 18:25
@hanno-becker hanno-becker force-pushed the sign_hooks branch 10 times, most recently from ebcd246 to 815f90d Compare July 12, 2026 18:33
@hanno-becker hanno-becker marked this pull request as draft July 12, 2026 21:08
@hanno-becker hanno-becker force-pushed the sign_hooks branch 2 times, most recently from 76c942b to e0b3cce Compare July 13, 2026 08:57
Move the kappa upper bound MLD_MAX_KAPPA -- the largest counter kappa keeping
the y-sampling nonces within uint16_t -- from sign.c to params.h, beside
MLDSA_L which it derives from. Replace the open-coded `UINT16_MAX - MLDSA_L`
in the polyvec contracts and comments with it. No functional change.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
Functions carrying the optional MLD_CONFIG_CONTEXT_PARAMETER that do not
otherwise use it must consume it to avoid -Wunused-parameter, but only when a
context is actually configured. This was previously done via an #if-guarded
((void)context).

Introduce MLD_CONTEXT_UNUSED(context) in context.h, expanding to
((void)(context)) when a context parameter is configured and to an empty
statement otherwise, and use it in the default (stack) MLD_FREE and in the
skip-PCT stub. No functional change.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
Redefine MLD_MAX_SIGNING_ATTEMPTS as the effective bound on signing attempts:
the configured MLD_CONFIG_MAX_SIGNING_ATTEMPTS if set, otherwise the hard
type-safety bound MLD_MAX_KAPPA / MLDSA_L. mld_get_max_signing_attempts()
returns it directly, and its contract bounds the result by MLD_MAX_KAPPA /
MLDSA_L (the hard bound), independent of the configured value.

This keeps the type-safety bound (used by the loop and casts) distinct from
the configured attempt limit, and prepares for the signing hooks, which clamp
the resume point against the effective bound. No functional change.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker hanno-becker force-pushed the sign_hooks branch 2 times, most recently from 8772ce2 to 915038e Compare July 13, 2026 10:14
@hanno-becker hanno-becker marked this pull request as ready for review July 13, 2026 10:20
@hanno-becker

Copy link
Copy Markdown
Contributor Author

@mkannwischer Thank you for the review!

I changed the distribution test so that a) by default, 2000 iterations are run and a wide error margin allowed, b) a dedicated CI job exercises a larger number of iterations and accordingly checks for a narrower error.

The runtime of ML-DSA signatures is theoretically unbounded. Even the
bound of max 814 signature attempts -- approved by NIST as lowering the
chance of signing failure below 2^{-256} -- leaves a performance
distribution whose peak percentiles can be unacceptable for constrained
systems with strict timing requirements.

The library already provides MLD_CONFIG_MAX_SIGNING_ATTEMPTS to cap the
number of signing attempts. However, FIPS 204 forbids lowering that bound
below 814, rendering the option non-compliant in constrained environments.

As a remedy, this commit introduces three optional 'signing hooks' around
the core rejection-sampling loop, keyed by the attempt counter (the loop
iteration; the spec counter is kappa = attempt*MLDSA_L):

- `attempt = sign_resume()`: Return the attempt to resume the operation
  from. `0` for an initial / non-restartable signing operation.
- `sign_attempt(attempt)`: Called before each attempt. Returns 0 to
  proceed, or non-zero to pause: signing then returns MLD_ERR_SIGNING_PAUSED
  with `attempt` as the resume point.
- `sign_finish(attempt)`: Called on success with the succeeding attempt.

Together, resume + attempt make signing _restartable_: a caller can pause
after a bounded number of attempts and later resume from the recorded
attempt, bounding per-call runtime while keeping a FIPS-compliant overall
bound and reproducing the same signature as an uninterrupted run.

This only works if the consumer drives the deterministic internal API: the
randomized API would choose a fresh seed on each (re-)start, so restarting
could not reproduce the uninterrupted signature. Enabling any of the three
hooks therefore requires MLD_CONFIG_NO_RANDOMIZED_API, which in turn is
incompatible with MLD_CONFIG_KEYGEN_PCT (whose one-shot internal signature
cannot be resumed). A logging-only use -- the attempt hook always returns 0,
with resume/finish merely observing, e.g. to benchmark the per-signature
attempt distribution -- would be safe with the randomized API too, but the
restriction is imposed uniformly on all three hooks for now.

Pausing is independent of MLD_CONFIG_MAX_SIGNING_ATTEMPTS, the upper bound on
the total number of attempts (>= 814 for FIPS 204 compliance) after which
signing gives up with the distinct error MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED; it
must not be lowered as a restart mechanism.

sign_{resume|attempt|finish} can be implemented on mutable globals or on a
context, so they are introduced under the existing MLD_CONFIG_CONTEXT_PARAMETER
wrapper, which lets functions be called with or without an
application-specific context pointer.

This commit adds the core machinery in mldsa/:

- Independent MLD_CONFIG_SIGN_HOOK_{RESUME,ATTEMPT,FINISH} options. When set,
  the integration provides, respectively:

  - `attempt = mld_sign_hook_resume([ctx])`: provide initial/resume attempt
  - `mld_sign_hook_attempt(attempt [, ctx])`: per-attempt hook; pause via
    non-zero return
  - `mld_sign_hook_finish(attempt [, ctx])`: note the succeeding attempt

  The unset dummies leave the default build unchanged.

- The MLD_ERR_SIGNING_PAUSED error code, returned when the attempt hook pauses.

CBMC proofs, a test, and the regenerated configs follow in separate commits.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
Add a FAQ entry to README.md pointing users with real-time / bounded-runtime
requirements at the signing hooks and the examples/restartable_sign example.
Documentation only.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
Verify the three signing-hook call sites added in the previous commit:
mld_sign_resume, mld_sign_attempt and mld_sign_finish. In the CBMC
configuration the hooks reduce to their contract dummies, so each harness
just checks the call-by-contract stub against its (empty) contract, mirroring
how sign.c invokes them (the CBMC config carries no context parameter, so the
`context` argument is consumed by the call macro exactly as at the call
sites).

Also refresh the sign_signature_internal harness Makefile for the reworked
signing loop.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
Add a test analogous to test_alloc, driven by a custom config
(test_sign_hook_config.h) that enables the three signing-hook options and
forward-declares the hook context; the context type and the hook
implementations live in the test.

The hooks pause signing after a configurable number of attempts and resume
from the recorded attempt, letting one context drive:

- a known-answer smoke test, reproducing the test-vector signature both
  one-shot and single-step;
- a restartable-signing equivalence test, checking that pausing after a
  random number of attempts and resuming yields the same signature as an
  uninterrupted run, over many random signing-randomness draws;
- a distribution test, gathering the attempts-per-signature histogram over
  many one-shot signatures and checking the measured attempts/signature
  ratio against the expected geometric mean for the parameter set.

The test requires the internal signing API, so it compiles to a no-op main
under MLD_CONFIG_NO_SIGN_API. The distribution test additionally generates a
fresh key per iteration (the other two use the fixed test-vector key), so it
alone is compiled out under MLD_CONFIG_NO_KEYPAIR_API. Statistics are printed
via printf only (no putchar), so freestanding platforms with a minimal stdio
shim can run it.

Wire it up in the Makefile, the test make fragments and scripts/tests
(new --sign-hook subcommand). Mirror alloc's CI plumbing: add a sign_hook
input to the functest / multi-functest actions and disable it for the
config variations it is incompatible with -- those passing their own
MLD_CONFIG_FILE (would clash with the test's fixed config) and those
enabling MLD_CONFIG_KEYGEN_PCT (the signing hooks require
MLD_CONFIG_NO_RANDOMIZED_API, which is incompatible with the PCT). The
generated configs follow in a separate commit.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
Rerun scripts/autogen after the preceding commits, updating
various files. Done separately to ease reviewing of the core
of the changes.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
Add examples/restartable_sign, demonstrating the MLD_CONFIG_SIGN_HOOK_{RESUME,
ATTEMPT,FINISH} hooks. The example provides the three hooks over a single
global, drives the deterministic signing API in a loop that pauses (via
MLD_ERR_SIGNING_PAUSED) after every attempt and resumes from the recorded
point, and checks that the split, single-step run reproduces both the one-shot
signature and the reference test vector.

Wire it into the examples README, the examples CI job, and scripts/tests.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants