Add coeff_signed_to_unsigned() functions and its proof

Signed-off-by: Rod Chapman <[email protected]>

cbmc/proofs/coeff_signed_to_unsigned/Makefile

@@ -0,0 +1,50 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = coeff_signed_to_unsigned_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 = coeff_signed_to_unsigned
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+CHECK_FUNCTION_CONTRACTS=coeff_signed_to_unsigned
+USE_FUNCTION_CONTRACTS=
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+CBMCFLAGS=--smt2
+
+# Uncomment this to see what commands litani is running...
+#VERBOSE=on
+
+# 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
+
+# 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
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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

cbmc/proofs/coeff_signed_to_unsigned/README.md

@@ -0,0 +1,14 @@
+# SPDX-License-Identifier: Apache-2.0
+
+coeff_signed_to_unsigned proof
+==============
+
+This directory contains a memory safety proof for coeff_signed_to_unsigned.
+
+To run the proof.
+-------------
+* Follow these [tool installation instructions](https://github.com/awslabs/aws-templates-for-cbmc-proofs/wiki/Installation) to install cbmc and cbmc-viewer.
+* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
+  to your path.
+* Run `make`.
+* Open `report/html/index.html` in a web browser.

cbmc/proofs/coeff_signed_to_unsigned/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

cbmc/proofs/coeff_signed_to_unsigned/coeff_signed_to_unsigned_harness.c

@@ -0,0 +1,30 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+/*
+ * Insert copyright notice
+ */
+
+/**
+ * @file coeff_signed_to_unsigned.c
+ * @brief Implements the proof harness for coeff_signed_to_unsigned function.
+ */
+
+/*
+ * Insert project header files that
+ *   - include the declaration of the function
+ *   - include the types needed to declare function arguments
+ */
+#include <poly.h>
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+    int16_t u;
+
+    /* Contracts for this function are in poly.h */
+    uint16_t d = coeff_signed_to_unsigned(u);
+}

cbmc/proofs/coeff_signed_to_unsigned/desktop.mk

@@ -0,0 +1,27 @@
+# SPDX-License-Identifier: Apache-2.0
+
+FILE = ../../../mlkem/poly
+HARNESS_FILE = coeff_signed_to_unsigned_harness
+TARGET ?= coeff_signed_to_unsigned
+
+CHECKS=--bounds-check --pointer-check \
+       --memory-cleanup-check --div-by-zero-check --signed-overflow-check \
+       --unsigned-overflow-check --pointer-overflow-check --conversion-check \
+       --undefined-shift-check --enum-range-check --pointer-primitive-check
+
+all: clean $(TARGET)
+
+coeff_signed_to_unsigned: $(FILE)_contracts.goto results_smt
+
+
+results_smt: $(FILE)_contracts.goto
+	cbmc --verbosity 6 --object-bits 8 $(CHECKS) --smt2 $<
+
+$(FILE)_contracts.goto: $(FILE).goto
+	goto-instrument --dfcc harness --apply-loop-contracts --enforce-contract $(TARGET) $< $@
+
+$(FILE).goto: $(FILE).c $(HARNESS_FILE).c
+	goto-cc --function harness -DCBMC -I../../../fips202 -I../../../mlkem -o $@ $^
+
+clean:
+	rm -f *.goto

mlkem/poly.c

@@ -87,6 +87,39 @@ uint32_t scalar_decompress_q_32(uint32_t u)
     return ((u * KYBER_Q) + 16) / 32;
 }
 
+/************************************************************
+ * Name: coeff_signed_to_unsigned
+ *
+ * Description: converts signed polynomial coefficient
+ *              from signed (-3328 .. 3328) form to
+ *              unsigned form (0 .. 3328).
+ *
+ * Note: Cryptographic constant time implementation
+ *
+ * Examples:       0 -> 0
+ *                 1 -> 1
+ *              3328 -> 3328
+ *                -1 -> 3328
+ *                -2 -> 3327
+ *             -3328 -> 1
+ *
+ * Arguments: c: signed coefficient to be converted
+ ************************************************************/
+uint16_t coeff_signed_to_unsigned (int16_t c)
+{
+    int32_t r = (int32_t) c;
+
+    // Add Q if r is negative
+    int32_t factor = (r < 0); // 1 if r < 0; 0 if r >= 0
+    r = r + (factor * KYBER_Q);
+
+    __CPROVER_assert(r >= 0, "coeff_signed_to_unsigned result lower bound");
+    __CPROVER_assert(r < KYBER_Q, "coeff_signed_to_unsigned result upper bound");
+
+    // and therefore cast to uint16_t is safe.
+    return (uint16_t) r;
+}
+
 /*************************************************
 * Name:        poly_compress
 *
@@ -99,21 +132,20 @@ uint32_t scalar_decompress_q_32(uint32_t u)
 void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a)
 {
     unsigned int i, j;
-    int32_t u;
     uint8_t t[8];
 
     #if (KYBER_POLYCOMPRESSEDBYTES == 128)
     for (i = 0; i < KYBER_N / 8; i++)
-        __CPROVER_assigns(i, j, u, t, r)
+        __CPROVER_assigns(i, j, t, r)
         /* Stronger loop invariant here TBD */
     {
         for (j = 0; j < 8; j++)
-            __CPROVER_assigns(j, u, t)
+            __CPROVER_assigns(j, t)
             /* Stronger loop invariant here TBD */
         {
             // map to positive standard representatives
-            u  = a->coeffs[8 * i + j];
-            u += (u >> 15) & KYBER_Q;
+            // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function
+            int32_t u = (int32_t) coeff_signed_to_unsigned(a->coeffs[8 * i + j]);
             // REF-CHANGE: Hoist scalar compression into separate function
             t[j] = scalar_compress_q_16(u);
         }
@@ -130,8 +162,8 @@ void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a)
         for (j = 0; j < 8; j++)
         {
             // map to positive standard representatives
-            u  = a->coeffs[8 * i + j];
-            u += (u >> 15) & KYBER_Q;
+            // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function
+            int32_t u = (int32_t) coeff_signed_to_unsigned(a->coeffs[8 * i + j]);
             // REF-CHANGE: Hoist scalar compression into separate function
             t[j] = scalar_compress_q_32(u);
         }
@@ -233,10 +265,9 @@ void poly_tobytes(uint8_t r[KYBER_POLYBYTES], const poly *a)
     for (i = 0; i < KYBER_N / 2; i++)
     {
         // map to positive standard representatives
-        t0  = a->coeffs[2 * i];
-        t0 += ((int16_t)t0 >> 15) & KYBER_Q;
-        t1 = a->coeffs[2 * i + 1];
-        t1 += ((int16_t)t1 >> 15) & KYBER_Q;
+        // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function
+        t0 = coeff_signed_to_unsigned(a->coeffs[2 * i]);
+        t1 = coeff_signed_to_unsigned(a->coeffs[2 * i + 1]);
         r[3 * i + 0] = (t0 >> 0);
         r[3 * i + 1] = (t0 >> 8) | (t1 << 4);
         r[3 * i + 2] = (t1 >> 4);

mlkem/poly.h

@@ -46,6 +46,15 @@ __CPROVER_requires(0 <= u && u < 32)
 __CPROVER_ensures(__CPROVER_return_value < KYBER_Q);
 /* INDENT-ON */
 
+uint16_t coeff_signed_to_unsigned (int16_t c)
+/* *INDENT-OFF* */
+__CPROVER_requires(c > -KYBER_Q) // c >= -3328
+__CPROVER_requires(c < KYBER_Q)  // c <= 3328
+__CPROVER_ensures(__CPROVER_return_value >= 0)
+__CPROVER_ensures(__CPROVER_return_value < KYBER_Q)
+__CPROVER_ensures(__CPROVER_return_value == (int32_t) c + (((int32_t) c < 0) * KYBER_Q));
+/* *INDENT-ON* */
+
 #define poly_compress KYBER_NAMESPACE(poly_compress)
 void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a);