CBMC: Add proof and contract for crypto_sign_keypair_internal

mldsa/poly.h

@@ -191,6 +191,7 @@ __contract__(
   requires(memory_no_alias(a0, sizeof(poly)))
   requires(memory_no_alias(a1, sizeof(poly)))
   requires(memory_no_alias(a, sizeof(poly)))
+  requires(a == a1)
   requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q))
   assigns(memory_slice(a1, sizeof(poly)))
   assigns(memory_slice(a0, sizeof(poly)))

mldsa/polyvec.h

@@ -391,6 +391,7 @@ __contract__(
   requires(memory_no_alias(v1, sizeof(polyveck)))
   requires(memory_no_alias(v0, sizeof(polyveck)))
   requires(memory_no_alias(v, sizeof(polyveck)))
+  requires(v == v1)
   requires(forall(k0, 0, MLDSA_K, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
   assigns(memory_slice(v1, sizeof(polyveck)))
   assigns(memory_slice(v0, sizeof(polyveck)))

mldsa/sign.c

@@ -18,17 +18,18 @@ int crypto_sign_keypair_internal(uint8_t *pk, uint8_t *sk,
                                  const uint8_t seed[MLDSA_SEEDBYTES])
 {
   uint8_t seedbuf[2 * MLDSA_SEEDBYTES + MLDSA_CRHBYTES];
+  uint8_t inbuf[MLDSA_SEEDBYTES + 2];
   uint8_t tr[MLDSA_TRBYTES];
   const uint8_t *rho, *rhoprime, *key;
   polyvecl mat[MLDSA_K];
   polyvecl s1, s1hat;
   polyveck s2, t1, t0;
 
   /* Get randomness for rho, rhoprime and key */
-  memcpy(seedbuf, seed, MLDSA_SEEDBYTES);
-  seedbuf[MLDSA_SEEDBYTES + 0] = MLDSA_K;
-  seedbuf[MLDSA_SEEDBYTES + 1] = MLDSA_L;
-  shake256(seedbuf, 2 * MLDSA_SEEDBYTES + MLDSA_CRHBYTES, seedbuf,
+  memcpy(inbuf, seed, MLDSA_SEEDBYTES);
+  inbuf[MLDSA_SEEDBYTES + 0] = MLDSA_K;
+  inbuf[MLDSA_SEEDBYTES + 1] = MLDSA_L;
+  shake256(seedbuf, 2 * MLDSA_SEEDBYTES + MLDSA_CRHBYTES, inbuf,
            MLDSA_SEEDBYTES + 2);
   rho = seedbuf;
   rhoprime = rho + MLDSA_SEEDBYTES;
@@ -149,9 +150,6 @@ int crypto_sign_signature_internal(uint8_t *sig, size_t *siglen,
   /* The loop statement also supplies a syntactic location to */
   /* place loop invariants for CBMC.                          */
   while (1)
-  __loop__(
-    invariant(true); /* TODO */
-  )
   {
     /* Sample intermediate vector y */
     polyvecl_uniform_gamma1(&y, rhoprime, nonce++);

mldsa/sign.h

@@ -7,11 +7,12 @@
 
 #include <stddef.h>
 #include <stdint.h>
+#include "cbmc.h"
 #include "common.h"
 #include "poly.h"
 #include "polyvec.h"
 
-#define crypto_sign_keypair_internal MLD_NAMESPACE(keypair_internal)
+#define crypto_sign_keypair_internal MLD_NAMESPACE(crypto_sign_keypair_internal)
 /*************************************************
  * Name:        crypto_sign_keypair_internal
  *
@@ -28,7 +29,14 @@
  * Returns 0 (success)
  **************************************************/
 int crypto_sign_keypair_internal(uint8_t *pk, uint8_t *sk,
-                                 const uint8_t seed[MLDSA_SEEDBYTES]);
+                                 const uint8_t seed[MLDSA_SEEDBYTES])
+__contract__(
+  requires(memory_no_alias(pk, CRYPTO_PUBLICKEYBYTES))
+  requires(memory_no_alias(sk, CRYPTO_SECRETKEYBYTES))
+  requires(memory_no_alias(seed, MLDSA_SEEDBYTES))
+  assigns(object_whole(pk))
+  assigns(object_whole(sk))
+);
 
 #define crypto_sign_keypair MLD_NAMESPACE(keypair)
 /*************************************************

proofs/cbmc/crypto_sign_keypair_internal/Makefile

@@ -0,0 +1,67 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = crypto_sign_keypair_internal_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = crypto_sign_keypair_internal
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += 
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)crypto_sign_keypair_internal
+USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_expand
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)poly_uniform_eta_4x
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvecl_ntt
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_reduce
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_invntt_tomont
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_add
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_caddq
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_power2round
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)pack_pk
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)pack_sk
+
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = crypto_sign_keypair_internal
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 9
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

proofs/cbmc/crypto_sign_keypair_internal/crypto_sign_keypair_internal_harness.c

@@ -0,0 +1,10 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "sign.h"
+
+void harness(void)
+{
+  uint8_t *a, *b, *c;
+  crypto_sign_keypair_internal(a, b, c);
+}