Add Pairwise Consistency Test (PCT) for FIPS-204 IG compliance

jakemas · jakemas · commit 74dc17aab1ba · 2025-07-23T19:15:57.000-07:00
- Implement PCT functionality in mldsa/sign.c with check_pct function
- Add PCT configuration in mldsa/config.h
- Add CBMC proof and specification for check_pct
- Include comprehensive test harness for verification

Complete proof of check_pct()

Weakens pre-conditions of crypto_sign_verify()
and crypto_sign_signature() to deal with the
case where ctx == NULL &amp;&amp; ctxlen == 0, which
is required by check_pct()

Signed-off-by: Jake Massimo &lt;jakemas@amazon.com&gt;
diff --git a/mldsa/config.h b/mldsa/config.h
@@ -59,4 +59,42 @@
 #define MLD_CONFIG_FIPS202_BACKEND_FILE "fips202/native/auto.h"
 #endif
 
+/******************************************************************************
+ * Name:        MLD_CONFIG_KEYGEN_PCT
+ *
+ * Description: Compliance with @[FIPS140_3_IG, p.87] requires a
+ *              Pairwise Consistency Test (PCT) to be carried out on a freshly
+ *              generated keypair before it can be exported.
+ *
+ *              Set this option if such a check should be implemented.
+ *              In this case, crypto_sign_keypair_internal and
+ *              crypto_sign_keypair will return a non-zero error code if the
+ *              PCT failed.
+ *
+ *              NOTE: This feature will drastically lower the performance of
+ *              key generation.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_KEYGEN_PCT */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TEST
+ *
+ * Description: If this option is set, the user must provide a runtime
+ *              function `static inline int mld_break_pct() { ... }` to
+ *              indicate whether the PCT should be made fail.
+ *
+ *              This option only has an effect if MLD_CONFIG_KEYGEN_PCT is set.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TEST
+   #if !defined(__ASSEMBLER__)
+   #include "sys.h"
+   static MLD_INLINE int mld_break_pct(void)
+   {
+       ... return 0/1 depending on whether PCT should be broken ...
+   }
+   #endif
+*/
+
 #endif /* !MLD_CONFIG_H */
diff --git a/mldsa/sign.c b/mldsa/sign.c
@@ -14,6 +14,79 @@
 #include "sign.h"
 #include "symmetric.h"
 
+
+static int mld_check_pct(uint8_t const pk[CRYPTO_PUBLICKEYBYTES],
+                         uint8_t const sk[CRYPTO_SECRETKEYBYTES])
+__contract__(
+  requires(memory_no_alias(pk, CRYPTO_PUBLICKEYBYTES))
+  requires(memory_no_alias(sk, CRYPTO_SECRETKEYBYTES))
+  ensures(return_value == 0 || return_value == -1)
+);
+
+#if defined(MLD_CONFIG_KEYGEN_PCT)
+/*************************************************
+ * [FIPS 140-3 IG]
+ * (https://csrc.nist.gov/csrc/media/Projects/cryptographic-module-validation-program/documents/fips%20140-3/FIPS%20140-3%20IG.pdf)
+ *
+ * TE10.35.02: Pair-wise Consistency Test (PCT) for DSA keypairs
+ *
+ * Purpose: Validates that a generated public/private key pair can correctly
+ * sign and verify data. Test performs signature generation using the private
+ * key (sk), followed by signature verification using the public key (pk).
+ * Returns 0 if the signature was successfully verified, non-zero if it cannot.
+ *
+ * Note: FIPS 204 requires that public/private key pairs are to be used only for
+ * the calculation and/of verification of digital signatures.
+ **************************************************/
+static int mld_check_pct(uint8_t const pk[CRYPTO_PUBLICKEYBYTES],
+                         uint8_t const sk[CRYPTO_SECRETKEYBYTES])
+{
+  uint8_t message[1] = {0};
+  uint8_t signature[CRYPTO_BYTES];
+  uint8_t pk_test[CRYPTO_PUBLICKEYBYTES];
+  size_t siglen;
+  int ret;
+
+  /* Copy public key for testing */
+  memcpy(pk_test, pk, CRYPTO_PUBLICKEYBYTES);
+
+  /* Sign a test message using the original secret key */
+  ret = crypto_sign_signature(signature, &siglen, message, sizeof(message),
+                              NULL, 0, sk);
+  if (ret == 0)
+  {
+#if defined(MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TEST)
+    /* Deliberately break public key for testing purposes */
+    if (mld_break_pct())
+    {
+      pk_test[0] = ~pk_test[0];
+    }
+#endif /* MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TEST */
+
+    /* Verify the signature using the (potentially corrupted) public key */
+    ret = crypto_sign_verify(signature, siglen, message, sizeof(message), NULL,
+                             0, pk_test);
+  }
+
+  /* Specification: Partially implements
+   * @[FIPS204, Section 3.6.3, Destruction of intermediate values]
+   TODO: add these when the rest of destruction of intermediate values are added
+    mld_zeroize(signature, sizeof(signature));
+    mld_zeroize(pk_test, sizeof(pk_test));
+  */
+  return ret;
+}
+#else  /* MLD_CONFIG_KEYGEN_PCT */
+static int mld_check_pct(uint8_t const pk[CRYPTO_PUBLICKEYBYTES],
+                         uint8_t const sk[CRYPTO_SECRETKEYBYTES])
+{
+  /* Skip PCT */
+  ((void)pk);
+  ((void)sk);
+  return 0;
+}
+#endif /* !MLD_CONFIG_KEYGEN_PCT */
+
 static void mld_sample_s1_s2(mld_polyvecl *s1, mld_polyveck *s2,
                              const uint8_t seed[MLDSA_CRHBYTES])
 __contract__(
@@ -96,6 +169,12 @@ int crypto_sign_keypair_internal(uint8_t *pk, uint8_t *sk,
   /* Compute H(rho, t1) and write secret key */
   shake256(tr, MLDSA_TRBYTES, pk, CRYPTO_PUBLICKEYBYTES);
   mld_pack_sk(sk, rho, tr, key, &t0, &s1, &s2);
+
+  /* Pairwise Consistency Test (PCT) @[FIPS140_3_IG, p.87] */
+  if (mld_check_pct(pk, sk))
+  {
+    return -1;
+  }
   return 0;
 }
 
diff --git a/mldsa/sign.h b/mldsa/sign.h
@@ -18,6 +18,8 @@
  *
  * Description: FIPS 204: Algorithm 6 ML-DSA.KeyGen_internal.
  *              Generates public and private key. Internal API.
+ *              When MLD_CONFIG_KEYGEN_PCT is set, performs a Pairwise
+ *              Consistency Test (PCT) as required by FIPS 140-3 IG.
  *
  * Arguments:   - uint8_t *pk:   pointer to output public key (allocated
  *                               array of CRYPTO_PUBLICKEYBYTES bytes)
@@ -26,7 +28,7 @@
  *              - uint8_t *seed: pointer to input random seed (MLDSA_SEEDBYTES
  *                               bytes)
  *
- * Returns 0 (success)
+ * Returns 0 (success) or -1 (PCT failure)
  **************************************************/
 int crypto_sign_keypair_internal(uint8_t *pk, uint8_t *sk,
                                  const uint8_t seed[MLDSA_SEEDBYTES])
@@ -36,6 +38,7 @@ __contract__(
   requires(memory_no_alias(seed, MLDSA_SEEDBYTES))
   assigns(object_whole(pk))
   assigns(object_whole(sk))
+  ensures(return_value == 0 || return_value == -1)
 );
 
 #define crypto_sign_keypair MLD_NAMESPACE(keypair)
@@ -44,20 +47,23 @@ __contract__(
  *
  * Description: FIPS 204: Algorithm 1 ML-DSA.KeyGen
  *              Generates public and private key.
+ *              When MLD_CONFIG_KEYGEN_PCT is set, performs a Pairwise
+ *              Consistency Test (PCT) as required by FIPS 140-3 IG.
  *
  * Arguments:   - uint8_t *pk:   pointer to output public key (allocated
  *                               array of CRYPTO_PUBLICKEYBYTES bytes)
  *              - uint8_t *sk:   pointer to output private key (allocated
  *                               array of CRYPTO_SECRETKEYBYTES bytes)
  *
- * Returns 0 (success)
+ * Returns 0 (success) or -1 (PCT failure)
  **************************************************/
 int crypto_sign_keypair(uint8_t *pk, uint8_t *sk)
 __contract__(
   requires(memory_no_alias(pk, CRYPTO_PUBLICKEYBYTES))
   requires(memory_no_alias(sk, CRYPTO_SECRETKEYBYTES))
   assigns(object_whole(pk))
   assigns(object_whole(sk))
+  ensures(return_value == 0 || return_value == -1)
 );
 
 #define crypto_sign_signature_internal MLD_NAMESPACE(signature_internal)
@@ -117,8 +123,9 @@ __contract__(
  *              - size_t *siglen: pointer to output length of signature
  *              - uint8_t *m:     pointer to message to be signed
  *              - size_t mlen:    length of message
- *              - uint8_t *ctx:   pointer to contex string
- *              - size_t ctxlen:  length of contex string. Should be <= 255.
+ *              - uint8_t *ctx:   pointer to context string. May be NULL
+ *                                iff ctxlen == 0
+ *              - size_t ctxlen:  length of context string. Should be <= 255.
  *              - uint8_t *sk:    pointer to bit-packed secret key
  *
  * Returns 0 (success) or -1 (context string too long OR nonce exhaustion)
@@ -130,7 +137,7 @@ __contract__(
   requires(memory_no_alias(sig, CRYPTO_BYTES))
   requires(memory_no_alias(siglen, sizeof(size_t)))
   requires(memory_no_alias(m, mlen))
-  requires(memory_no_alias(ctx, ctxlen))
+  requires((ctx == NULL && ctxlen == 0) || memory_no_alias(ctx, ctxlen))
   requires(memory_no_alias(sk, CRYPTO_SECRETKEYBYTES))
   assigns(memory_slice(sig, CRYPTO_BYTES))
   assigns(object_whole(siglen))
@@ -243,6 +250,7 @@ __contract__(
  *              - const uint8_t *m: pointer to message
  *              - size_t mlen: length of message
  *              - const uint8_t *ctx: pointer to context string
+ *                                    May be NULL iff ctxlen == 0
  *              - size_t ctxlen: length of context string
  *              - const uint8_t *pk: pointer to bit-packed public key
  *
@@ -254,7 +262,7 @@ int crypto_sign_verify(const uint8_t *sig, size_t siglen, const uint8_t *m,
 __contract__(
   requires(memory_no_alias(sig, siglen))
   requires(memory_no_alias(m, mlen))
-  requires(memory_no_alias(ctx, ctxlen))
+  requires((ctx == NULL && ctxlen == 0) || memory_no_alias(ctx, ctxlen))
   requires(memory_no_alias(pk, CRYPTO_PUBLICKEYBYTES))
   ensures(return_value == 0 || return_value == -1)
 );
diff --git a/proofs/cbmc/check_pct/Makefile b/proofs/cbmc/check_pct/Makefile
@@ -0,0 +1,55 @@
+# 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 = check_pct_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 = mld_check_pct
+
+DEFINES += -DMLD_CONFIG_KEYGEN_PCT
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c
+
+CHECK_FUNCTION_CONTRACTS=mld_check_pct
+USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature $(MLD_NAMESPACE)verify
+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 = mld_check_pct
+
+# 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 = 8
+
+# 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/sign.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/sign.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
diff --git a/proofs/cbmc/check_pct/check_pct_harness.c b/proofs/cbmc/check_pct/check_pct_harness.c
@@ -0,0 +1,14 @@
+// Copyright (c) The mldsa-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include "sign.h"
+
+int mld_check_pct(uint8_t const pk[CRYPTO_PUBLICKEYBYTES],
+                  uint8_t const sk[CRYPTO_SECRETKEYBYTES]);
+
+void harness(void)
+{
+  uint8_t *a, *b;
+  mld_check_pct(a, b);
+}
diff --git a/proofs/cbmc/crypto_sign_keypair_internal/Makefile b/proofs/cbmc/crypto_sign_keypair_internal/Makefile
@@ -32,6 +32,7 @@ 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
+USE_FUNCTION_CONTRACTS+=mld_check_pct
 
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
