[Test] Namespacing: Add MLD_CONFIG_PARAMETER_SET + MLD_CONFIG_NAMESPACE_PREFIX

.github/actions/cbmc/action.yml

@@ -18,9 +18,9 @@ inputs:
   custom_shell:
     description: The shell to use. Only relevant if use-nix is 'false'
     default: "bash"
-  mldsa_mode:
-    description: "Security level for ML-DSA (2,3,5)"
-    default: "2"
+  mldsa_parameter_set:
+    description: "Parameter set for ML-DSA (44,65,87)"
+    default: "44"
   gh_token:
     description: Github access token to use
     required: true
@@ -50,9 +50,9 @@ runs:
               - Cadical Version $(cadical --version)
               - $(bash --version | grep -m1 "")
             EOF
-      - name: Run CBMC proofs (MLDSA_MODE=${{ inputs.mldsa_mode }})
+      - name: Run CBMC proofs (MLD_CONFIG_PARAMETER_SET=${{ inputs.mldsa_parameter_set }})
         shell: ${{ env.SHELL }}
         run: |
-          echo "::group::cbmc_${{ inputs.mldsa_mode }}"
-          tests cbmc --mode ${{ inputs.mldsa_mode }};
+          echo "::group::cbmc_${{ inputs.mldsa_parameter_set }}"
+          tests cbmc --parameter-set ${{ inputs.mldsa_parameter_set }};
           echo "::endgroup::"

.github/workflows/cbmc.yml

@@ -28,7 +28,7 @@ jobs:
       kattest: false
       acvptest: false
       cbmc: true
-      cbmc_mldsa_mode: 2
+      cbmc_mldsa_parameter_set: 44
     secrets: inherit
   cbmc_65:
     name: CBMC (ML-DSA-65)
@@ -50,7 +50,7 @@ jobs:
       kattest: false
       acvptest: false
       cbmc: true
-      cbmc_mldsa_mode: 3
+      cbmc_mldsa_parameter_set: 65
     secrets: inherit
   cbmc_87:
     name: CBMC (ML-DSA-87)
@@ -72,5 +72,5 @@ jobs:
       kattest: false
       acvptest: false
       cbmc: true
-      cbmc_mldsa_mode: 5
+      cbmc_mldsa_parameter_set: 87
     secrets: inherit

.github/workflows/ci_ec2_reusable.yml

@@ -61,9 +61,9 @@ on:
       slothy:
         type: boolean
         default: false
-      cbmc_mldsa_mode:
+      cbmc_mldsa_parameter_set:
         type: string
-        default: 2
+        default: 44
 env:
   AWS_ROLE: arn:aws:iam::904233116199:role/mldsa-native-ci
   AWS_REGION: us-east-1
@@ -174,7 +174,7 @@ jobs:
         with:
           nix-shell: ci-cbmc
           nix-verbose: ${{ inputs.verbose }}
-          mldsa_mode: ${{ inputs.cbmc_mldsa_mode }}
+          mldsa_parameter_set: ${{ inputs.cbmc_mldsa_parameter_set }}
           gh_token: ${{ secrets.AWS_GITHUB_TOKEN }}
       # - name: SLOTHY
       #   if: ${{ inputs.slothy }}

Makefile

@@ -33,6 +33,7 @@ $(error Neither 'shasum' nor 'sha256sum' found. Please install one of these tool
 endif
 
 include test/mk/config.mk
+include test/mk/compiler.mk
 include test/mk/components.mk
 include test/mk/rules.mk
 

Makefile.Microsoft_nmake

@@ -31,57 +31,57 @@ OPT = 0
 # compilation for mldsa44
 {mldsa}.c{$(MLDSA44_BUILD_DIR)\mldsa}.obj::
     @if NOT EXIST $(MLDSA44_BUILD_DIR)\mldsa mkdir $(MLDSA44_BUILD_DIR)\mldsa
-    $(CC) $(CFLAGS) /D MLDSA_MODE=2 /c /Fo$(MLDSA44_BUILD_DIR)\mldsa\ $<
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=44 /c /Fo$(MLDSA44_BUILD_DIR)\mldsa\ $<
 
 {mldsa\fips202}.c{$(MLDSA44_BUILD_DIR)\mldsa\fips202}.obj::
     @if NOT EXIST $(MLDSA44_BUILD_DIR)\mldsa\fips202 mkdir $(MLDSA44_BUILD_DIR)\mldsa\fips202
-    $(CC) $(CFLAGS) /D MLDSA_MODE=2 /c /Fo$(MLDSA44_BUILD_DIR)\mldsa\fips202\ $<
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=44 /c /Fo$(MLDSA44_BUILD_DIR)\mldsa\fips202\ $<
 
 {test}.c{$(MLDSA44_BUILD_DIR)\test}.obj::
     @if NOT EXIST $(MLDSA44_BUILD_DIR)\test mkdir $(MLDSA44_BUILD_DIR)\test
-    $(CC) $(CFLAGS) /D MLDSA_MODE=2 /c /Fo$(MLDSA44_BUILD_DIR)\test\ $<
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=44 /c /Fo$(MLDSA44_BUILD_DIR)\test\ $<
 
 # compilation for mldsa65
 {mldsa}.c{$(MLDSA65_BUILD_DIR)\mldsa}.obj::
     @if NOT EXIST $(MLDSA65_BUILD_DIR)\mldsa mkdir $(MLDSA65_BUILD_DIR)\mldsa
-    $(CC) $(CFLAGS) /D MLDSA_MODE=3 /c /Fo$(MLDSA65_BUILD_DIR)\mldsa\ $<
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=65 /c /Fo$(MLDSA65_BUILD_DIR)\mldsa\ $<
 
 {mldsa\fips202}.c{$(MLDSA65_BUILD_DIR)\mldsa\fips202}.obj::
     @if NOT EXIST $(MLDSA65_BUILD_DIR)\mldsa\fips202 mkdir $(MLDSA65_BUILD_DIR)\mldsa\fips202
-    $(CC) $(CFLAGS) /D MLDSA_MODE=3 /c /Fo$(MLDSA65_BUILD_DIR)\mldsa\fips202\ $<
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=65 /c /Fo$(MLDSA65_BUILD_DIR)\mldsa\fips202\ $<
 
 {test}.c{$(MLDSA65_BUILD_DIR)\test}.obj::
     @if NOT EXIST $(MLDSA65_BUILD_DIR)\test mkdir $(MLDSA65_BUILD_DIR)\test
-    $(CC) $(CFLAGS) /D MLDSA_MODE=3 /c /Fo$(MLDSA65_BUILD_DIR)\test\ $<
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=65 /c /Fo$(MLDSA65_BUILD_DIR)\test\ $<
 
 # compilation for mldsa87
 {mldsa}.c{$(MLDSA87_BUILD_DIR)\mldsa}.obj::
     @if NOT EXIST $(MLDSA87_BUILD_DIR)\mldsa mkdir $(MLDSA87_BUILD_DIR)\mldsa
-    $(CC) $(CFLAGS) /D MLDSA_MODE=5 /c /Fo$(MLDSA87_BUILD_DIR)\mldsa\ $<
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=87 /c /Fo$(MLDSA87_BUILD_DIR)\mldsa\ $<
 
 {mldsa\fips202}.c{$(MLDSA87_BUILD_DIR)\mldsa\fips202}.obj::
     @if NOT EXIST $(MLDSA87_BUILD_DIR)\mldsa\fips202 mkdir $(MLDSA87_BUILD_DIR)\mldsa\fips202
-    $(CC) $(CFLAGS) /D MLDSA_MODE=5 /c /Fo$(MLDSA87_BUILD_DIR)\mldsa\fips202\ $<
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=87 /c /Fo$(MLDSA87_BUILD_DIR)\mldsa\fips202\ $<
 
 {test}.c{$(MLDSA87_BUILD_DIR)\test}.obj::
     @if NOT EXIST $(MLDSA87_BUILD_DIR)\test mkdir $(MLDSA87_BUILD_DIR)\test
-    $(CC) $(CFLAGS) /D MLDSA_MODE=5 /c /Fo$(MLDSA87_BUILD_DIR)\test\ $<
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=87 /c /Fo$(MLDSA87_BUILD_DIR)\test\ $<
 
 
 # compile functional test for mldsa44
 test_mldsa44: $(OBJ_FILES_44) $(MLDSA44_BUILD_DIR)\test\test_mldsa.obj $(BUILD_DIR)\randombytes\notrandombytes.obj
     @if NOT EXIST $(MLDSA44_BUILD_DIR)\bin mkdir $(MLDSA44_BUILD_DIR)\bin
-    $(CC) $(CFLAGS) /D MLDSA_MODE=2 /Fe$(MLDSA44_BUILD_DIR)\bin\test_mldsa44 $** /link
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=44 /Fe$(MLDSA44_BUILD_DIR)\bin\test_mldsa44 $** /link
 
 # compile functional test for mldsa65
 test_mldsa65: $(OBJ_FILES_65) $(MLDSA65_BUILD_DIR)\test\test_mldsa.obj $(BUILD_DIR)\randombytes\notrandombytes.obj
     @if NOT EXIST $(MLDSA65_BUILD_DIR)\bin mkdir $(MLDSA65_BUILD_DIR)\bin
-    $(CC) $(CFLAGS) /D MLDSA_MODE=3 /Fe$(MLDSA65_BUILD_DIR)\bin\test_mldsa65 $** /link
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=65 /Fe$(MLDSA65_BUILD_DIR)\bin\test_mldsa65 $** /link
 
 # compile functional test for mldsa87
 test_mldsa87: $(OBJ_FILES_87) $(MLDSA87_BUILD_DIR)\test\test_mldsa.obj $(BUILD_DIR)\randombytes\notrandombytes.obj
     @if NOT EXIST $(MLDSA87_BUILD_DIR)\bin mkdir $(MLDSA87_BUILD_DIR)\bin
-    $(CC) $(CFLAGS) /D MLDSA_MODE=5 /Fe$(MLDSA87_BUILD_DIR)\bin\test_mldsa87 $** /link
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=87 /Fe$(MLDSA87_BUILD_DIR)\bin\test_mldsa87 $** /link
 
 quickcheck: test_mldsa44 test_mldsa65 test_mldsa87
     $(MLDSA44_BUILD_DIR)\bin\test_mldsa44.exe

mldsa/api.h

@@ -7,107 +7,40 @@
 
 #include <stddef.h>
 #include <stdint.h>
+#include "common.h"
 
 #define MLD_44_PUBLICKEYBYTES 1312
 #define MLD_44_SECRETKEYBYTES 2560
 #define MLD_44_BYTES 2420
 
-#define MLD_44_ref_PUBLICKEYBYTES MLD_44_PUBLICKEYBYTES
-#define MLD_44_ref_SECRETKEYBYTES MLD_44_SECRETKEYBYTES
-#define MLD_44_ref_BYTES MLD_44_BYTES
-
-int MLD_44_ref_keypair(uint8_t *pk, uint8_t *sk);
-
-int MLD_44_ref_signature(uint8_t *sig, size_t *siglen, const uint8_t *m,
-                         size_t mlen, const uint8_t *ctx, size_t ctxlen,
-                         const uint8_t *sk);
-
-int MLD_44_ref(uint8_t *sm, size_t *smlen, const uint8_t *m, size_t mlen,
-               const uint8_t *ctx, size_t ctxlen, const uint8_t *sk);
-
-int MLD_44_ref_verify(const uint8_t *sig, size_t siglen, const uint8_t *m,
-                      size_t mlen, const uint8_t *ctx, size_t ctxlen,
-                      const uint8_t *pk);
-
-int MLD_44_ref_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen,
-                    const uint8_t *ctx, size_t ctxlen, const uint8_t *pk);
-
 #define MLD_65_PUBLICKEYBYTES 1952
 #define MLD_65_SECRETKEYBYTES 4032
 #define MLD_65_BYTES 3309
 
-#define MLD_65_ref_PUBLICKEYBYTES MLD_65_PUBLICKEYBYTES
-#define MLD_65_ref_SECRETKEYBYTES MLD_65_SECRETKEYBYTES
-#define MLD_65_ref_BYTES MLD_65_BYTES
-
-int MLD_65_ref_keypair(uint8_t *pk, uint8_t *sk);
-
-int MLD_65_ref_signature(uint8_t *sig, size_t *siglen, const uint8_t *m,
-                         size_t mlen, const uint8_t *ctx, size_t ctxlen,
-                         const uint8_t *sk);
-
-int MLD_65_ref(uint8_t *sm, size_t *smlen, const uint8_t *m, size_t mlen,
-               const uint8_t *ctx, size_t ctxlen, const uint8_t *sk);
-
-int MLD_65_ref_verify(const uint8_t *sig, size_t siglen, const uint8_t *m,
-                      size_t mlen, const uint8_t *ctx, size_t ctxlen,
-                      const uint8_t *pk);
-
-int MLD_65_ref_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen,
-                    const uint8_t *ctx, size_t ctxlen, const uint8_t *pk);
-
 #define MLD_87_PUBLICKEYBYTES 2592
 #define MLD_87_SECRETKEYBYTES 4896
 #define MLD_87_BYTES 4627
 
-#define MLD_87_ref_PUBLICKEYBYTES MLD_87_PUBLICKEYBYTES
-#define MLD_87_ref_SECRETKEYBYTES MLD_87_SECRETKEYBYTES
-#define MLD_87_ref_BYTES MLD_87_BYTES
-
-int MLD_87_ref_keypair(uint8_t *pk, uint8_t *sk);
-
-int MLD_87_ref_signature(uint8_t *sig, size_t *siglen, const uint8_t *m,
-                         size_t mlen, const uint8_t *ctx, size_t ctxlen,
-                         const uint8_t *sk);
 
-int MLD_87_ref(uint8_t *sm, size_t *smlen, const uint8_t *m, size_t mlen,
-               const uint8_t *ctx, size_t ctxlen, const uint8_t *sk);
-
-int MLD_87_ref_verify(const uint8_t *sig, size_t siglen, const uint8_t *m,
-                      size_t mlen, const uint8_t *ctx, size_t ctxlen,
-                      const uint8_t *pk);
-
-int MLD_87_ref_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen,
-                    const uint8_t *ctx, size_t ctxlen, const uint8_t *pk);
-
-#if MLDSA_MODE == 2
+#if MLD_CONFIG_PARAMETER_SET == 44
 #define CRYPTO_PUBLICKEYBYTES MLD_44_PUBLICKEYBYTES
 #define CRYPTO_SECRETKEYBYTES MLD_44_SECRETKEYBYTES
 #define CRYPTO_BYTES MLD_44_BYTES
-#define crypto_sign_keypair MLD_44_ref_keypair
-#define crypto_sign_signature MLD_44_ref_signature
-#define crypto_sign MLD_44_ref
-#define crypto_sign_verify MLD_44_ref_verify
-#define crypto_sign_open MLD_44_ref_open
-#elif MLDSA_MODE == 3
+#elif MLD_CONFIG_PARAMETER_SET == 65
 #define CRYPTO_PUBLICKEYBYTES MLD_65_PUBLICKEYBYTES
 #define CRYPTO_SECRETKEYBYTES MLD_65_SECRETKEYBYTES
 #define CRYPTO_BYTES MLD_65_BYTES
-#define crypto_sign_keypair MLD_65_ref_keypair
-#define crypto_sign_signature MLD_65_ref_signature
-#define crypto_sign MLD_65_ref
-#define crypto_sign_verify MLD_65_ref_verify
-#define crypto_sign_open MLD_65_ref_open
-#elif MLDSA_MODE == 5
+#elif MLD_CONFIG_PARAMETER_SET == 87
 #define CRYPTO_PUBLICKEYBYTES MLD_87_PUBLICKEYBYTES
 #define CRYPTO_SECRETKEYBYTES MLD_87_SECRETKEYBYTES
 #define CRYPTO_BYTES MLD_87_BYTES
-#define crypto_sign_keypair MLD_87_ref_keypair
-#define crypto_sign_signature MLD_87_ref_signature
-#define crypto_sign MLD_87_ref
-#define crypto_sign_verify MLD_87_ref_verify
-#define crypto_sign_open MLD_87_ref_open
-#endif /* MLDSA_MODE == 5 */
+#endif
+
+#define crypto_sign_keypair MLD_NAMESPACE_K(keypair)
+#define crypto_sign_signature MLD_NAMESPACE_K(signature)
+#define crypto_sign MLD_NAMESPACE_K(sign)
+#define crypto_sign_verify MLD_NAMESPACE_K(verify)
+#define crypto_sign_open MLD_NAMESPACE_K(open)
 
 
 #endif /* !MLD_API_H */

mldsa/common.h

@@ -16,19 +16,50 @@
 #include "params.h"
 #include "sys.h"
 
+/* Internal and public API have external linkage by default, but
+ * this can be overwritten by the user, e.g. for single-CU builds. */
+#if !defined(MLD_CONFIG_INTERNAL_API_QUALIFIER)
+#define MLD_INTERNAL_API
+#else
+#define MLD_INTERNAL_API MLD_CONFIG_INTERNAL_API_QUALIFIER
+#endif
 
-#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) && \
-    !defined(MLD_CONFIG_ARITH_BACKEND_FILE)
-#error Bad configuration: MLD_CONFIG_USE_NATIVE_BACKEND_ARITH is set, but MLD_CONFIG_ARITH_BACKEND_FILE is not.
+#if !defined(MLD_CONFIG_EXTERNAL_API_QUALIFIER)
+#define MLD_EXTERNAL_API
+#else
+#define MLD_EXTERNAL_API MLD_CONFIG_EXTERNAL_API_QUALIFIER
 #endif
 
-#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH)
-#include MLD_CONFIG_ARITH_BACKEND_FILE
+#if defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) || \
+    defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED)
+#define MLD_MULTILEVEL_BUILD
 #endif
 
 #define MLD_CONCAT_(x1, x2) x1##x2
 #define MLD_CONCAT(x1, x2) MLD_CONCAT_(x1, x2)
 
+#if defined(MLD_MULTILEVEL_BUILD)
+#define MLD_ADD_PARAM_SET(s) MLD_CONCAT(s, MLD_CONFIG_PARAMETER_SET)
+#else
+#define MLD_ADD_PARAM_SET(s) s
+#endif
+
+#define MLD_NAMESPACE_PREFIX MLD_CONCAT(MLD_CONFIG_NAMESPACE_PREFIX, _)
+#define MLD_NAMESPACE_PREFIX_K \
+  MLD_CONCAT(MLD_ADD_PARAM_SET(MLD_CONFIG_NAMESPACE_PREFIX), _)
+
+/* Functions are prefixed by MLD_CONFIG_NAMESPACE_PREFIX.
+ *
+ * Functions depending on the parameter set are additionally prefixed with
+ * 44/65/87. See config.h.
+ *
+ * Example: If MLD_CONFIG_NAMESPACE_PREFIX is PQCP_MLDSA_NATIVE_MLDSA, then
+ * MLD_NAMESPACE_K(keypair) becomes PQCP_MLDSA_NATIVE_MLDSA44_keypair/
+ * PQCP_MLDSA_NATIVE_MLDSA65_keypair/PQCP_MLDSA_NATIVE_MLDSA87_keypair.
+ */
+#define MLD_NAMESPACE(s) MLD_CONCAT(MLD_NAMESPACE_PREFIX, s)
+#define MLD_NAMESPACE_K(s) MLD_CONCAT(MLD_NAMESPACE_PREFIX_K, s)
+
 /* On Apple platforms, we need to emit leading underscore
  * in front of assembly symbols. We thus introducee a separate
  * namespace wrapper for ASM symbols. */
@@ -53,11 +84,47 @@
  * all source files are included, even those that are not needed.
  * Those files are appropriately guarded and will be empty when unneeded.
  * The following is to avoid compilers complaining about this. */
-#define MLD_EMPTY_CU(s) extern int MLD_NAMESPACE(empty_cu_##s);
+#define MLD_EMPTY_CU(s) extern int MLD_NAMESPACE_K(empty_cu_##s);
+
+/* MLD_CONFIG_NO_ASM takes precedence over MLD_USE_NATIVE_XXX */
+#if defined(MLD_CONFIG_NO_ASM)
+#undef MLD_CONFIG_USE_NATIVE_BACKEND_ARITH
+#undef MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202
+#endif
+
+#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) && \
+    !defined(MLD_CONFIG_ARITH_BACKEND_FILE)
+#error Bad configuration: MLD_CONFIG_USE_NATIVE_BACKEND_ARITH is set, but MLD_CONFIG_ARITH_BACKEND_FILE is not.
+#endif
+
+#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202) && \
+    !defined(MLD_CONFIG_FIPS202_BACKEND_FILE)
+#error Bad configuration: MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 is set, but MLD_CONFIG_FIPS202_BACKEND_FILE is not.
+#endif
+
+#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH)
+#include MLD_CONFIG_ARITH_BACKEND_FILE
+/* Include to enforce consistency of API and implementation,
+ * and conduct sanity checks on the backend.
+ *
+ * Keep this _after_ the inclusion of the backend; otherwise,
+ * the sanity checks won't have an effect. */
+#if defined(MLD_CHECK_APIS) && !defined(__ASSEMBLER__)
+#include "native/api.h"
+#endif
+#endif /* MLD_CONFIG_USE_NATIVE_BACKEND_ARITH */
 
 #if defined(MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202)
 #include MLD_CONFIG_FIPS202_BACKEND_FILE
+/* Include to enforce consistency of API and implementation,
+ * and conduct sanity checks on the backend.
+ *
+ * Keep this _after_ the inclusion of the backend; otherwise,
+ * the sanity checks won't have an effect. */
+#if defined(MLD_CHECK_APIS) && !defined(__ASSEMBLER__)
+#include "fips202/native/api.h"
 #endif
+#endif /* MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 */
 
 #if !defined(__ASSEMBLER__)
 #include <string.h>