From 115130ba3466cb98ace699c6d795c3b8864bb951 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Sun, 25 Oct 2026 23:45:38 +0800 Subject: [PATCH] Zeroize stack in assembly routines spilling to the stack The x86_64 AVX2 Keccak-f1600x4, the aarch64 scalar/hybrid Keccak-f1600 routines, and the aarch64 rej_uniform{,_eta2,_eta4} routines left data on the stack upon return. Zeroize the used stack locals/buffers before returning, and strengthen the HOL Light specifications to state that the stack region is zero on return. Signed-off-by: Matthias J. Kannwischer --- .../src/mldsa_rej_uniform_aarch64_asm.S | 38 ++++++ .../src/mldsa_rej_uniform_eta2_aarch64_asm.S | 22 ++++ .../src/mldsa_rej_uniform_eta4_aarch64_asm.S | 22 ++++ .../src/mldsa_rej_uniform_aarch64_asm.S | 38 ++++++ .../src/mldsa_rej_uniform_eta2_aarch64_asm.S | 22 ++++ .../src/mldsa_rej_uniform_eta4_aarch64_asm.S | 22 ++++ .../src/keccak_f1600_x1_scalar_aarch64_asm.S | 4 + ...k_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S | 6 + ...00_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S | 6 + .../x86_64/src/keccak_f1600_x4_avx2_asm.S | 27 +++++ .../src/keccak_f1600_x1_scalar_aarch64_asm.S | 2 + ...k_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S | 4 + ...00_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S | 4 + .../x86_64/src/keccak_f1600_x4_avx2_asm.S | 25 ++++ .../src/mldsa_rej_uniform_aarch64_asm.S | 36 ++++++ .../src/mldsa_rej_uniform_eta2_aarch64_asm.S | 20 ++++ .../src/mldsa_rej_uniform_eta4_aarch64_asm.S | 20 ++++ .../keccak_f1600_x1_scalar_aarch64_asm.S | 2 + ...k_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S | 4 + ...00_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S | 4 + .../mldsa/mldsa_rej_uniform_aarch64_asm.S | 36 ++++++ .../mldsa_rej_uniform_eta2_aarch64_asm.S | 20 ++++ .../mldsa_rej_uniform_eta4_aarch64_asm.S | 20 ++++ .../keccak_f1600_x1_scalar_aarch64_asm.ml | 12 +- ..._f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml | 12 +- ...0_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml | 12 +- .../proofs/mldsa_rej_uniform_aarch64_asm.ml | 51 +++++++- .../mldsa_rej_uniform_eta2_aarch64_asm.ml | 90 ++++++++++---- .../mldsa_rej_uniform_eta4_aarch64_asm.ml | 113 ++++++++++++++---- proofs/hol_light/common/stack_zero.ml | 26 ++++ .../x86_64/mldsa/keccak_f1600_x4_avx2_asm.S | 25 ++++ .../x86_64/proofs/keccak_f1600_x4_avx2_asm.ml | 56 +++++++++ 32 files changed, 747 insertions(+), 54 deletions(-) create mode 100644 proofs/hol_light/common/stack_zero.ml diff --git a/dev/aarch64_clean/src/mldsa_rej_uniform_aarch64_asm.S b/dev/aarch64_clean/src/mldsa_rej_uniform_aarch64_asm.S index 2e1a95155e..9af0ac4ead 100644 --- a/dev/aarch64_clean/src/mldsa_rej_uniform_aarch64_asm.S +++ b/dev/aarch64_clean/src/mldsa_rej_uniform_aarch64_asm.S @@ -372,6 +372,44 @@ mld_rej_uniform_final_copy: cmp final_copy_count, #MLDSA_N b.lt mld_rej_uniform_final_copy + // Zeroize the stack buffer + eor val0.16b, val0.16b, val0.16b + mov output_tmp, output_tmp_base + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + mov x0, count b mld_rej_uniform_return diff --git a/dev/aarch64_clean/src/mldsa_rej_uniform_eta2_aarch64_asm.S b/dev/aarch64_clean/src/mldsa_rej_uniform_eta2_aarch64_asm.S index e2c2f2d5df..a5d19a635a 100644 --- a/dev/aarch64_clean/src/mldsa_rej_uniform_eta2_aarch64_asm.S +++ b/dev/aarch64_clean/src/mldsa_rej_uniform_eta2_aarch64_asm.S @@ -308,6 +308,28 @@ mld_rej_uniform_eta2_final_copy: cmp final_copy_count, #MLDSA_N b.lt mld_rej_uniform_eta2_final_copy + // Zeroize the stack buffer + eor val0.16b, val0.16b, val0.16b + mov output_tmp, output_tmp_base + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + mov x0, count pop_stack ret diff --git a/dev/aarch64_clean/src/mldsa_rej_uniform_eta4_aarch64_asm.S b/dev/aarch64_clean/src/mldsa_rej_uniform_eta4_aarch64_asm.S index e0048fe616..8a21f47549 100644 --- a/dev/aarch64_clean/src/mldsa_rej_uniform_eta4_aarch64_asm.S +++ b/dev/aarch64_clean/src/mldsa_rej_uniform_eta4_aarch64_asm.S @@ -288,6 +288,28 @@ mld_rej_uniform_eta4_final_copy: cmp final_copy_count, #MLDSA_N b.lt mld_rej_uniform_eta4_final_copy + // Zeroize the stack buffer + eor val0.16b, val0.16b, val0.16b + mov output_tmp, output_tmp_base + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + mov x0, count pop_stack ret diff --git a/dev/aarch64_opt/src/mldsa_rej_uniform_aarch64_asm.S b/dev/aarch64_opt/src/mldsa_rej_uniform_aarch64_asm.S index 2e1a95155e..9af0ac4ead 100644 --- a/dev/aarch64_opt/src/mldsa_rej_uniform_aarch64_asm.S +++ b/dev/aarch64_opt/src/mldsa_rej_uniform_aarch64_asm.S @@ -372,6 +372,44 @@ mld_rej_uniform_final_copy: cmp final_copy_count, #MLDSA_N b.lt mld_rej_uniform_final_copy + // Zeroize the stack buffer + eor val0.16b, val0.16b, val0.16b + mov output_tmp, output_tmp_base + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + mov x0, count b mld_rej_uniform_return diff --git a/dev/aarch64_opt/src/mldsa_rej_uniform_eta2_aarch64_asm.S b/dev/aarch64_opt/src/mldsa_rej_uniform_eta2_aarch64_asm.S index e2c2f2d5df..a5d19a635a 100644 --- a/dev/aarch64_opt/src/mldsa_rej_uniform_eta2_aarch64_asm.S +++ b/dev/aarch64_opt/src/mldsa_rej_uniform_eta2_aarch64_asm.S @@ -308,6 +308,28 @@ mld_rej_uniform_eta2_final_copy: cmp final_copy_count, #MLDSA_N b.lt mld_rej_uniform_eta2_final_copy + // Zeroize the stack buffer + eor val0.16b, val0.16b, val0.16b + mov output_tmp, output_tmp_base + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + mov x0, count pop_stack ret diff --git a/dev/aarch64_opt/src/mldsa_rej_uniform_eta4_aarch64_asm.S b/dev/aarch64_opt/src/mldsa_rej_uniform_eta4_aarch64_asm.S index e0048fe616..8a21f47549 100644 --- a/dev/aarch64_opt/src/mldsa_rej_uniform_eta4_aarch64_asm.S +++ b/dev/aarch64_opt/src/mldsa_rej_uniform_eta4_aarch64_asm.S @@ -288,6 +288,28 @@ mld_rej_uniform_eta4_final_copy: cmp final_copy_count, #MLDSA_N b.lt mld_rej_uniform_eta4_final_copy + // Zeroize the stack buffer + eor val0.16b, val0.16b, val0.16b + mov output_tmp, output_tmp_base + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + stp val0q, val0q, [output_tmp], #32 + mov x0, count pop_stack ret diff --git a/dev/fips202/aarch64/src/keccak_f1600_x1_scalar_aarch64_asm.S b/dev/fips202/aarch64/src/keccak_f1600_x1_scalar_aarch64_asm.S index 9013937b8b..dfbcb226bc 100644 --- a/dev/fips202/aarch64/src/keccak_f1600_x1_scalar_aarch64_asm.S +++ b/dev/fips202/aarch64/src/keccak_f1600_x1_scalar_aarch64_asm.S @@ -425,6 +425,10 @@ mld_keccak_f1600_x1_scalar_initial: ldr input_addr, [sp, #STACK_LOC_INPUT] store_state + // Zeroize the stack locals + stp xzr, xzr, [sp, #STACK_LOC_INPUT] + stp xzr, xzr, [sp, #STACK_LOC_COUNT] + restore_gprs free_stack ret diff --git a/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S b/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S index 4589f7d041..62a44ae6ae 100644 --- a/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S +++ b/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S @@ -2453,6 +2453,12 @@ mld_keccak_f1600_x4_v8a_scalar_hybrid_done: store_input_scalar 1 store_input_vector + // Zeroize the stack locals + stp xzr, xzr, [sp, #STACK_OFFSET_INPUT] + stp xzr, xzr, [sp, #STACK_OFFSET_CONST_VECTOR] + str xzr, [sp, #STACK_OFFSET_OUTER] + str xzr, [sp, #STACK_LOC_0] + restore_vregs restore_gprs free_stack diff --git a/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S b/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S index b8820f5400..6193cadfd9 100644 --- a/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S +++ b/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S @@ -2283,6 +2283,12 @@ mld_keccak_f1600_x4_v8a_v84a_scalar_hybrid_done: store_input_scalar 1 store_input_vector + // Zeroize the stack locals + stp xzr, xzr, [sp, #STACK_OFFSET_INPUT] + stp xzr, xzr, [sp, #STACK_OFFSET_CONST_VECTOR] + str xzr, [sp, #STACK_OFFSET_OUTER] + str xzr, [sp, #STACK_LOC_0] + restore_vregs restore_gprs free_stack diff --git a/dev/fips202/x86_64/src/keccak_f1600_x4_avx2_asm.S b/dev/fips202/x86_64/src/keccak_f1600_x4_avx2_asm.S index 313f7eca16..4c13c15368 100644 --- a/dev/fips202/x86_64/src/keccak_f1600_x4_avx2_asm.S +++ b/dev/fips202/x86_64/src/keccak_f1600_x4_avx2_asm.S @@ -652,6 +652,33 @@ MLD_ASM_FN_SYMBOL(keccak_f1600_x4_avx2_asm) vmovhpd %xmm3, 0x188(%rdi) vmovq %xmm15, 0x250(%rdi) vmovhpd %xmm15, 0x318(%rdi) + + // Zeroize the stack frame + vpxor %ymm0, %ymm0, %ymm0 + vmovdqu %ymm0, 0x0(%rsp) + vmovdqu %ymm0, 0x20(%rsp) + vmovdqu %ymm0, 0x40(%rsp) + vmovdqu %ymm0, 0x60(%rsp) + vmovdqu %ymm0, 0x80(%rsp) + vmovdqu %ymm0, 0xa0(%rsp) + vmovdqu %ymm0, 0xc0(%rsp) + vmovdqu %ymm0, 0xe0(%rsp) + vmovdqu %ymm0, 0x100(%rsp) + vmovdqu %ymm0, 0x120(%rsp) + vmovdqu %ymm0, 0x140(%rsp) + vmovdqu %ymm0, 0x160(%rsp) + vmovdqu %ymm0, 0x180(%rsp) + vmovdqu %ymm0, 0x1a0(%rsp) + vmovdqu %ymm0, 0x1c0(%rsp) + vmovdqu %ymm0, 0x1e0(%rsp) + vmovdqu %ymm0, 0x200(%rsp) + vmovdqu %ymm0, 0x220(%rsp) + vmovdqu %ymm0, 0x240(%rsp) + vmovdqu %ymm0, 0x260(%rsp) + vmovdqu %ymm0, 0x280(%rsp) + vmovdqu %ymm0, 0x2a0(%rsp) + vmovdqu %ymm0, 0x2c0(%rsp) + vmovdqu %ymm0, 0x2e0(%rsp) /* Clear upper halves of YMM registers to avoid a performance * penalty when switching to SSE. */ vzeroupper diff --git a/mldsa/src/fips202/native/aarch64/src/keccak_f1600_x1_scalar_aarch64_asm.S b/mldsa/src/fips202/native/aarch64/src/keccak_f1600_x1_scalar_aarch64_asm.S index 2b8e426f1f..19de5ca881 100644 --- a/mldsa/src/fips202/native/aarch64/src/keccak_f1600_x1_scalar_aarch64_asm.S +++ b/mldsa/src/fips202/native/aarch64/src/keccak_f1600_x1_scalar_aarch64_asm.S @@ -345,6 +345,8 @@ Lmld_keccak_f1600_x1_scalar_loop: stp x5, x10, [x0, #0xa0] stp x15, x20, [x0, #0xb0] str x25, [x0, #0xc0] + stp xzr, xzr, [sp] + stp xzr, xzr, [sp, #0x10] ldp x19, x20, [sp, #0x20] .cfi_restore x19 .cfi_restore x20 diff --git a/mldsa/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S b/mldsa/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S index 07af46a207..0f768d64d0 100644 --- a/mldsa/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S +++ b/mldsa/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S @@ -1035,6 +1035,10 @@ Lmld_keccak_f1600_x4_v8a_scalar_hybrid_done: str d24, [x0] trn2 v25.2d, v24.2d, v24.2d str d25, [x4] + stp xzr, xzr, [sp] + stp xzr, xzr, [sp, #0x10] + str xzr, [sp, #0x20] + str xzr, [sp, #0xd0] ldp d8, d9, [sp, #0x90] .cfi_restore d8 .cfi_restore d9 diff --git a/mldsa/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S b/mldsa/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S index e7fd82adce..0cae91c54d 100644 --- a/mldsa/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S +++ b/mldsa/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S @@ -943,6 +943,10 @@ Lmld_keccak_f1600_x4_v8a_v84a_scalar_hybrid_done: str d24, [x0] trn2 v25.2d, v24.2d, v24.2d str d25, [x4] + stp xzr, xzr, [sp] + stp xzr, xzr, [sp, #0x10] + str xzr, [sp, #0x20] + str xzr, [sp, #0xd0] ldp d8, d9, [sp, #0x90] .cfi_restore d8 .cfi_restore d9 diff --git a/mldsa/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S b/mldsa/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S index 9697b59bf6..3a79bdb998 100644 --- a/mldsa/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S +++ b/mldsa/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S @@ -474,6 +474,31 @@ LLmld_keccak_f1600_x4_avx2_asm: vmovhpd %xmm3, 0x188(%rdi) vmovq %xmm15, 0x250(%rdi) vmovhpd %xmm15, 0x318(%rdi) + vpxor %ymm0, %ymm0, %ymm0 + vmovdqu %ymm0, (%rsp) + vmovdqu %ymm0, 0x20(%rsp) + vmovdqu %ymm0, 0x40(%rsp) + vmovdqu %ymm0, 0x60(%rsp) + vmovdqu %ymm0, 0x80(%rsp) + vmovdqu %ymm0, 0xa0(%rsp) + vmovdqu %ymm0, 0xc0(%rsp) + vmovdqu %ymm0, 0xe0(%rsp) + vmovdqu %ymm0, 0x100(%rsp) + vmovdqu %ymm0, 0x120(%rsp) + vmovdqu %ymm0, 0x140(%rsp) + vmovdqu %ymm0, 0x160(%rsp) + vmovdqu %ymm0, 0x180(%rsp) + vmovdqu %ymm0, 0x1a0(%rsp) + vmovdqu %ymm0, 0x1c0(%rsp) + vmovdqu %ymm0, 0x1e0(%rsp) + vmovdqu %ymm0, 0x200(%rsp) + vmovdqu %ymm0, 0x220(%rsp) + vmovdqu %ymm0, 0x240(%rsp) + vmovdqu %ymm0, 0x260(%rsp) + vmovdqu %ymm0, 0x280(%rsp) + vmovdqu %ymm0, 0x2a0(%rsp) + vmovdqu %ymm0, 0x2c0(%rsp) + vmovdqu %ymm0, 0x2e0(%rsp) vzeroupper movq %r11, %rsp .cfi_def_cfa_register %rsp diff --git a/mldsa/src/native/aarch64/src/mldsa_rej_uniform_aarch64_asm.S b/mldsa/src/native/aarch64/src/mldsa_rej_uniform_aarch64_asm.S index 9511893de5..cd43594d96 100644 --- a/mldsa/src/native/aarch64/src/mldsa_rej_uniform_aarch64_asm.S +++ b/mldsa/src/native/aarch64/src/mldsa_rej_uniform_aarch64_asm.S @@ -204,6 +204,42 @@ Lmld_rej_uniform_final_copy: add x11, x11, #0x10 cmp x11, #0x100 b.lt Lmld_rej_uniform_final_copy + eor v16.16b, v16.16b, v16.16b + mov x7, x8 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 mov x0, x9 b Lmld_rej_uniform_return diff --git a/mldsa/src/native/aarch64/src/mldsa_rej_uniform_eta2_aarch64_asm.S b/mldsa/src/native/aarch64/src/mldsa_rej_uniform_eta2_aarch64_asm.S index 562f711165..3521d07244 100644 --- a/mldsa/src/native/aarch64/src/mldsa_rej_uniform_eta2_aarch64_asm.S +++ b/mldsa/src/native/aarch64/src/mldsa_rej_uniform_eta2_aarch64_asm.S @@ -153,6 +153,26 @@ Lmld_rej_uniform_eta2_final_copy: add x11, x11, #0x10 cmp x11, #0x100 b.lt Lmld_rej_uniform_eta2_final_copy + eor v16.16b, v16.16b, v16.16b + mov x7, x8 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 mov x0, x9 add sp, sp, #0x240 .cfi_adjust_cfa_offset -0x240 diff --git a/mldsa/src/native/aarch64/src/mldsa_rej_uniform_eta4_aarch64_asm.S b/mldsa/src/native/aarch64/src/mldsa_rej_uniform_eta4_aarch64_asm.S index 114f23f33a..55e13c7dce 100644 --- a/mldsa/src/native/aarch64/src/mldsa_rej_uniform_eta4_aarch64_asm.S +++ b/mldsa/src/native/aarch64/src/mldsa_rej_uniform_eta4_aarch64_asm.S @@ -146,6 +146,26 @@ Lmld_rej_uniform_eta4_final_copy: add x11, x11, #0x10 cmp x11, #0x100 b.lt Lmld_rej_uniform_eta4_final_copy + eor v16.16b, v16.16b, v16.16b + mov x7, x8 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 mov x0, x9 add sp, sp, #0x240 .cfi_adjust_cfa_offset -0x240 diff --git a/proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_scalar_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_scalar_aarch64_asm.S index 0675f30ab3..9e2a5780f8 100644 --- a/proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_scalar_aarch64_asm.S +++ b/proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_scalar_aarch64_asm.S @@ -347,6 +347,8 @@ Lmld_keccak_f1600_x1_scalar_loop: stp x5, x10, [x0, #0xa0] stp x15, x20, [x0, #0xb0] str x25, [x0, #0xc0] + stp xzr, xzr, [sp] + stp xzr, xzr, [sp, #0x10] ldp x19, x20, [sp, #0x20] .cfi_restore x19 .cfi_restore x20 diff --git a/proofs/hol_light/aarch64/mldsa/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S index 9a3914b0fa..a16f08db2b 100644 --- a/proofs/hol_light/aarch64/mldsa/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S +++ b/proofs/hol_light/aarch64/mldsa/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S @@ -1037,6 +1037,10 @@ Lmld_keccak_f1600_x4_v8a_scalar_hybrid_done: str d24, [x0] trn2 v25.2d, v24.2d, v24.2d str d25, [x4] + stp xzr, xzr, [sp] + stp xzr, xzr, [sp, #0x10] + str xzr, [sp, #0x20] + str xzr, [sp, #0xd0] ldp d8, d9, [sp, #0x90] .cfi_restore d8 .cfi_restore d9 diff --git a/proofs/hol_light/aarch64/mldsa/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S index 3392656ad4..58c84d4154 100644 --- a/proofs/hol_light/aarch64/mldsa/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S +++ b/proofs/hol_light/aarch64/mldsa/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S @@ -944,6 +944,10 @@ Lmld_keccak_f1600_x4_v8a_v84a_scalar_hybrid_done: str d24, [x0] trn2 v25.2d, v24.2d, v24.2d str d25, [x4] + stp xzr, xzr, [sp] + stp xzr, xzr, [sp, #0x10] + str xzr, [sp, #0x20] + str xzr, [sp, #0xd0] ldp d8, d9, [sp, #0x90] .cfi_restore d8 .cfi_restore d9 diff --git a/proofs/hol_light/aarch64/mldsa/mldsa_rej_uniform_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/mldsa_rej_uniform_aarch64_asm.S index 2e532d40ae..2855ade2f3 100644 --- a/proofs/hol_light/aarch64/mldsa/mldsa_rej_uniform_aarch64_asm.S +++ b/proofs/hol_light/aarch64/mldsa/mldsa_rej_uniform_aarch64_asm.S @@ -206,6 +206,42 @@ Lmld_rej_uniform_final_copy: add x11, x11, #0x10 cmp x11, #0x100 b.lt Lmld_rej_uniform_final_copy + eor v16.16b, v16.16b, v16.16b + mov x7, x8 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 mov x0, x9 b Lmld_rej_uniform_return diff --git a/proofs/hol_light/aarch64/mldsa/mldsa_rej_uniform_eta2_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/mldsa_rej_uniform_eta2_aarch64_asm.S index f644f29f4d..64f4c23cf1 100644 --- a/proofs/hol_light/aarch64/mldsa/mldsa_rej_uniform_eta2_aarch64_asm.S +++ b/proofs/hol_light/aarch64/mldsa/mldsa_rej_uniform_eta2_aarch64_asm.S @@ -153,6 +153,26 @@ Lmld_rej_uniform_eta2_final_copy: add x11, x11, #0x10 cmp x11, #0x100 b.lt Lmld_rej_uniform_eta2_final_copy + eor v16.16b, v16.16b, v16.16b + mov x7, x8 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 mov x0, x9 add sp, sp, #0x240 .cfi_adjust_cfa_offset -0x240 diff --git a/proofs/hol_light/aarch64/mldsa/mldsa_rej_uniform_eta4_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/mldsa_rej_uniform_eta4_aarch64_asm.S index 6086be9cc5..9ccbfe682d 100644 --- a/proofs/hol_light/aarch64/mldsa/mldsa_rej_uniform_eta4_aarch64_asm.S +++ b/proofs/hol_light/aarch64/mldsa/mldsa_rej_uniform_eta4_aarch64_asm.S @@ -146,6 +146,26 @@ Lmld_rej_uniform_eta4_final_copy: add x11, x11, #0x10 cmp x11, #0x100 b.lt Lmld_rej_uniform_eta4_final_copy + eor v16.16b, v16.16b, v16.16b + mov x7, x8 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 + stp q16, q16, [x7], #0x20 mov x0, x9 add sp, sp, #0x240 .cfi_adjust_cfa_offset -0x240 diff --git a/proofs/hol_light/aarch64/proofs/keccak_f1600_x1_scalar_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/keccak_f1600_x1_scalar_aarch64_asm.ml index eb30bb43aa..32bf5426b9 100644 --- a/proofs/hol_light/aarch64/proofs/keccak_f1600_x1_scalar_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/keccak_f1600_x1_scalar_aarch64_asm.ml @@ -12,6 +12,7 @@ needs "s2n_bignum/arm/proofs/base.ml";; needs "mldsa_native/common/keccak_spec.ml";; +needs "mldsa_native/common/stack_zero.ml";; (**** print_literal_from_elf "aarch64/mldsa/keccak_f1600_x1_scalar_aarch64_asm.o";; ****) @@ -300,6 +301,8 @@ let keccak_f1600_x1_scalar_mc = define_assert_from_elf 0xa90a2805; (* arm_STP X5 X10 X0 (Immediate_Offset (iword (&160))) *) 0xa90b500f; (* arm_STP X15 X20 X0 (Immediate_Offset (iword (&176))) *) 0xf9006019; (* arm_STR X25 X0 (Immediate_Offset (word 192)) *) + 0xa9007fff; (* arm_STP XZR XZR SP (Immediate_Offset (iword (&0))) *) + 0xa9017fff; (* arm_STP XZR XZR SP (Immediate_Offset (iword (&16))) *) 0xa94253f3; (* arm_LDP X19 X20 SP (Immediate_Offset (iword (&32))) *) 0xa9435bf5; (* arm_LDP X21 X22 SP (Immediate_Offset (iword (&48))) *) 0xa94463f7; (* arm_LDP X23 X24 SP (Immediate_Offset (iword (&64))) *) @@ -377,7 +380,8 @@ let KECCAK_F1600_X1_SCALAR_CORRECT = prove wordlist_from_memory(a,25) s = A /\ wordlist_from_memory(rc,24) s = round_constants) (\s. read PC s = word(pc + KECCAK_F1600_X1_SCALAR_CORE_END) /\ - wordlist_from_memory(a,25) s = keccak 24 A) + wordlist_from_memory(a,25) s = keccak 24 A /\ + read (memory :> bytes(stackpointer,32)) s = 0) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30] ,, @@ -478,7 +482,8 @@ let KECCAK_F1600_X1_SCALAR_CORRECT = prove (*** The tail of deferred rotations and writeback ***) GHOST_REGLIST_TAC THEN - ARM_SIM_TAC KECCAK_F1600_X1_SCALAR_EXEC (1--38) THEN + ARM_SIM_TAC KECCAK_F1600_X1_SCALAR_EXEC (1--40) THEN + CONJ_TAC THENL [ALL_TAC; STACK_ZERO_TAC] THEN CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN @@ -504,7 +509,8 @@ let KECCAK_F1600_X1_SCALAR_SUBROUTINE_CORRECT = prove wordlist_from_memory(a,25) s = A /\ wordlist_from_memory(rc,24) s = round_constants) (\s. read PC s = returnaddress /\ - wordlist_from_memory(a,25) s = keccak 24 A) + wordlist_from_memory(a,25) s = keccak 24 A /\ + read (memory :> bytes(word_sub stackpointer (word 128),32)) s = 0) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a,200); memory :> bytes(word_sub stackpointer (word 128),128)])`, diff --git a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml index 14ae71218c..e6f193fee7 100644 --- a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml @@ -12,6 +12,7 @@ needs "s2n_bignum/arm/proofs/base.ml";; needs "mldsa_native/aarch64/proofs/keccak_utils.ml";; +needs "mldsa_native/common/stack_zero.ml";; (**** print_literal_from_elf "aarch64/mldsa/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.o";; ****) @@ -977,6 +978,10 @@ let keccak_f1600_x4_v8a_scalar_mc = define_assert_from_elf 0xfd000018; (* arm_STR D24 X0 (Immediate_Offset (word 0)) *) 0x4ed86b19; (* arm_TRN2 Q25 Q24 Q24 64 128 *) 0xfd000099; (* arm_STR D25 X4 (Immediate_Offset (word 0)) *) + 0xa9007fff; (* arm_STP XZR XZR SP (Immediate_Offset (iword (&0))) *) + 0xa9017fff; (* arm_STP XZR XZR SP (Immediate_Offset (iword (&16))) *) + 0xf90013ff; (* arm_STR XZR SP (Immediate_Offset (word 32)) *) + 0xf9006bff; (* arm_STR XZR SP (Immediate_Offset (word 208)) *) 0x6d4927e8; (* arm_LDP D8 D9 SP (Immediate_Offset (iword (&144))) *) 0x6d4a2fea; (* arm_LDP D10 D11 SP (Immediate_Offset (iword (&160))) *) 0x6d4b37ec; (* arm_LDP D12 D13 SP (Immediate_Offset (iword (&176))) *) @@ -1053,6 +1058,8 @@ let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORRECT = prove wordlist_from_memory(word_add a (word 600),25) s = A4 /\ wordlist_from_memory(rc,24) s = round_constants) (\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END) /\ + read (memory :> bytes(stackpointer,40)) s = 0 /\ + read (memory :> bytes(word_add stackpointer (word 208),8)) s = 0 /\ wordlist_from_memory(a,25) s = keccak 24 A1 /\ wordlist_from_memory(word_add a (word 200),25) s = keccak 24 A2 /\ @@ -1433,8 +1440,9 @@ let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORRECT = prove ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN REWRITE_TAC[GSYM round_constants] THEN ENSURES_INIT_TAC "s0" THEN - ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--83) THEN + ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--87) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + REPLICATE_TAC 2 (CONJ_TAC THENL [STACK_ZERO_TAC; ALL_TAC]) THEN CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN ASM_REWRITE_TAC[] THEN @@ -1467,6 +1475,8 @@ let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_SUBROUTINE_CORRECT = prove wordlist_from_memory(word_add a (word 600),25) s = A4 /\ wordlist_from_memory(rc,24) s = round_constants) (\s. read PC s = returnaddress /\ + read (memory :> bytes(word_sub stackpointer (word 224),40)) s = 0 /\ + read (memory :> bytes(word_sub stackpointer (word 16),8)) s = 0 /\ wordlist_from_memory(a,25) s = keccak 24 A1 /\ wordlist_from_memory(word_add a (word 200),25) s = keccak 24 A2 /\ diff --git a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml index d82ea57e44..63333e0eac 100644 --- a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml @@ -12,6 +12,7 @@ needs "s2n_bignum/arm/proofs/base.ml";; needs "mldsa_native/aarch64/proofs/keccak_utils.ml";; +needs "mldsa_native/common/stack_zero.ml";; (**** print_literal_from_elf "aarch64/mldsa/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.o";; ****) @@ -883,6 +884,10 @@ let keccak_f1600_x4_v8a_v84a_scalar_mc = define_assert_from_elf 0xfd000018; (* arm_STR D24 X0 (Immediate_Offset (word 0)) *) 0x4ed86b19; (* arm_TRN2 Q25 Q24 Q24 64 128 *) 0xfd000099; (* arm_STR D25 X4 (Immediate_Offset (word 0)) *) + 0xa9007fff; (* arm_STP XZR XZR SP (Immediate_Offset (iword (&0))) *) + 0xa9017fff; (* arm_STP XZR XZR SP (Immediate_Offset (iword (&16))) *) + 0xf90013ff; (* arm_STR XZR SP (Immediate_Offset (word 32)) *) + 0xf9006bff; (* arm_STR XZR SP (Immediate_Offset (word 208)) *) 0x6d4927e8; (* arm_LDP D8 D9 SP (Immediate_Offset (iword (&144))) *) 0x6d4a2fea; (* arm_LDP D10 D11 SP (Immediate_Offset (iword (&160))) *) 0x6d4b37ec; (* arm_LDP D12 D13 SP (Immediate_Offset (iword (&176))) *) @@ -958,6 +963,8 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORRECT = prove wordlist_from_memory(word_add a (word 600),25) s = A4 /\ wordlist_from_memory(rc,24) s = round_constants) (\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_END) /\ + read (memory :> bytes(stackpointer,40)) s = 0 /\ + read (memory :> bytes(word_add stackpointer (word 208),8)) s = 0 /\ wordlist_from_memory(a,25) s = keccak 24 A1 /\ wordlist_from_memory(word_add a (word 200),25) s = keccak 24 A2 /\ @@ -1338,8 +1345,9 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORRECT = prove ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN REWRITE_TAC[GSYM round_constants] THEN ENSURES_INIT_TAC "s0" THEN - ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC (1--83) THEN + ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC (1--87) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + REPLICATE_TAC 2 (CONJ_TAC THENL [STACK_ZERO_TAC; ALL_TAC]) THEN CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN ASM_REWRITE_TAC[] THEN @@ -1372,6 +1380,8 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_SUBROUTINE_CORRECT = prove wordlist_from_memory(word_add a (word 600),25) s = A4 /\ wordlist_from_memory(rc,24) s = round_constants) (\s. read PC s = returnaddress /\ + read (memory :> bytes(word_sub stackpointer (word 224),40)) s = 0 /\ + read (memory :> bytes(word_sub stackpointer (word 16),8)) s = 0 /\ wordlist_from_memory(a,25) s = keccak 24 A1 /\ wordlist_from_memory(word_add a (word 200),25) s = keccak 24 A2 /\ diff --git a/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_aarch64_asm.ml index bebbc5950d..15e67d7460 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_aarch64_asm.ml @@ -17,6 +17,7 @@ needs "s2n_bignum/arm/proofs/base.ml";; needs "mldsa_native/common/mldsa_specs.ml";; needs "mldsa_native/aarch64/proofs/aarch64_utils.ml";; needs "mldsa_native/aarch64/proofs/mldsa_rej_uniform_table.ml";; +needs "mldsa_native/common/stack_zero.ml";; (**** print_literal_from_elf "aarch64/mldsa/mldsa_rej_uniform_aarch64_asm.o";; ****) @@ -166,6 +167,42 @@ let mldsa_rej_uniform_mc = define_assert_from_elf 0x9100416b; (* arm_ADD X11 X11 (rvalue (word 16)) *) 0xf104017f; (* arm_CMP X11 (rvalue (word 256)) *) 0x54fffecb; (* arm_BLT (word 2097112) *) + 0x6e301e10; (* arm_EOR_VEC Q16 Q16 Q16 128 *) + 0xaa0803e7; (* arm_MOV X7 X8 *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) 0xaa0903e0; (* arm_MOV X0 X9 *) 0x14000001; (* arm_B (word 4) *) 0x911103ff; (* arm_ADD SP SP (rvalue (word 1088)) *) @@ -496,6 +533,7 @@ let MLDSA_REJ_UNIFORM_CORRECT = prove read(memory :> bytes(buf,val buflen)) s = num_of_wordlist inlist) (\s. read PC s = word(pc + MLDSA_REJ_UNIFORM_CORE_END) /\ + read(memory :> bytes(stackpointer,1088)) s = 0 /\ let outlist = SUB_LIST(0,256) (REJ_SAMPLE inlist) in let outlen = LENGTH outlist in C_RETURN s = word outlen /\ @@ -542,10 +580,9 @@ let MLDSA_REJ_UNIFORM_CORRECT = prove `read (memory :> bytes(stackpointer,8 * 128)) s0` THEN MEMORY_128_FROM_64_TAC "stackpointer" 0 64 THEN ASM_REWRITE_TAC[WORD_ADD_0] THEN STRIP_TAC THEN - ARM_STEPS_TAC MLDSA_REJ_UNIFORM_EXEC (1--182) THEN - ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_EXEC (1--180) THEN SUBGOAL_THEN - `read (memory :> bytes (res,4 * MIN 256 outlen)) s182 = + `read (memory :> bytes (res,4 * MIN 256 outlen)) s180 = num_of_wordlist (SUB_LIST (0,256) outlist:int32 list)` ASSUME_TAC THENL [REWRITE_TAC[NUM_OF_WORDLIST_SUB_LIST_0; DIMINDEX_32] THEN @@ -563,6 +600,11 @@ let MLDSA_REJ_UNIFORM_CORRECT = prove RULE_ASSUM_TAC(CONV_RULE(ONCE_DEPTH_CONV(READ_MEMORY_SPLIT_CONV 1))) THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_EXEC (181--218) THEN + ENSURES_FINAL_STATE_TAC THEN + CONJ_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN + CONJ_TAC THENL [STACK_ZERO_TAC; ALL_TAC] THEN + ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM DISJ_CASES_TAC THENL [SUBGOAL_THEN `SUB_LIST (0,8 * n) (inlist:(24 word)list) = inlist` SUBST_ALL_TAC THENL @@ -1685,6 +1727,7 @@ let MLDSA_REJ_UNIFORM_SUBROUTINE_CORRECT = prove read(memory :> bytes(buf,val buflen)) s = num_of_wordlist inlist) (\s. read PC s = returnaddress /\ + read(memory :> bytes(word_sub stackpointer (word 1088),1088)) s = 0 /\ let outlist = SUB_LIST(0,256) (REJ_SAMPLE inlist) in let outlen = LENGTH outlist in C_RETURN s = word outlen /\ @@ -1874,7 +1917,7 @@ let MLDSA_REJ_UNIFORM_MEMSAFE = prove `read (memory :> bytes(stackpointer,8 * 128)) s0` THEN MEMORY_128_FROM_64_TAC "stackpointer" 0 64 THEN ASM_REWRITE_TAC[WORD_ADD_0] THEN STRIP_TAC THEN - ARM_STEPS_TAC MLDSA_REJ_UNIFORM_EXEC (1--182) THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_EXEC (1--218) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[GSYM REJ_SAMPLE] THEN (* Normalize val(word buflen) if needed *) diff --git a/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta2_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta2_aarch64_asm.ml index fb509cbda4..207980298f 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta2_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta2_aarch64_asm.ml @@ -14,6 +14,7 @@ needs "s2n_bignum/arm/proofs/base.ml";; needs "mldsa_native/aarch64/proofs/aarch64_utils.ml";; needs "mldsa_native/aarch64/proofs/mldsa_rej_uniform_eta_table.ml";; +needs "mldsa_native/common/stack_zero.ml";; (**** print_literal_from_elf "aarch64/mldsa/mldsa_rej_uniform_eta2_aarch64_asm.o";; ****) @@ -112,6 +113,26 @@ let mldsa_rej_uniform_eta2_mc = define_assert_from_elf 0x9100416b; (* arm_ADD X11 X11 (rvalue (word 16)) *) 0xf104017f; (* arm_CMP X11 (rvalue (word 256)) *) 0x54fffdcb; (* arm_BLT (word 2097080) *) + 0x6e301e10; (* arm_EOR_VEC Q16 Q16 Q16 128 *) + 0xaa0803e7; (* arm_MOV X7 X8 *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) 0xaa0903e0; (* arm_MOV X0 X9 *) 0x910903ff; (* arm_ADD SP SP (rvalue (word 576)) *) 0xd65f03c0 (* arm_RET X30 *) @@ -904,6 +925,7 @@ let MLDSA_REJ_UNIFORM_ETA2_CORRECT = prove read(memory :> bytes(buf,val buflen)) s = num_of_wordlist inlist) (\s. read PC s = word(pc + MLDSA_REJ_UNIFORM_ETA2_CORE_END) /\ + read(memory :> bytes(stackpointer,576)) s = 0 /\ let outlist = SUB_LIST(0,256) (REJ_SAMPLE_ETA2_BYTES inlist) in let outlen = LENGTH outlist in C_RETURN s = word outlen /\ @@ -927,7 +949,7 @@ let MLDSA_REJ_UNIFORM_ETA2_CORRECT = prove read PC s = word(pc + 0xfc) /\ read X0 s = res /\ read X4 s = word 256 /\ read X8 s = stackpointer /\ - ALL (nonoverlapping (res,1024)) [(word pc,372); (stackpointer,576)] /\ + ALL (nonoverlapping (res,1024)) [(word pc,452); (stackpointer,576)] /\ ?n. let niblist = REJ_NIBBLES_ETA2(SUB_LIST(0,8*n) inlist) in let niblen = LENGTH niblist in niblen < 272 /\ @@ -938,7 +960,17 @@ let MLDSA_REJ_UNIFORM_ETA2_CORRECT = prove CONJ_TAC THENL [ALL_TAC; - ENSURES_INIT_TAC "s0" THEN + ENSURES_SEQUENCE_TAC `pc + 0x168` + `\s. aligned_bytes_loaded s (word pc) mldsa_rej_uniform_eta2_mc /\ + read PC s = word(pc + 0x168) /\ + read X8 s = stackpointer /\ + let outlist = SUB_LIST(0,256) (REJ_SAMPLE_ETA2_BYTES inlist) in + let outlen = LENGTH outlist in + read X9 s = word outlen /\ + read(memory :> bytes(res,4 * outlen)) s = + num_of_wordlist outlist` THEN + CONJ_TAC THENL + [ENSURES_INIT_TAC "s0" THEN FIRST_X_ASSUM(X_CHOOSE_THEN `nn:num` MP_TAC) THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN ABBREV_TAC `niblist = REJ_NIBBLES_ETA2 @@ -974,7 +1006,7 @@ let MLDSA_REJ_UNIFORM_ETA2_CORRECT = prove ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (241--280) THEN RULE_ASSUM_TAC(CONV_RULE(TOP_DEPTH_CONV WORD_SIMPLE_SUBWORD_CONV)) THEN RULE_ASSUM_TAC(CONV_RULE WORD_REDUCE_CONV) THEN - ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (281--313) THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (281--312) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `LENGTH(SUB_LIST(0,256)(REJ_SAMPLE_ETA2_BYTES inlist):int32 list) = @@ -1071,7 +1103,7 @@ let MLDSA_REJ_UNIFORM_ETA2_CORRECT = prove UNDISCH_TAC `LENGTH(niblist:int16 list) = niblen` THEN DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN - MP_TAC(GEN `k:num` (ISPECL [`s313:armstate`; `stackpointer:int64`; + MP_TAC(GEN `k:num` (ISPECL [`s312:armstate`; `stackpointer:int64`; `niblist:int16 list`; `k:num`] BK_FROM_STACK_GE256)) THEN ASM_REWRITE_TAC[] THEN @@ -1209,7 +1241,7 @@ let MLDSA_REJ_UNIFORM_ETA2_CORRECT = prove [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUB_LIST_REFL THEN REWRITE_TAC[LENGTH_MAP] THEN ASM_ARITH_TAC; ALL_TAC] THEN - MP_TAC(ISPECL [`stackpointer:int64`; `256`; `s313:armstate`] + MP_TAC(ISPECL [`stackpointer:int64`; `256`; `s312:armstate`] BYTES_EXISTS_WORDLIST) THEN REWRITE_TAC[ARITH_RULE `2 * 256 = 512`] THEN DISCH_THEN(X_CHOOSE_THEN `L:int16 list` STRIP_ASSUME_TAC) THEN @@ -1217,7 +1249,7 @@ let MLDSA_REJ_UNIFORM_ETA2_CORRECT = prove ASSUME_TAC THENL [MATCH_MP_TAC PREFIX_FROM_STACK THEN MAP_EVERY EXISTS_TAC - [`stackpointer:int64`; `s313:armstate`] THEN + [`stackpointer:int64`; `s312:armstate`] THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `niblen <= 256` ASSUME_TAC THENL @@ -1239,7 +1271,7 @@ let MLDSA_REJ_UNIFORM_ETA2_CORRECT = prove ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `256 <= LENGTH (L:int16 list)` ASSUME_TAC THENL [ASM_REWRITE_TAC[] THEN ARITH_TAC; ALL_TAC] THEN - MP_TAC(GEN `k:num` (ISPECL [`s313:armstate`; `stackpointer:int64`; + MP_TAC(GEN `k:num` (ISPECL [`s312:armstate`; `stackpointer:int64`; `L:int16 list`; `k:num`] BK_FROM_STACK_GE256)) THEN ASM_REWRITE_TAC[ARITH_RULE `2 * 256 = 512`] THEN @@ -1346,7 +1378,7 @@ let MLDSA_REJ_UNIFORM_ETA2_CORRECT = prove UNDISCH_TAC `LENGTH(niblist:int16 list) = niblen` THEN DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN - MP_TAC(GEN `k:num` (ISPECL [`s313:armstate`; `stackpointer:int64`; + MP_TAC(GEN `k:num` (ISPECL [`s312:armstate`; `stackpointer:int64`; `niblist:int16 list`; `k:num`] BK_FROM_STACK_GE256)) THEN ASM_REWRITE_TAC[] THEN @@ -1456,7 +1488,19 @@ let MLDSA_REJ_UNIFORM_ETA2_CORRECT = prove ASM_SIMP_TAC[BARRETT_RAW_EQ_UMOD] THEN REWRITE_TAC[WORD_SHL_ZERO; WORD_SUBWORD_LO64_FROM_INT128; WORD_SUBWORD_HI64_FROM_INT128] THEN - MATCH_MP_TAC PAIR_MAP_IDX_128 THEN ASM_REWRITE_TAC[]]]] THEN + MATCH_MP_TAC PAIR_MAP_IDX_128 THEN ASM_REWRITE_TAC[]]]; + + CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN + ABBREV_TAC `outlist = SUB_LIST(0,256) (REJ_SAMPLE_ETA2_BYTES inlist)` THEN + ABBREV_TAC `outlen = LENGTH(outlist:int32 list)` THEN + SUBGOAL_THEN `outlen <= 256` ASSUME_TAC THENL + [MAP_EVERY EXPAND_TAC ["outlen"; "outlist"] THEN + REWRITE_TAC[LENGTH_SUB_LIST] THEN ARITH_TAC; ALL_TAC] THEN + ENSURES_INIT_TAC "s0" THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (1--21) THEN + ENSURES_FINAL_STATE_TAC THEN + CONJ_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN + CONJ_TAC THENL [STACK_ZERO_TAC; ASM_REWRITE_TAC[]]]] THEN SUBGOAL_THEN `?N. buflen < 8 * (N + 1) \/ @@ -1547,7 +1591,7 @@ let MLDSA_REJ_UNIFORM_ETA2_CORRECT = prove read Q16 s = word(num_of_wordlist lis0):int128 /\ read Q17 s = word(num_of_wordlist lis1):int128) /\ curlen < 256 /\ - nonoverlapping (stackpointer,576) (word pc,372)` THEN + nonoverlapping (stackpointer,576) (word pc,452)` THEN CONJ_TAC THENL [(* First half: SIMD compute chain — 29 steps *) GHOST_INTRO_TAC `nibbles1:int128` `read Q17` THEN @@ -2018,7 +2062,7 @@ let MLDSA_REJ_UNIFORM_ETA2_CORRECT = prove read X9 s = word niblen /\ read (memory :> bytes (stackpointer,2 * niblen)) s = num_of_wordlist (REJ_NIBBLES_ETA2(SUB_LIST(0,8*N) inlist):int16 list) /\ - ALL (nonoverlapping (res,1024)) [(word pc,372); (stackpointer,576)]` THEN + ALL (nonoverlapping (res,1024)) [(word pc,452); (stackpointer,576)]` THEN CONJ_TAC THENL [(* pc+0xf4 -> pc+0x68: CMP X2,8; BCS back *) ENSURES_INIT_TAC "s0" THEN @@ -2181,6 +2225,7 @@ let MLDSA_REJ_UNIFORM_ETA2_SUBROUTINE_CORRECT = prove read(memory :> bytes(buf,val buflen)) s = num_of_wordlist inlist) (\s. read PC s = returnaddress /\ + read(memory :> bytes(word_sub stackpointer (word 576),576)) s = 0 /\ let outlist = SUB_LIST(0,256) (REJ_SAMPLE_ETA2 inlist) in let outlen = LENGTH outlist in outlen <= 256 /\ @@ -2235,6 +2280,7 @@ let MLDSA_REJ_UNIFORM_ETA2_SUBROUTINE_CORRECT = prove read(memory :> bytes(buf,val buflen)) s = num_of_wordlist inlist) (\s. read PC s = returnaddress /\ + read(memory :> bytes(word_sub stackpointer (word 576),576)) s = 0 /\ let outlist = SUB_LIST(0,256) (REJ_SAMPLE_ETA2_BYTES inlist) in let outlen = LENGTH outlist in @@ -2404,7 +2450,7 @@ let MLDSA_REJ_UNIFORM_ETA2_MEMSAFE = prove `e:(uarch_event)list`; `stackpointer:int64`] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN - (* === Split: pc+4 to pc+0xfc (computation) and pc+0xfc to pc+364 (writeback) === + (* === Split: pc+4 to pc+0xfc (computation) and pc+0xfc to pc+444 (writeback) === The intermediate state at pc+0xfc tracks the partial niblist (same as CORRECT) plus an event accumulator with memaccess_inbounds. *) ENSURES_SEQUENCE_TAC `pc + 0xfc` @@ -2412,7 +2458,7 @@ let MLDSA_REJ_UNIFORM_ETA2_MEMSAFE = prove read PC s = word(pc + 0xfc) /\ read X0 s = res /\ read X4 s = word 256 /\ read X8 s = stackpointer /\ - ALL (nonoverlapping (res,1024)) [(word pc,372); (stackpointer,576)] /\ + ALL (nonoverlapping (res,1024)) [(word pc,452); (stackpointer,576)] /\ (?n. let niblist = REJ_NIBBLES_ETA2(SUB_LIST(0,8*n) inlist) in let niblen = LENGTH niblist in niblen < 272 /\ @@ -2528,7 +2574,7 @@ let MLDSA_REJ_UNIFORM_ETA2_MEMSAFE = prove read Q16 s = word(num_of_wordlist lis0):int128 /\ read Q17 s = word(num_of_wordlist lis1):int128) /\ curlen < 256 /\ - nonoverlapping (stackpointer,576) (word pc,372) /\ + nonoverlapping (stackpointer,576) (word pc,452) /\ (exists e_acc. read events s = APPEND e_acc e /\ memaccess_inbounds e_acc @@ -3055,7 +3101,7 @@ let MLDSA_REJ_UNIFORM_ETA2_MEMSAFE = prove read X9 s = word niblen /\ read (memory :> bytes (stackpointer,2 * niblen)) s = num_of_wordlist (REJ_NIBBLES_ETA2(SUB_LIST(0,8*N) inlist):int16 list) /\ - ALL (nonoverlapping (res,1024)) [(word pc,372); (stackpointer,576)] /\ + ALL (nonoverlapping (res,1024)) [(word pc,452); (stackpointer,576)] /\ (?e_acc. read events s = APPEND e_acc e /\ memaccess_inbounds e_acc [buf,buflen; table,4096; stackpointer,576] @@ -3129,8 +3175,8 @@ let MLDSA_REJ_UNIFORM_ETA2_MEMSAFE = prove DISJ1_TAC THEN ASM_REWRITE_TAC[]]; DISCHARGE_MEMSAFE_ASM_TAC]]]; - (* === Writeback phase (pc+0xfc to pc+364): unrolled, fixed sequence === - Symbolic-execute all 313 instructions in one ARM_STEPS_TAC call. + (* === Writeback phase (pc+0xfc to pc+444): unrolled, fixed sequence === + Symbolic-execute all 333 instructions in one ARM_STEPS_TAC call. Unlike the CORRECT writeback we skip BIGNUM_LDIGITIZE_TAC and MEMORY_128_FROM_64_TAC: those introduce ~100 stack bytes64/bytes128 reads needed to derive nibble values, but irrelevant to memory safety @@ -3148,7 +3194,7 @@ let MLDSA_REJ_UNIFORM_ETA2_MEMSAFE = prove SUBGOAL_THEN `val(word niblen:int64) = niblen` ASSUME_TAC THENL [MATCH_MP_TAC VAL_WORD_EQ THEN REWRITE_TAC[DIMINDEX_64] THEN UNDISCH_TAC `niblen < 272` THEN ARITH_TAC; ALL_TAC] THEN - ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (1--313) THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (1--333) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN DISCHARGE_MEMSAFE_TAC]);; @@ -3786,7 +3832,7 @@ let MLDSA_ETA2_LOOP8_COMPUTE = prove 8 * (i + 1) <= val buflen /\ NUM_ACCEPTED(SUB_LIST(0,16 * i) mask) < 256 /\ ALL (nonoverlapping (word_sub stackpointer (word 576),576)) - [(word pc,372); (buf,val buflen); (table,4096)] + [(word pc,452); (buf,val buflen); (table,4096)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) mldsa_rej_uniform_eta2_mc /\ read PC s = word (pc + 0x70) /\ @@ -3947,7 +3993,7 @@ let MLDSA_ETA2_LOOP8_COMPUTE = prove FIRST_X_ASSUM(fun th -> if is_eq(concl th) && lhs(concl th) = `read X7 s29:int64` then ASSUME_TAC(GEN_REWRITE_RULE RAND_CONV [WORD_ADD_SHL1] th) else failwith "no") THEN SUBGOAL_THEN - `nonoverlapping (word_add sp0 (word(2*(curlen + val(len0:int64)))):int64,16) (word pc:int64,372)` + `nonoverlapping (word_add sp0 (word(2*(curlen + val(len0:int64)))):int64,16) (word pc:int64,452)` ASSUME_TAC THENL [NONOVERLAPPING_TAC; ALL_TAC] THEN ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC [30] THEN ARM_VERBOSE_STEP_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC "s31" THEN @@ -4099,7 +4145,7 @@ let MLDSA_ETA2_LOOP8_BODY_ADAPTED = [`mask = REJ_MASK_ETA2 inlist`; `LENGTH (inlist:byte list) = val (buflen:int64)`; `ALL (nonoverlapping (word_sub stackpointer (word 576),576)) - [(word pc,372); (buf:int64,val (buflen:int64)); (table:int64,4096)]`] in + [(word pc,452); (buf:int64,val (buflen:int64)); (table:int64,4096)]`] in prove(mk_imp(ambient, conj2), REPEAT STRIP_TAC THEN ASM_CASES_TAC mi THENL @@ -4357,5 +4403,5 @@ let MLDSA_REJ_UNIFORM_ETA2_SUBROUTINE_SAFE = time prove ARITH_RULE `16*(i+1)=16*i+16`] THEN CONV_TAC WORD_RULE; ALL_TAC] THEN DISCHARGE_SAFETY_PROPERTY_TAC; ARM_SIM_TAC ~preprocess_tac:(TRY STRIP_EXISTS_ASSUM_TAC) - ~canonicalize_pc_diff:false MLDSA_REJ_UNIFORM_ETA2_EXEC (1--3) THEN + ~canonicalize_pc_diff:false MLDSA_REJ_UNIFORM_ETA2_EXEC (1--23) THEN DISCHARGE_SAFETY_PROPERTY_TAC]]]);; diff --git a/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta4_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta4_aarch64_asm.ml index 6e08922300..9be7dc18dc 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta4_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta4_aarch64_asm.ml @@ -14,6 +14,7 @@ needs "s2n_bignum/arm/proofs/base.ml";; needs "mldsa_native/aarch64/proofs/aarch64_utils.ml";; needs "mldsa_native/aarch64/proofs/mldsa_rej_uniform_eta_table.ml";; +needs "mldsa_native/common/stack_zero.ml";; (**** print_literal_from_elf "aarch64/mldsa/mldsa_rej_uniform_eta4_aarch64_asm.o";; ****) @@ -105,6 +106,26 @@ let mldsa_rej_uniform_eta4_mc = define_assert_from_elf 0x9100416b; (* arm_ADD X11 X11 (rvalue (word 16)) *) 0xf104017f; (* arm_CMP X11 (rvalue (word 256)) *) 0x54fffe4b; (* arm_BLT (word 2097096) *) + 0x6e301e10; (* arm_EOR_VEC Q16 Q16 Q16 128 *) + 0xaa0803e7; (* arm_MOV X7 X8 *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) + 0xac8140f0; (* arm_STP Q16 Q16 X7 (Postimmediate_Offset (iword (&32))) *) 0xaa0903e0; (* arm_MOV X0 X9 *) 0x910903ff; (* arm_ADD SP SP (rvalue (word 576)) *) 0xd65f03c0 (* arm_RET X30 *) @@ -642,6 +663,15 @@ let CASE_B_TRUNCATE_L = prove (* ------------------------------------------------------------------------- *) +let READ_BYTES_PREFIX_MOD = prove + (`!(a:int64) k n (s:armstate). + k <= n + ==> read (memory :> bytes(a,k)) s = + read (memory :> bytes(a,n)) s MOD 2 EXP (8 * k)`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[READ_COMPONENT_COMPOSE; READ_BYTES_MOD] THEN + ASM_SIMP_TAC[ARITH_RULE `k <= n ==> MIN n k = k`]);; + let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove (`!res buf buflen table (inlist:byte list) pc stackpointer. 8 divides val buflen /\ @@ -663,6 +693,7 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove read(memory :> bytes(buf,val buflen)) s = num_of_wordlist inlist) (\s. read PC s = word(pc + MLDSA_REJ_UNIFORM_ETA4_CORE_END) /\ + read (memory :> bytes(stackpointer,576)) s = 0 /\ let outlist = SUB_LIST(0,256) (REJ_SAMPLE_ETA4_BYTES inlist) in let outlen = LENGTH outlist in C_RETURN s = word outlen /\ @@ -687,7 +718,7 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove read X0 s = res /\ read X4 s = word 256 /\ read X8 s = stackpointer /\ read Q7 s = word 20769504351625144638033088116686852 /\ - ALL (nonoverlapping (res,1024)) [(word pc,344); (stackpointer,576)] /\ + ALL (nonoverlapping (res,1024)) [(word pc,424); (stackpointer,576)] /\ ?n. let niblist = REJ_NIBBLES_ETA4(SUB_LIST(0,8*n) inlist) in let niblen = LENGTH niblist in niblen < 272 /\ @@ -698,7 +729,17 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove CONJ_TAC THENL [ALL_TAC; - ENSURES_INIT_TAC "s0" THEN + ENSURES_SEQUENCE_TAC `pc + 332` + `\s. aligned_bytes_loaded s (word pc) mldsa_rej_uniform_eta4_mc /\ + read PC s = word(pc + 332) /\ + read X8 s = stackpointer /\ + let outlist = SUB_LIST(0,256) (REJ_SAMPLE_ETA4_BYTES inlist) in + let outlen = LENGTH outlist in + read X9 s = word outlen /\ + read(memory :> bytes(res,4 * outlen)) s = + num_of_wordlist outlist` THEN + CONJ_TAC THENL + [ENSURES_INIT_TAC "s0" THEN FIRST_X_ASSUM(X_CHOOSE_THEN `nn:num` MP_TAC) THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN ABBREV_TAC `niblist = REJ_NIBBLES_ETA4 @@ -713,7 +754,7 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove `read (memory :> bytes(stackpointer,8 * 64)) s0` THEN MEMORY_128_FROM_64_TAC "stackpointer" 0 32 THEN ASM_REWRITE_TAC[WORD_ADD_0] THEN STRIP_TAC THEN - ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA4_EXEC (1--245) THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA4_EXEC (1--244) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `LENGTH(SUB_LIST(0,256)(REJ_SAMPLE_ETA4_BYTES inlist):int32 list) = @@ -810,7 +851,7 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove UNDISCH_TAC `LENGTH(niblist:int16 list) = niblen` THEN DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN - MP_TAC(GEN `k:num` (ISPECL [`s245:armstate`; `stackpointer:int64`; + MP_TAC(GEN `k:num` (ISPECL [`s244:armstate`; `stackpointer:int64`; `niblist:int16 list`; `k:num`] BK_FROM_STACK_GE256)) THEN ASM_REWRITE_TAC[] THEN @@ -903,7 +944,7 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUB_LIST_REFL THEN REWRITE_TAC[LENGTH_MAP] THEN ASM_ARITH_TAC; ALL_TAC] THEN - MP_TAC(ISPECL [`stackpointer:int64`; `256`; `s245:armstate`] + MP_TAC(ISPECL [`stackpointer:int64`; `256`; `s244:armstate`] BYTES_EXISTS_WORDLIST) THEN REWRITE_TAC[ARITH_RULE `2 * 256 = 512`] THEN DISCH_THEN(X_CHOOSE_THEN `L:int16 list` STRIP_ASSUME_TAC) THEN @@ -911,7 +952,7 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove ASSUME_TAC THENL [MATCH_MP_TAC PREFIX_FROM_STACK THEN MAP_EVERY EXISTS_TAC - [`stackpointer:int64`; `s245:armstate`] THEN + [`stackpointer:int64`; `s244:armstate`] THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC CASE_B_TRUNCATE_L THEN @@ -920,7 +961,7 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `256 <= LENGTH (L:int16 list)` ASSUME_TAC THENL [ASM_REWRITE_TAC[] THEN ARITH_TAC; ALL_TAC] THEN - MP_TAC(GEN `k:num` (ISPECL [`s245:armstate`; `stackpointer:int64`; + MP_TAC(GEN `k:num` (ISPECL [`s244:armstate`; `stackpointer:int64`; `L:int16 list`; `k:num`] BK_FROM_STACK_GE256)) THEN ASM_REWRITE_TAC[ARITH_RULE `2 * 256 = 512`] THEN @@ -1009,7 +1050,7 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove UNDISCH_TAC `LENGTH(niblist:int16 list) = niblen` THEN DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN - MP_TAC(GEN `k:num` (ISPECL [`s245:armstate`; `stackpointer:int64`; + MP_TAC(GEN `k:num` (ISPECL [`s244:armstate`; `stackpointer:int64`; `niblist:int16 list`; `k:num`] BK_FROM_STACK_GE256)) THEN ASM_REWRITE_TAC[] THEN @@ -1074,7 +1115,31 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove [MATCH_MP_TAC STACK_CONTENT_LARGE THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN MATCH_MP_TAC PAIR_MAP_IDX_128 THEN - ASM_REWRITE_TAC[]]]] THEN + ASM_REWRITE_TAC[]]]; + + ENSURES_INIT_TAC "s0" THEN + FIRST_X_ASSUM(MP_TAC o check (is_let o concl)) THEN + CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN + ABBREV_TAC `outlist = SUB_LIST(0,256) (REJ_SAMPLE_ETA4_BYTES inlist):int32 list` THEN + ABBREV_TAC `outlen = LENGTH(outlist:int32 list)` THEN + STRIP_TAC THEN + SUBGOAL_THEN `4 * outlen <= 1024` ASSUME_TAC THENL + [EXPAND_TAC "outlen" THEN EXPAND_TAC "outlist" THEN + REWRITE_TAC[LENGTH_SUB_LIST] THEN ARITH_TAC; + ALL_TAC] THEN + UNDISCH_TAC `read (memory :> bytes(res,4 * outlen)) s0 = + num_of_wordlist(outlist:int32 list)` THEN + MP_TAC(SPECL [`res:int64`; `4 * outlen`; `1024`; `s0:armstate`] + READ_BYTES_PREFIX_MOD) THEN + ANTS_TAC THENL [ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC] THEN + DISCH_TAC THEN + ABBREV_TAC `r = read (memory :> bytes(res,1024)) s0` THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA4_EXEC (1--21) THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + CONJ_TAC THENL [STACK_ZERO_TAC; ALL_TAC] THEN + MP_TAC(SPECL [`res:int64`; `4 * outlen`; `1024`; `s21:armstate`] + READ_BYTES_PREFIX_MOD) THEN + ASM_REWRITE_TAC[]]] THEN SUBGOAL_THEN `?N. buflen < 8 * (N + 1) \/ @@ -1167,7 +1232,7 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove read Q16 s = word(num_of_wordlist lis0):int128 /\ read Q17 s = word(num_of_wordlist lis1):int128) /\ curlen < 256 /\ - nonoverlapping (stackpointer,576) (word pc,344)` THEN + nonoverlapping (stackpointer,576) (word pc,424)` THEN CONJ_TAC THENL [(* First half: SIMD compute chain — 29 steps *) GHOST_INTRO_TAC `nibbles1:int128` `read Q17` THEN @@ -1498,7 +1563,7 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove ASM_REWRITE_TAC[] THEN DISCH_TAC THEN SUBGOAL_THEN `nonoverlapping (word_add stackpointer (word(2 * (curlen + len0))):int64, - 16) (word pc:int64, 344)` + 16) (word pc:int64, 424)` ASSUME_TAC THENL [NONOVERLAPPING_TAC; ALL_TAC] THEN SUBGOAL_THEN `val(word len0:int64) = len0` ASSUME_TAC THENL [MATCH_MP_TAC VAL_WORD_EQ THEN REWRITE_TAC[DIMINDEX_64] THEN @@ -1639,7 +1704,7 @@ let MLDSA_REJ_UNIFORM_ETA4_CORRECT = prove read X9 s = word niblen /\ read (memory :> bytes (stackpointer,2 * niblen)) s = num_of_wordlist (REJ_NIBBLES_ETA4(SUB_LIST(0,8*N) inlist):int16 list) /\ - ALL (nonoverlapping (res,1024)) [(word pc,344); (stackpointer,576)]` THEN + ALL (nonoverlapping (res,1024)) [(word pc,424); (stackpointer,576)]` THEN CONJ_TAC THENL [(* pc+248 -> pc+108: CMP X2,8; BCS back *) ENSURES_INIT_TAC "s0" THEN @@ -1786,6 +1851,7 @@ let MLDSA_REJ_UNIFORM_ETA4_SUBROUTINE_CORRECT = prove read(memory :> bytes(buf,val buflen)) s = num_of_wordlist inlist) (\s. read PC s = returnaddress /\ + read (memory :> bytes(word_sub stackpointer (word 576),576)) s = 0 /\ let outlist = SUB_LIST(0,256) (REJ_SAMPLE_ETA4 inlist) in let outlen = LENGTH outlist in outlen <= 256 /\ @@ -1836,6 +1902,7 @@ let MLDSA_REJ_UNIFORM_ETA4_SUBROUTINE_CORRECT = prove read(memory :> bytes(buf,val buflen)) s = num_of_wordlist inlist) (\s. read PC s = returnaddress /\ + read (memory :> bytes(word_sub stackpointer (word 576),576)) s = 0 /\ let outlist = SUB_LIST(0,256) (REJ_SAMPLE_ETA4_BYTES inlist) in let outlen = LENGTH outlist in @@ -2011,7 +2078,7 @@ let MLDSA_REJ_UNIFORM_ETA4_MEMSAFE = prove read X0 s = res /\ read X4 s = word 256 /\ read X8 s = stackpointer /\ read Q7 s = word 20769504351625144638033088116686852 /\ - ALL (nonoverlapping (res,1024)) [(word pc,344); (stackpointer,576)] /\ + ALL (nonoverlapping (res,1024)) [(word pc,424); (stackpointer,576)] /\ ?n. let niblist = REJ_NIBBLES_ETA4(SUB_LIST(0,8*n) inlist) in let niblen = LENGTH niblist in niblen < 272 /\ @@ -2027,7 +2094,7 @@ let MLDSA_REJ_UNIFORM_ETA4_MEMSAFE = prove CONJ_TAC THENL [ALL_TAC; - (* ---- Writeback branch (pc+256 -> pc+336) ---- + (* ---- Writeback branch (pc+256 -> pc+416) ---- Skip BIGNUM_LDIGITIZE_TAC and MEMORY_128_FROM_64_TAC: they introduce ~100 stack bytes64/bytes128 reads needed for CORRECT to derive nibble values, but irrelevant to memory safety (only events + PC + memaccess @@ -2043,7 +2110,7 @@ let MLDSA_REJ_UNIFORM_ETA4_MEMSAFE = prove SUBGOAL_THEN `val(word niblen:int64) = niblen` ASSUME_TAC THENL [MATCH_MP_TAC VAL_WORD_EQ THEN REWRITE_TAC[DIMINDEX_64] THEN UNDISCH_TAC `niblen < 272` THEN ARITH_TAC; ALL_TAC] THEN - ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA4_EXEC (1--245) THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA4_EXEC (1--265) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN TRY DISCHARGE_MEMSAFE_TAC THEN ALL_TAC] THEN @@ -2147,7 +2214,7 @@ let MLDSA_REJ_UNIFORM_ETA4_MEMSAFE = prove read Q16 s = word(num_of_wordlist lis0):int128 /\ read Q17 s = word(num_of_wordlist lis1):int128) /\ curlen < 256 /\ - nonoverlapping (stackpointer,576) (word pc,344) /\ + nonoverlapping (stackpointer,576) (word pc,424) /\ (exists e_acc. read events s = APPEND e_acc e /\ memaccess_inbounds e_acc @@ -2528,7 +2595,7 @@ let MLDSA_REJ_UNIFORM_ETA4_MEMSAFE = prove ASM_REWRITE_TAC[] THEN DISCH_TAC THEN SUBGOAL_THEN `nonoverlapping (word_add stackpointer (word(2 * (curlen + len0))):int64, - 16) (word pc:int64, 344)` + 16) (word pc:int64, 424)` ASSUME_TAC THENL [NONOVERLAPPING_TAC; ALL_TAC] THEN SUBGOAL_THEN `val(word len0:int64) = len0` ASSUME_TAC THENL [MATCH_MP_TAC VAL_WORD_EQ THEN REWRITE_TAC[DIMINDEX_64] THEN @@ -2674,7 +2741,7 @@ let MLDSA_REJ_UNIFORM_ETA4_MEMSAFE = prove read X9 s = word niblen /\ read (memory :> bytes (stackpointer,2 * niblen)) s = num_of_wordlist (REJ_NIBBLES_ETA4(SUB_LIST(0,8*N) inlist):int16 list) /\ - ALL (nonoverlapping (res,1024)) [(word pc,344); (stackpointer,576)] /\ + ALL (nonoverlapping (res,1024)) [(word pc,424); (stackpointer,576)] /\ (exists e_acc. read events s = APPEND e_acc e /\ memaccess_inbounds e_acc @@ -3095,7 +3162,7 @@ let MLDSA_ETA4_LOOP8_TRIP_MINIMAL = prove (* REJECT-MASK, demonstrated. (Accepted VALUES never enter the trace.) *) (* *) (* add x7; add x12; add x9; cmp x2,#8]. *) -(* BEFORE `add x7`. (b) stores need `nonoverlapping (word pc,344) *) +(* BEFORE `add x7`. (b) stores need `nonoverlapping (word pc,424) *) (* (stackpointer,576)` in context (from the theorem's ALL clause) AND the 2nd *) (* store additionally needs val len0<=8 (UADDLV_BOUND_LEMMA) + the MEMSAFE *) (* WORD_ADD_SHL1 rewrite (eta4.ml:2971) on the word_shl'd X7 offset, else *) @@ -3519,7 +3586,7 @@ let MLDSA_ETA4_LOOP8_COMPUTE = prove 8 * (i + 1) <= val buflen /\ NUM_ACCEPTED(SUB_LIST(0,16 * i) mask) < 256 /\ ALL (nonoverlapping (word_sub stackpointer (word 576),576)) - [(word pc,344); (buf,val buflen); (table,4096)] + [(word pc,424); (buf,val buflen); (table,4096)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) mldsa_rej_uniform_eta4_mc /\ read PC s = word (pc + 0x74) /\ @@ -3680,7 +3747,7 @@ let MLDSA_ETA4_LOOP8_COMPUTE = prove FIRST_X_ASSUM(fun th -> if is_eq(concl th) && lhs(concl th) = `read X7 s29:int64` then ASSUME_TAC(GEN_REWRITE_RULE RAND_CONV [WORD_ADD_SHL1] th) else failwith "no") THEN SUBGOAL_THEN - `nonoverlapping (word_add sp0 (word(2*(curlen + val(len0:int64)))):int64,16) (word pc:int64,344)` + `nonoverlapping (word_add sp0 (word(2*(curlen + val(len0:int64)))):int64,16) (word pc:int64,424)` ASSUME_TAC THENL [NONOVERLAPPING_TAC; ALL_TAC] THEN ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA4_EXEC [30] THEN ARM_VERBOSE_STEP_TAC MLDSA_REJ_UNIFORM_ETA4_EXEC "s31" THEN @@ -3860,7 +3927,7 @@ let MLDSA_ETA4_LOOP8_BODY_ADAPTED = [`mask = REJ_MASK_ETA4 inlist`; `LENGTH (inlist:byte list) = val (buflen:int64)`; `ALL (nonoverlapping (word_sub stackpointer (word 576),576)) - [(word pc,344); (buf:int64,val (buflen:int64)); (table:int64,4096)]`] in + [(word pc,424); (buf:int64,val (buflen:int64)); (table:int64,4096)]`] in prove(mk_imp(ambient, conj2), REPEAT STRIP_TAC THEN ASM_CASES_TAC mi THENL @@ -4121,5 +4188,5 @@ let MLDSA_REJ_UNIFORM_ETA4_SUBROUTINE_SAFE = time prove ARITH_RULE `16*(i+1)=16*i+16`] THEN CONV_TAC WORD_RULE; ALL_TAC] THEN DISCHARGE_SAFETY_PROPERTY_TAC; ARM_SIM_TAC ~preprocess_tac:(TRY STRIP_EXISTS_ASSUM_TAC) - ~canonicalize_pc_diff:false MLDSA_REJ_UNIFORM_ETA4_EXEC (1--3) THEN + ~canonicalize_pc_diff:false MLDSA_REJ_UNIFORM_ETA4_EXEC (1--23) THEN DISCHARGE_SAFETY_PROPERTY_TAC]]]);; diff --git a/proofs/hol_light/common/stack_zero.ml b/proofs/hol_light/common/stack_zero.ml new file mode 100644 index 0000000000..aaf39e6c3c --- /dev/null +++ b/proofs/hol_light/common/stack_zero.ml @@ -0,0 +1,26 @@ +(* + * Copyright (c) The mldsa-native project authors + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0 + *) + +(* ========================================================================= *) +(* Proving that a stack region has been zeroized. *) +(* ========================================================================= *) + +(* Proves `read (memory :> bytes(a,n)) s = 0` for n a multiple of 8. *) +let STACK_ZERO_TAC = + let split_assum n pat = + REPEAT(FIRST_X_ASSUM(STRIP_ASSUME_TAC o CONV_RULE(READ_MEMORY_SPLIT_CONV n) o + check (can (term_match [] pat) o concl))) in + W(fun (asl,w) -> + let n = dest_small_numeral(rand(rand(rand(rand(rator(lhand w)))))) in + let nth = SYM(NUM_REDUCE_CONV(mk_binop `( * ):num->num->num` + (mk_small_numeral 8) (mk_small_numeral(n / 8)))) in + CONV_TAC(LAND_CONV(RATOR_CONV(RAND_CONV(RAND_CONV(RAND_CONV(RAND_CONV + (fun t -> if t = lhs(concl nth) then nth else failwith "")))))))) THEN + CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN + split_assum 2 `read (memory :> bytes256 a) s = x` THEN + split_assum 1 `read (memory :> bytes128 a) s = x` THEN + CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN + ASM_REWRITE_TAC[WORD_XOR_REFL] THEN + CONV_TAC(WORD_REDUCE_CONV THENC NUM_REDUCE_CONV);; diff --git a/proofs/hol_light/x86_64/mldsa/keccak_f1600_x4_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/keccak_f1600_x4_avx2_asm.S index 22b7968120..c12688ea52 100644 --- a/proofs/hol_light/x86_64/mldsa/keccak_f1600_x4_avx2_asm.S +++ b/proofs/hol_light/x86_64/mldsa/keccak_f1600_x4_avx2_asm.S @@ -477,6 +477,31 @@ LLmld_keccak_f1600_x4_avx2_asm: vmovhpd %xmm3, 0x188(%rdi) vmovq %xmm15, 0x250(%rdi) vmovhpd %xmm15, 0x318(%rdi) + vpxor %ymm0, %ymm0, %ymm0 + vmovdqu %ymm0, (%rsp) + vmovdqu %ymm0, 0x20(%rsp) + vmovdqu %ymm0, 0x40(%rsp) + vmovdqu %ymm0, 0x60(%rsp) + vmovdqu %ymm0, 0x80(%rsp) + vmovdqu %ymm0, 0xa0(%rsp) + vmovdqu %ymm0, 0xc0(%rsp) + vmovdqu %ymm0, 0xe0(%rsp) + vmovdqu %ymm0, 0x100(%rsp) + vmovdqu %ymm0, 0x120(%rsp) + vmovdqu %ymm0, 0x140(%rsp) + vmovdqu %ymm0, 0x160(%rsp) + vmovdqu %ymm0, 0x180(%rsp) + vmovdqu %ymm0, 0x1a0(%rsp) + vmovdqu %ymm0, 0x1c0(%rsp) + vmovdqu %ymm0, 0x1e0(%rsp) + vmovdqu %ymm0, 0x200(%rsp) + vmovdqu %ymm0, 0x220(%rsp) + vmovdqu %ymm0, 0x240(%rsp) + vmovdqu %ymm0, 0x260(%rsp) + vmovdqu %ymm0, 0x280(%rsp) + vmovdqu %ymm0, 0x2a0(%rsp) + vmovdqu %ymm0, 0x2c0(%rsp) + vmovdqu %ymm0, 0x2e0(%rsp) vzeroupper movq %r11, %rsp .cfi_def_cfa_register %rsp diff --git a/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml index a3b3535d93..eb43f4a582 100644 --- a/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml @@ -8,6 +8,7 @@ needs "mldsa_native/x86_64/proofs/mldsa_utils.ml";; needs "mldsa_native/x86_64/proofs/keccak_utils.ml";; + needs "mldsa_native/common/stack_zero.ml";; (**** print_literal_from_elf "x86/sha3/keccak_f1600_x4_avx2.o";; ****) @@ -746,6 +747,55 @@ let keccak_f1600_x4_avx2_mc = define_assert_from_elf (* VMOVQ (Memop Quadword (%% (rdi,592))) (%_% xmm15) *) 0xc5; 0x79; 0x17; 0xbf; 0x18; 0x03; 0x00; 0x00; (* VMOVHPD (Memop Quadword (%% (rdi,792))) (%_% xmm15) *) + 0xc5; 0xfd; 0xef; 0xc0; (* VPXOR (%_% ymm0) (%_% ymm0) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x04; 0x24; + (* VMOVDQU (Memop Word256 (%% (rsp,0))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x44; 0x24; 0x20; + (* VMOVDQU (Memop Word256 (%% (rsp,32))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x44; 0x24; 0x40; + (* VMOVDQU (Memop Word256 (%% (rsp,64))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x44; 0x24; 0x60; + (* VMOVDQU (Memop Word256 (%% (rsp,96))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0x80; 0x00; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,128))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0xa0; 0x00; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,160))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0xc0; 0x00; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,192))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0xe0; 0x00; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,224))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0x00; 0x01; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,256))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0x20; 0x01; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,288))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0x40; 0x01; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,320))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0x60; 0x01; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,352))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0x80; 0x01; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,384))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0xa0; 0x01; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,416))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0xc0; 0x01; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,448))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0xe0; 0x01; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,480))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0x00; 0x02; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,512))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0x20; 0x02; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,544))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0x40; 0x02; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,576))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0x60; 0x02; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,608))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0x80; 0x02; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,640))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0xa0; 0x02; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,672))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0xc0; 0x02; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,704))) (%_% ymm0) *) + 0xc5; 0xfe; 0x7f; 0x84; 0x24; 0xe0; 0x02; 0x00; 0x00; + (* VMOVDQU (Memop Word256 (%% (rsp,736))) (%_% ymm0) *) 0xc5; 0xf8; 0x77; (* VZEROUPPER *) 0x4c; 0x89; 0xdc; (* MOV (% rsp) (% r11) *) 0xc3 (* RET *) @@ -802,6 +852,7 @@ let KECCAK_F1600_X4_CORRECT = prove wordlist_from_memory(word_add bitstate_in (word 400),25) s = A3 /\ wordlist_from_memory(word_add bitstate_in (word 600),25) s = A4) (\s. read RIP s = word(pc + KECCAK_F1600_X4_CORE_END) /\ + read (memory :> bytes(stackpointer,0x300)) s = 0 /\ wordlist_from_memory(bitstate_in,25) s = keccak 24 A1 /\ wordlist_from_memory(word_add bitstate_in (word 200),25) s = keccak 24 A2 /\ wordlist_from_memory(word_add bitstate_in (word 400),25) s = keccak 24 A3 /\ @@ -1024,6 +1075,7 @@ let KECCAK_F1600_X4_CORRECT = prove check (can (term_match [] `read qqq s:int256 = xxx`) o concl))) THEN CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + CONJ_TAC THENL [STACK_ZERO_TAC; ALL_TAC] THEN REPEAT CONJ_TAC THEN BITBLAST_TAC]);; @@ -1055,6 +1107,8 @@ let KECCAK_F1600_X4_NOIBT_SUBROUTINE_CORRECT = prove wordlist_from_memory(word_add bitstate_in (word 600), 25) s = A4) (\s. read RIP s = returnaddress /\ read RSP s = word_add stackpointer (word 8) /\ + read (memory :> bytes(word_sub (word_and stackpointer (word 0xffffffffffffffe0)) + (word 0x300), 0x300)) s = 0 /\ wordlist_from_memory(bitstate_in, 25) s = keccak 24 A1 /\ wordlist_from_memory(word_add bitstate_in (word 200), 25) s = keccak 24 A2 /\ wordlist_from_memory(word_add bitstate_in (word 400), 25) s = keccak 24 A3 /\ @@ -1149,6 +1203,8 @@ let KECCAK_F1600_X4_SUBROUTINE_CORRECT = prove wordlist_from_memory(word_add bitstate_in (word 600), 25) s = A4) (\s. read RIP s = returnaddress /\ read RSP s = word_add stackpointer (word 8) /\ + read (memory :> bytes(word_sub (word_and stackpointer (word 0xffffffffffffffe0)) + (word 0x300), 0x300)) s = 0 /\ wordlist_from_memory(bitstate_in, 25) s = keccak 24 A1 /\ wordlist_from_memory(word_add bitstate_in (word 200), 25) s = keccak 24 A2 /\ wordlist_from_memory(word_add bitstate_in (word 400), 25) s = keccak 24 A3 /\