Replace mld_zeroize with memset when zeroing state

bremoran · bremoran · commit a8da8c65be37 · 2025-09-08T13:41:31.000+01:00
Signed-off-by: Brendan Moran &lt;brendan.moran@arm.com&gt;
diff --git a/mldsa/fips202/fips202.c b/mldsa/fips202/fips202.c
@@ -28,7 +28,7 @@ __contract__(
   assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
 )
 {
-  mld_zeroize(s, sizeof(uint64_t) * MLD_KECCAK_LANES);
+  memset(s, 0, sizeof(uint64_t) * MLD_KECCAK_LANES);
   cassert(forall(k, 0, MLD_KECCAK_LANES, s[k] == 0));
 }
 
@@ -187,7 +187,8 @@ __contract__(
   requires(memory_no_alias(in, inlen))
   assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)))
 {
-  mld_zeroize(s, sizeof(uint64_t) * MLD_KECCAK_LANES);
+  memset(s, 0, sizeof(uint64_t) * MLD_KECCAK_LANES);
+  cassert(forall(k, 0, MLD_KECCAK_LANES, s[k] == 0));
 
   while (inlen >= r)
   __loop__(
diff --git a/proofs/cbmc/keccak_absorb_once/Makefile b/proofs/cbmc/keccak_absorb_once/Makefile
@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mldsa/fips202/fips202.c
 
 CHECK_FUNCTION_CONTRACTS=keccak_absorb_once
-USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccakf1600_permute $(FIPS202_NAMESPACE)keccakf1600_xor_bytes keccak_finalize mld_zeroize
+USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccakf1600_permute $(FIPS202_NAMESPACE)keccakf1600_xor_bytes keccak_finalize
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
diff --git a/proofs/cbmc/keccak_init/Makefile b/proofs/cbmc/keccak_init/Makefile
@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mldsa/fips202/fips202.c
 
 CHECK_FUNCTION_CONTRACTS=keccak_init
-USE_FUNCTION_CONTRACTS=mld_zeroize
+USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 

Original file line number	Diff line number	Diff line change
`@@ -28,7 +28,7 @@ __contract__(`
`28`	`28`	`assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES))`
`29`	`29`	`)`
`30`	`30`	`{`
`31`		`- mld_zeroize(s, sizeof(uint64_t) * MLD_KECCAK_LANES);`
	`31`	`+ memset(s, 0, sizeof(uint64_t) * MLD_KECCAK_LANES);`
`32`	`32`	`cassert(forall(k, 0, MLD_KECCAK_LANES, s[k] == 0));`
`33`	`33`	`}`
`34`	`34`
`@@ -187,7 +187,8 @@ __contract__(`
`187`	`187`	`requires(memory_no_alias(in, inlen))`
`188`	`188`	`assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)))`
`189`	`189`	`{`
`190`		`- mld_zeroize(s, sizeof(uint64_t) * MLD_KECCAK_LANES);`
	`190`	`+ memset(s, 0, sizeof(uint64_t) * MLD_KECCAK_LANES);`
	`191`	`+ cassert(forall(k, 0, MLD_KECCAK_LANES, s[k] == 0));`
`191`	`192`
`192`	`193`	`while (inlen >= r)`
`193`	`194`	`__loop__(`