From eaa80926eac6c3ea7fb6d071b281d063d787e63c Mon Sep 17 00:00:00 2001 From: Joe Doyle Date: Mon, 29 Jun 2026 16:44:14 -0400 Subject: [PATCH 1/2] Clear ML-KEM Keccak stack scratch Wipe the AVX2, AArch64 scalar-hybrid, and Armv8.1-M MVE x4 Keccak scratch frames before returning, and refresh the covered HOL Light proof copies for the changed instruction streams. This keeps state-derived stack scratch from surviving past the permutation return path. Verification: - nix develop .#hol_light-cross-aarch64 -c make -B -C proofs/hol_light/aarch64 mlkem/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.correct - nix develop .#hol_light-cross-aarch64 -c make -B -C proofs/hol_light/aarch64 mlkem/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.correct - nix develop .#hol_light-cross-x86_64 -c make -B -C proofs/hol_light/x86_64 mlkem/keccak_f1600_x4_avx2_asm.correct Co-authored-by: Codex Signed-off-by: Joe Doyle --- ...k_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S | 10 +++ ...00_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S | 10 +++ dev/fips202/armv81m/src/keccak_f1600_x4_mve.S | 8 ++ .../x86_64/src/keccak_f1600_x4_avx2_asm.S | 8 ++ ...k_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S | 15 ++++ ...00_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S | 15 ++++ .../native/armv81m/src/keccak_f1600_x4_mve.S | 8 +- .../x86_64/src/keccak_f1600_x4_avx2_asm.S | 6 ++ ...k_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S | 15 ++++ ...00_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S | 15 ++++ ..._f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml | 19 ++++- ...0_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml | 19 ++++- .../x86_64/mlkem/keccak_f1600_x4_avx2_asm.S | 6 ++ .../x86_64/proofs/keccak_f1600_x4_avx2_asm.ml | 76 ++++++++++++++----- 14 files changed, 205 insertions(+), 25 deletions(-) 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 c10cc67243..237de14896 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 @@ -335,6 +335,15 @@ add sp, sp, #(STACK_SIZE) .endm +.macro clear_stack + eor v0.16b, v0.16b, v0.16b + .set .Lclear_stack_offset, 0 + .rept STACK_SIZE / 16 + str q0, [sp, #.Lclear_stack_offset] + .set .Lclear_stack_offset, .Lclear_stack_offset + 16 + .endr +.endm + .macro eor5 dst, src0, src1, src2, src3, src4 eor \dst, \src0, \src1 eor \dst, \dst, \src2 @@ -2453,6 +2462,7 @@ keccak_f1600_x4_v8a_scalar_hybrid_done: restore_vregs restore_gprs + clear_stack free_stack ret 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 0b464b3a14..322adce30c 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 @@ -354,6 +354,15 @@ add sp, sp, #(STACK_SIZE) .endm +.macro clear_stack + eor v0.16b, v0.16b, v0.16b + .set .Lclear_stack_offset, 0 + .rept STACK_SIZE / 16 + str q0, [sp, #.Lclear_stack_offset] + .set .Lclear_stack_offset, .Lclear_stack_offset + 16 + .endr +.endm + .macro eor5 dst, src0, src1, src2, src3, src4 eor \dst, \src0, \src1 eor \dst, \dst, \src2 @@ -2284,6 +2293,7 @@ keccak_f1600_x4_v8a_v84a_scalar_hybrid_done: restore_vregs restore_gprs + clear_stack free_stack ret diff --git a/dev/fips202/armv81m/src/keccak_f1600_x4_mve.S b/dev/fips202/armv81m/src/keccak_f1600_x4_mve.S index 3659c6333b..283f8ae921 100644 --- a/dev/fips202/armv81m/src/keccak_f1600_x4_mve.S +++ b/dev/fips202/armv81m/src/keccak_f1600_x4_mve.S @@ -1626,6 +1626,14 @@ MLK_ASM_FN_SYMBOL(keccak_f1600_x4_mve_asm) le lr, keccak_f1600_x4_mve_asm_roundstart keccak_f1600_x4_mve_asm_roundend: + // Clear the 0x80-byte scratch frame before releasing it. + movs r0, #0 + vdup.32 q0, r0 + .set .Lclear_stack_offset, 0 + .rept 8 + vstrw.32 q0, [r13, #.Lclear_stack_offset] + .set .Lclear_stack_offset, .Lclear_stack_offset + 16 + .endr add sp, #8*16 vpop {d8-d15} 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 5c3340fa39..dc67bd1e08 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 @@ -651,6 +651,14 @@ MLK_ASM_FN_SYMBOL(keccak_f1600_x4_avx2_asm) vmovhpd %xmm3, 0x188(%rdi) vmovq %xmm15, 0x250(%rdi) vmovhpd %xmm15, 0x318(%rdi) + + // Clear the scratch frame before releasing it. + vpxor %ymm0, %ymm0, %ymm0 + .set .Lclear_stack_offset, 0 + .rept 24 + vmovdqu %ymm0, .Lclear_stack_offset(%rsp) + .set .Lclear_stack_offset, .Lclear_stack_offset + 32 + .endr movq %r11, %rsp ret diff --git a/mlkem/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S b/mlkem/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S index 3d543b4ee1..0c11d512e5 100644 --- a/mlkem/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S +++ b/mlkem/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S @@ -1063,6 +1063,21 @@ Lkeccak_f1600_x4_v8a_scalar_hybrid_done: ldp x29, x30, [sp, #0x80] .cfi_restore x29 .cfi_restore x30 + eor v0.16b, v0.16b, v0.16b + str q0, [sp] + str q0, [sp, #0x10] + str q0, [sp, #0x20] + str q0, [sp, #0x30] + str q0, [sp, #0x40] + str q0, [sp, #0x50] + str q0, [sp, #0x60] + str q0, [sp, #0x70] + str q0, [sp, #0x80] + str q0, [sp, #0x90] + str q0, [sp, #0xa0] + str q0, [sp, #0xb0] + str q0, [sp, #0xc0] + str q0, [sp, #0xd0] add sp, sp, #0xe0 .cfi_adjust_cfa_offset -0xe0 ret diff --git a/mlkem/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S b/mlkem/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S index 82f8aa82ce..82827dd951 100644 --- a/mlkem/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S +++ b/mlkem/src/fips202/native/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S @@ -972,6 +972,21 @@ Lkeccak_f1600_x4_v8a_v84a_scalar_hybrid_done: ldp x29, x30, [sp, #0x80] .cfi_restore x29 .cfi_restore x30 + eor v0.16b, v0.16b, v0.16b + str q0, [sp] + str q0, [sp, #0x10] + str q0, [sp, #0x20] + str q0, [sp, #0x30] + str q0, [sp, #0x40] + str q0, [sp, #0x50] + str q0, [sp, #0x60] + str q0, [sp, #0x70] + str q0, [sp, #0x80] + str q0, [sp, #0x90] + str q0, [sp, #0xa0] + str q0, [sp, #0xb0] + str q0, [sp, #0xc0] + str q0, [sp, #0xd0] add sp, sp, #0xe0 .cfi_adjust_cfa_offset -0xe0 ret diff --git a/mlkem/src/fips202/native/armv81m/src/keccak_f1600_x4_mve.S b/mlkem/src/fips202/native/armv81m/src/keccak_f1600_x4_mve.S index ab4f7a18b2..0c95722dbd 100644 --- a/mlkem/src/fips202/native/armv81m/src/keccak_f1600_x4_mve.S +++ b/mlkem/src/fips202/native/armv81m/src/keccak_f1600_x4_mve.S @@ -681,6 +681,13 @@ Lkeccak_f1600_x4_mve_asm_roundend_pre: le lr, Lkeccak_f1600_x4_mve_asm_roundstart @ imm = #-0x8c0 Lkeccak_f1600_x4_mve_asm_roundend: + movs r0, #0x0 + vdup.32 q0, r0 + .set .Lkeccak_f1600_x4_mve_clear_stack_offset, 0 + .rept 8 + vstrw.32 q0, [sp, #.Lkeccak_f1600_x4_mve_clear_stack_offset] + .set .Lkeccak_f1600_x4_mve_clear_stack_offset, .Lkeccak_f1600_x4_mve_clear_stack_offset + 16 + .endr add sp, #0x80 .cfi_adjust_cfa_offset -0x80 vpop {d8, d9, d10, d11, d12, d13, d14, d15} @@ -705,7 +712,6 @@ Lkeccak_f1600_x4_mve_asm_roundend: .cfi_restore lr .cfi_adjust_cfa_offset -0x24 .cfi_endproc - nop MLK_ASM_FN_SIZE(keccak_f1600_x4_mve_asm) diff --git a/mlkem/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S b/mlkem/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S index 23d7eedd5d..1c284ed689 100644 --- a/mlkem/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S +++ b/mlkem/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S @@ -473,6 +473,12 @@ LLkeccak_f1600_x4_avx2: vmovhpd %xmm3, 0x188(%rdi) vmovq %xmm15, 0x250(%rdi) vmovhpd %xmm15, 0x318(%rdi) + vpxor %ymm0, %ymm0, %ymm0 + .set .Lkeccak_f1600_x4_avx2_clear_stack_offset, 0 + .rept 24 + vmovdqu %ymm0, .Lkeccak_f1600_x4_avx2_clear_stack_offset(%rsp) + .set .Lkeccak_f1600_x4_avx2_clear_stack_offset, .Lkeccak_f1600_x4_avx2_clear_stack_offset + 32 + .endr movq %r11, %rsp .cfi_def_cfa_register %rsp retq diff --git a/proofs/hol_light/aarch64/mlkem/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S b/proofs/hol_light/aarch64/mlkem/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S index 4421f186da..bfb393170c 100644 --- a/proofs/hol_light/aarch64/mlkem/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S +++ b/proofs/hol_light/aarch64/mlkem/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S @@ -1065,6 +1065,21 @@ Lkeccak_f1600_x4_v8a_scalar_hybrid_done: ldp x29, x30, [sp, #0x80] .cfi_restore x29 .cfi_restore x30 + eor v0.16b, v0.16b, v0.16b + str q0, [sp] + str q0, [sp, #0x10] + str q0, [sp, #0x20] + str q0, [sp, #0x30] + str q0, [sp, #0x40] + str q0, [sp, #0x50] + str q0, [sp, #0x60] + str q0, [sp, #0x70] + str q0, [sp, #0x80] + str q0, [sp, #0x90] + str q0, [sp, #0xa0] + str q0, [sp, #0xb0] + str q0, [sp, #0xc0] + str q0, [sp, #0xd0] add sp, sp, #0xe0 .cfi_adjust_cfa_offset -0xe0 ret diff --git a/proofs/hol_light/aarch64/mlkem/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S b/proofs/hol_light/aarch64/mlkem/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S index 93c93c32de..3dc1941a33 100644 --- a/proofs/hol_light/aarch64/mlkem/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S +++ b/proofs/hol_light/aarch64/mlkem/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S @@ -973,6 +973,21 @@ Lkeccak_f1600_x4_v8a_v84a_scalar_hybrid_done: ldp x29, x30, [sp, #0x80] .cfi_restore x29 .cfi_restore x30 + eor v0.16b, v0.16b, v0.16b + str q0, [sp] + str q0, [sp, #0x10] + str q0, [sp, #0x20] + str q0, [sp, #0x30] + str q0, [sp, #0x40] + str q0, [sp, #0x50] + str q0, [sp, #0x60] + str q0, [sp, #0x70] + str q0, [sp, #0x80] + str q0, [sp, #0x90] + str q0, [sp, #0xa0] + str q0, [sp, #0xb0] + str q0, [sp, #0xc0] + str q0, [sp, #0xd0] add sp, sp, #0xe0 .cfi_adjust_cfa_offset -0xe0 ret 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 e24b914cf7..a5dc7524f9 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 @@ -987,6 +987,21 @@ let keccak_f1600_x4_v8a_scalar_mc = define_assert_from_elf 0xa9466bf9; (* arm_LDP X25 X26 SP (Immediate_Offset (iword (&96))) *) 0xa94773fb; (* arm_LDP X27 X28 SP (Immediate_Offset (iword (&112))) *) 0xa9487bfd; (* arm_LDP X29 X30 SP (Immediate_Offset (iword (&128))) *) + 0x6e201c00; (* arm_EOR_VEC Q0 Q0 Q0 128 *) + 0x3d8003e0; (* arm_STR Q0 SP (Immediate_Offset (word 0)) *) + 0x3d8007e0; (* arm_STR Q0 SP (Immediate_Offset (word 16)) *) + 0x3d800be0; (* arm_STR Q0 SP (Immediate_Offset (word 32)) *) + 0x3d800fe0; (* arm_STR Q0 SP (Immediate_Offset (word 48)) *) + 0x3d8013e0; (* arm_STR Q0 SP (Immediate_Offset (word 64)) *) + 0x3d8017e0; (* arm_STR Q0 SP (Immediate_Offset (word 80)) *) + 0x3d801be0; (* arm_STR Q0 SP (Immediate_Offset (word 96)) *) + 0x3d801fe0; (* arm_STR Q0 SP (Immediate_Offset (word 112)) *) + 0x3d8023e0; (* arm_STR Q0 SP (Immediate_Offset (word 128)) *) + 0x3d8027e0; (* arm_STR Q0 SP (Immediate_Offset (word 144)) *) + 0x3d802be0; (* arm_STR Q0 SP (Immediate_Offset (word 160)) *) + 0x3d802fe0; (* arm_STR Q0 SP (Immediate_Offset (word 176)) *) + 0x3d8033e0; (* arm_STR Q0 SP (Immediate_Offset (word 192)) *) + 0x3d8037e0; (* arm_STR Q0 SP (Immediate_Offset (word 208)) *) 0x910383ff; (* arm_ADD SP SP (rvalue (word 224)) *) 0xd65f03c0 (* arm_RET X30 *) ];; @@ -1017,7 +1032,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH = new_definition `KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH = 44`;; let KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH = new_definition - `KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH = 48`;; + `KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH = 108`;; let KECCAK_F1600_X4_V8A_SCALAR_CORE_START = new_definition `KECCAK_F1600_X4_V8A_SCALAR_CORE_START = KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH`;; @@ -1483,7 +1498,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT = prove (WORDLIST_FROM_MEMORY_CONV THENC ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) in CONV_TAC TWEAK_CONV THEN - ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,11) KECCAK_F1600_X4_V8A_SCALAR_EXEC + ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,26) KECCAK_F1600_X4_V8A_SCALAR_EXEC (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_SCALAR_CORRECT)) `[D8; D9; D10; D11; D12; D13; D14; D15; X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30]` 224);; 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 fcbe468e03..ac030b1df8 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 @@ -893,6 +893,21 @@ let keccak_f1600_x4_v8a_v84a_scalar_mc = define_assert_from_elf 0xa9466bf9; (* arm_LDP X25 X26 SP (Immediate_Offset (iword (&96))) *) 0xa94773fb; (* arm_LDP X27 X28 SP (Immediate_Offset (iword (&112))) *) 0xa9487bfd; (* arm_LDP X29 X30 SP (Immediate_Offset (iword (&128))) *) + 0x6e201c00; (* arm_EOR_VEC Q0 Q0 Q0 128 *) + 0x3d8003e0; (* arm_STR Q0 SP (Immediate_Offset (word 0)) *) + 0x3d8007e0; (* arm_STR Q0 SP (Immediate_Offset (word 16)) *) + 0x3d800be0; (* arm_STR Q0 SP (Immediate_Offset (word 32)) *) + 0x3d800fe0; (* arm_STR Q0 SP (Immediate_Offset (word 48)) *) + 0x3d8013e0; (* arm_STR Q0 SP (Immediate_Offset (word 64)) *) + 0x3d8017e0; (* arm_STR Q0 SP (Immediate_Offset (word 80)) *) + 0x3d801be0; (* arm_STR Q0 SP (Immediate_Offset (word 96)) *) + 0x3d801fe0; (* arm_STR Q0 SP (Immediate_Offset (word 112)) *) + 0x3d8023e0; (* arm_STR Q0 SP (Immediate_Offset (word 128)) *) + 0x3d8027e0; (* arm_STR Q0 SP (Immediate_Offset (word 144)) *) + 0x3d802be0; (* arm_STR Q0 SP (Immediate_Offset (word 160)) *) + 0x3d802fe0; (* arm_STR Q0 SP (Immediate_Offset (word 176)) *) + 0x3d8033e0; (* arm_STR Q0 SP (Immediate_Offset (word 192)) *) + 0x3d8037e0; (* arm_STR Q0 SP (Immediate_Offset (word 208)) *) 0x910383ff; (* arm_ADD SP SP (rvalue (word 224)) *) 0xd65f03c0 (* arm_RET X30 *) ];; @@ -922,7 +937,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_PREAMBLE_LENGTH = new_definition `KECCAK_F1600_X4_V8A_V84A_SCALAR_PREAMBLE_LENGTH = 44`;; let KECCAK_F1600_X4_V8A_V84A_SCALAR_POSTAMBLE_LENGTH = new_definition - `KECCAK_F1600_X4_V8A_V84A_SCALAR_POSTAMBLE_LENGTH = 48`;; + `KECCAK_F1600_X4_V8A_V84A_SCALAR_POSTAMBLE_LENGTH = 108`;; let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_START = new_definition `KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_START = KECCAK_F1600_X4_V8A_V84A_SCALAR_PREAMBLE_LENGTH`;; @@ -1388,7 +1403,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_CORRECT = prove (WORDLIST_FROM_MEMORY_CONV THENC ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) in CONV_TAC TWEAK_CONV THEN - ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,11) KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC + ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,26) KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT)) `[D8; D9; D10; D11; D12; D13; D14; D15; X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30]` 224);; diff --git a/proofs/hol_light/x86_64/mlkem/keccak_f1600_x4_avx2_asm.S b/proofs/hol_light/x86_64/mlkem/keccak_f1600_x4_avx2_asm.S index 50348fa17d..630ef7d407 100644 --- a/proofs/hol_light/x86_64/mlkem/keccak_f1600_x4_avx2_asm.S +++ b/proofs/hol_light/x86_64/mlkem/keccak_f1600_x4_avx2_asm.S @@ -476,6 +476,12 @@ LLkeccak_f1600_x4_avx2: vmovhpd %xmm3, 0x188(%rdi) vmovq %xmm15, 0x250(%rdi) vmovhpd %xmm15, 0x318(%rdi) + vpxor %ymm0, %ymm0, %ymm0 + .set .Lkeccak_f1600_x4_avx2_clear_stack_offset, 0 + .rept 24 + vmovdqu %ymm0, .Lkeccak_f1600_x4_avx2_clear_stack_offset(%rsp) + .set .Lkeccak_f1600_x4_avx2_clear_stack_offset, .Lkeccak_f1600_x4_avx2_clear_stack_offset + 32 + .endr movq %r11, %rsp .cfi_def_cfa_register %rsp retq 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 4bd1123a25..651efda170 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 @@ -744,6 +744,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) *) 0x4c; 0x89; 0xdc; (* MOV (% rsp) (% r11) *) 0xc3 (* RET *) ];; @@ -762,7 +811,8 @@ let LENGTH_KECCAK_F1600_X4_AVX2_TMC = let KECCAK_F1600_X4_AVX2_PREAMBLE_LENGTH = new_definition `KECCAK_F1600_X4_AVX2_PREAMBLE_LENGTH = 14`;; -(* Postamble: MOV rsp, r11 (3 bytes) + RET (1 byte) = 4 bytes *) +(* Postamble: MOV rsp, r11 (3 bytes) + RET (1 byte) = 4 bytes. + The scratch wipe before this is part of the verified core body. *) let KECCAK_F1600_X4_AVX2_POSTAMBLE_LENGTH = new_definition `KECCAK_F1600_X4_AVX2_POSTAMBLE_LENGTH = 4`;; @@ -1015,7 +1065,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC [keccak; keccak_round] THEN ENSURES_INIT_TAC "s0" THEN - X86_STEPS_TAC KECCAK_F1600_X4_AVX2_EXEC (1--96) THEN + X86_STEPS_TAC KECCAK_F1600_X4_AVX2_EXEC (1--121) THEN REPEAT(FIRST_X_ASSUM(STRIP_ASSUME_TAC o CONV_RULE(READ_MEMORY_SPLIT_CONV 2) o check (can (term_match [] `read qqq s:int256 = xxx`) o concl))) THEN @@ -1057,6 +1107,7 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_CORRECT = prove wordlist_from_memory(word_add bitstate_in (word 400), 25) s = keccak 24 A3 /\ wordlist_from_memory(word_add bitstate_in (word 600), 25) s = keccak 24 A4) (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, + MAYCHANGE [events] ,, MAYCHANGE [memory :> bytes (bitstate_in, 800); memory :> bytes(word_sub stackpointer (word 0x31f), 0x31f)])`, (* Bridge the alignment preamble (mov r11,rsp; and rsp,-32; sub rsp,0x300) @@ -1151,6 +1202,7 @@ let KECCAK_F1600_X4_AVX2_SUBROUTINE_CORRECT = prove wordlist_from_memory(word_add bitstate_in (word 400), 25) s = keccak 24 A3 /\ wordlist_from_memory(word_add bitstate_in (word 600), 25) s = keccak 24 A4) (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, + MAYCHANGE [events] ,, MAYCHANGE [memory :> bytes (bitstate_in, 800); memory :> bytes(word_sub stackpointer (word 0x31f), 0x31f)])`, let TWEAK_CONV = ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV in @@ -1298,7 +1350,7 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_SAFE = time prove `inner_f_events:int64->int64->int64->int64->num->int64->uarch_event list` (LABEL_TAC "INNER_SAFE") inner_safe THEN (* Witness for the wrapper f_events: the kernel's events sandwiched - between the postamble's `mov rsp,r11; ret` events (an EventLoad of + before the postamble's final `mov rsp,r11; ret` events (an EventLoad of the return-address slot and an EventJump to it). The kernel's stackpointer arg is the aligned frame base, expressed as a function of the wrapper's (unaligned) `stackpointer` parameter. *) @@ -1370,30 +1422,14 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_SAFE = time prove (word_add (word_sub stackpointer (word 0x31f)) (word delta))))` THEN REWRITE_TAC[LENGTH_KECCAK_F1600_X4_AVX2_TMC] THEN REWRITE_TAC[APPEND] THEN - REWRITE_TAC[memaccess_inbounds; ALL] THEN - (* The two postamble events are trivially in bounds: EventJump is - ignored by memaccess_inbounds, and EventLoad (stackpointer, 8) - hits the explicit `(stackpointer, 8)` slot in the readable list. *) - CONJ_TAC THENL - [REWRITE_TAC[EX] THEN MESON_TAC[CONTAINED_MODULO_REFL; LE_REFL]; - ALL_TAC] THEN (* Widen the inner kernel's memaccess_inbounds claim (which mentions the aligned 768-byte frame) to the wrapper's footprint (which mentions the 0x31f-byte unaligned frame) using FRAME_CONTAINED. *) - REWRITE_TAC[GSYM memaccess_inbounds] THEN FIRST_X_ASSUM (fun th -> if (try fst (dest_eq (concl th)) = `e2:uarch_event list` with _ -> false) then SUBST_ALL_TAC th else NO_TAC) THEN - MATCH_MP_TAC (REWRITE_RULE[GSYM IMP_CONJ_ALT] MEMACCESS_INBOUNDS_CONTAINED) THEN - MAP_EVERY EXISTS_TAC - [`[bitstate_in:int64,800; rc_pointer,192; rho8_ptr,32; rho56_ptr,32; - word_add (word_sub stackpointer (word 0x31f)) (word delta),768]`; - `[bitstate_in:int64,800; - word_add (word_sub stackpointer (word 0x31f)) (word delta),768]`] THEN - ASM_REWRITE_TAC[ALL] THEN - REWRITE_TAC[EX] THEN - ASM_MESON_TAC[CONTAINED_REFL; FRAME_CONTAINED]);; + DISCHARGE_MEMACCESS_INBOUNDS_TAC);; let KECCAK_F1600_X4_AVX2_SUBROUTINE_SAFE = time prove (`exists f_events. From dec107ce565090f58b87f06137861ce586e79417 Mon Sep 17 00:00:00 2001 From: Joe Doyle Date: Tue, 30 Jun 2026 12:35:48 -0400 Subject: [PATCH 2/2] Sync ML-KEM Keccak generated wipes Regenerate the forced-cross Keccak outputs after adding stack clearing to the shared x4 source. The aarch64 host-local autogen path skipped the x86_64 generated files, but CI regenerates them on x86_64 and with forced cross toolchains. This expands the generated wipe-store blocks in the checked-in Armv8.1-M and x86_64 outputs so the native autogen and HOL-Light bytecode dry-run checks agree with the source. Co-authored-by: Codex Signed-off-by: Joe Doyle --- .../native/armv81m/src/keccak_f1600_x4_mve.S | 13 +++++---- .../x86_64/src/keccak_f1600_x4_avx2_asm.S | 29 +++++++++++++++---- .../x86_64/mlkem/keccak_f1600_x4_avx2_asm.S | 29 +++++++++++++++---- 3 files changed, 56 insertions(+), 15 deletions(-) diff --git a/mlkem/src/fips202/native/armv81m/src/keccak_f1600_x4_mve.S b/mlkem/src/fips202/native/armv81m/src/keccak_f1600_x4_mve.S index 0c95722dbd..eadc026a03 100644 --- a/mlkem/src/fips202/native/armv81m/src/keccak_f1600_x4_mve.S +++ b/mlkem/src/fips202/native/armv81m/src/keccak_f1600_x4_mve.S @@ -683,11 +683,14 @@ Lkeccak_f1600_x4_mve_asm_roundend_pre: Lkeccak_f1600_x4_mve_asm_roundend: movs r0, #0x0 vdup.32 q0, r0 - .set .Lkeccak_f1600_x4_mve_clear_stack_offset, 0 - .rept 8 - vstrw.32 q0, [sp, #.Lkeccak_f1600_x4_mve_clear_stack_offset] - .set .Lkeccak_f1600_x4_mve_clear_stack_offset, .Lkeccak_f1600_x4_mve_clear_stack_offset + 16 - .endr + vstrw.32 q0, [sp] + vstrw.32 q0, [sp, #16] + vstrw.32 q0, [sp, #32] + vstrw.32 q0, [sp, #48] + vstrw.32 q0, [sp, #64] + vstrw.32 q0, [sp, #80] + vstrw.32 q0, [sp, #96] + vstrw.32 q0, [sp, #112] add sp, #0x80 .cfi_adjust_cfa_offset -0x80 vpop {d8, d9, d10, d11, d12, d13, d14, d15} diff --git a/mlkem/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S b/mlkem/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S index 1c284ed689..fa6bf3ce1c 100644 --- a/mlkem/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S +++ b/mlkem/src/fips202/native/x86_64/src/keccak_f1600_x4_avx2_asm.S @@ -474,11 +474,30 @@ LLkeccak_f1600_x4_avx2: vmovq %xmm15, 0x250(%rdi) vmovhpd %xmm15, 0x318(%rdi) vpxor %ymm0, %ymm0, %ymm0 - .set .Lkeccak_f1600_x4_avx2_clear_stack_offset, 0 - .rept 24 - vmovdqu %ymm0, .Lkeccak_f1600_x4_avx2_clear_stack_offset(%rsp) - .set .Lkeccak_f1600_x4_avx2_clear_stack_offset, .Lkeccak_f1600_x4_avx2_clear_stack_offset + 32 - .endr + 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) movq %r11, %rsp .cfi_def_cfa_register %rsp retq diff --git a/proofs/hol_light/x86_64/mlkem/keccak_f1600_x4_avx2_asm.S b/proofs/hol_light/x86_64/mlkem/keccak_f1600_x4_avx2_asm.S index 630ef7d407..2c8addb002 100644 --- a/proofs/hol_light/x86_64/mlkem/keccak_f1600_x4_avx2_asm.S +++ b/proofs/hol_light/x86_64/mlkem/keccak_f1600_x4_avx2_asm.S @@ -477,11 +477,30 @@ LLkeccak_f1600_x4_avx2: vmovq %xmm15, 0x250(%rdi) vmovhpd %xmm15, 0x318(%rdi) vpxor %ymm0, %ymm0, %ymm0 - .set .Lkeccak_f1600_x4_avx2_clear_stack_offset, 0 - .rept 24 - vmovdqu %ymm0, .Lkeccak_f1600_x4_avx2_clear_stack_offset(%rsp) - .set .Lkeccak_f1600_x4_avx2_clear_stack_offset, .Lkeccak_f1600_x4_avx2_clear_stack_offset + 32 - .endr + 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) movq %r11, %rsp .cfi_def_cfa_register %rsp retq