From 33418930bc9389eaa116de06c49706753a20a162 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 18 Jun 2024 14:43:47 +0100 Subject: [PATCH 1/6] Add coeff_signed_to_unsigned() functions and its proof Signed-off-by: Rod Chapman --- cbmc/proofs/coeff_signed_to_unsigned/Makefile | 50 +++++++++++++++++ .../proofs/coeff_signed_to_unsigned/README.md | 14 +++++ .../coeff_signed_to_unsigned/cbmc-proof.txt | 3 ++ .../coeff_signed_to_unsigned_harness.c | 30 +++++++++++ .../coeff_signed_to_unsigned/desktop.mk | 27 ++++++++++ mlkem/poly.c | 53 +++++++++++++++---- mlkem/poly.h | 9 ++++ 7 files changed, 175 insertions(+), 11 deletions(-) create mode 100644 cbmc/proofs/coeff_signed_to_unsigned/Makefile create mode 100644 cbmc/proofs/coeff_signed_to_unsigned/README.md create mode 100644 cbmc/proofs/coeff_signed_to_unsigned/cbmc-proof.txt create mode 100644 cbmc/proofs/coeff_signed_to_unsigned/coeff_signed_to_unsigned_harness.c create mode 100644 cbmc/proofs/coeff_signed_to_unsigned/desktop.mk diff --git a/cbmc/proofs/coeff_signed_to_unsigned/Makefile b/cbmc/proofs/coeff_signed_to_unsigned/Makefile new file mode 100644 index 000000000..4f7f4e53e --- /dev/null +++ b/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 diff --git a/cbmc/proofs/coeff_signed_to_unsigned/README.md b/cbmc/proofs/coeff_signed_to_unsigned/README.md new file mode 100644 index 000000000..3ee617186 --- /dev/null +++ b/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. diff --git a/cbmc/proofs/coeff_signed_to_unsigned/cbmc-proof.txt b/cbmc/proofs/coeff_signed_to_unsigned/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/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. diff --git a/cbmc/proofs/coeff_signed_to_unsigned/coeff_signed_to_unsigned_harness.c b/cbmc/proofs/coeff_signed_to_unsigned/coeff_signed_to_unsigned_harness.c new file mode 100644 index 000000000..9989182e8 --- /dev/null +++ b/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 + +/** + * @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); +} diff --git a/cbmc/proofs/coeff_signed_to_unsigned/desktop.mk b/cbmc/proofs/coeff_signed_to_unsigned/desktop.mk new file mode 100644 index 000000000..61543e86d --- /dev/null +++ b/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 diff --git a/mlkem/poly.c b/mlkem/poly.c index 58e3a7ff9..596a0ab73 100644 --- a/mlkem/poly.c +++ b/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); diff --git a/mlkem/poly.h b/mlkem/poly.h index 48ff1efee..871576a88 100644 --- a/mlkem/poly.h +++ b/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); From 933fe53fe3c5460225af7e4e9ea6072ef2caca7b Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Tue, 2 Jul 2024 04:35:19 +0100 Subject: [PATCH 2/6] Rename coeff_signed_to_unsigned -> scalar_signed_to_unsigned_q_16 Also, uniformize file structure of proof subdirctory for scalar_signed_to_unsigned_q_16 with those of other functions. Signed-off-by: Hanno Becker --- .../coeff_signed_to_unsigned/desktop.mk | 27 ------------------- .../Makefile | 6 ++--- .../README.md | 4 +-- .../cbmc-proof.txt | 0 .../cbmc-viewer.json | 7 +++++ .../scalar_signed_to_unsigned_q_16_harness.c} | 6 ++--- mlkem/poly.c | 16 +++++------ mlkem/poly.h | 11 ++++---- 8 files changed, 29 insertions(+), 48 deletions(-) delete mode 100644 cbmc/proofs/coeff_signed_to_unsigned/desktop.mk rename cbmc/proofs/{coeff_signed_to_unsigned => scalar_signed_to_unsigned_q_16}/Makefile (90%) rename cbmc/proofs/{coeff_signed_to_unsigned => scalar_signed_to_unsigned_q_16}/README.md (77%) rename cbmc/proofs/{coeff_signed_to_unsigned => scalar_signed_to_unsigned_q_16}/cbmc-proof.txt (100%) create mode 100644 cbmc/proofs/scalar_signed_to_unsigned_q_16/cbmc-viewer.json rename cbmc/proofs/{coeff_signed_to_unsigned/coeff_signed_to_unsigned_harness.c => scalar_signed_to_unsigned_q_16/scalar_signed_to_unsigned_q_16_harness.c} (72%) diff --git a/cbmc/proofs/coeff_signed_to_unsigned/desktop.mk b/cbmc/proofs/coeff_signed_to_unsigned/desktop.mk deleted file mode 100644 index 61543e86d..000000000 --- a/cbmc/proofs/coeff_signed_to_unsigned/desktop.mk +++ /dev/null @@ -1,27 +0,0 @@ -# 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 diff --git a/cbmc/proofs/coeff_signed_to_unsigned/Makefile b/cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile similarity index 90% rename from cbmc/proofs/coeff_signed_to_unsigned/Makefile rename to cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile index 4f7f4e53e..89ed71bdd 100644 --- a/cbmc/proofs/coeff_signed_to_unsigned/Makefile +++ b/cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile @@ -3,11 +3,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = coeff_signed_to_unsigned_harness +HARNESS_FILE = scalar_signed_to_unsigned_q_16_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 +PROOF_UID = scalar_signed_to_unsigned_q_16 DEFINES += INCLUDES += @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=coeff_signed_to_unsigned +CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)scalar_signed_to_unsigned_q_16 USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/coeff_signed_to_unsigned/README.md b/cbmc/proofs/scalar_signed_to_unsigned_q_16/README.md similarity index 77% rename from cbmc/proofs/coeff_signed_to_unsigned/README.md rename to cbmc/proofs/scalar_signed_to_unsigned_q_16/README.md index 3ee617186..e12a8d51f 100644 --- a/cbmc/proofs/coeff_signed_to_unsigned/README.md +++ b/cbmc/proofs/scalar_signed_to_unsigned_q_16/README.md @@ -1,9 +1,9 @@ # SPDX-License-Identifier: Apache-2.0 -coeff_signed_to_unsigned proof +scalar_signed_to_unsigned_q_16 proof ============== -This directory contains a memory safety proof for coeff_signed_to_unsigned. +This directory contains a memory safety proof for scalar_signed_to_unsigned_q_16. To run the proof. ------------- diff --git a/cbmc/proofs/coeff_signed_to_unsigned/cbmc-proof.txt b/cbmc/proofs/scalar_signed_to_unsigned_q_16/cbmc-proof.txt similarity index 100% rename from cbmc/proofs/coeff_signed_to_unsigned/cbmc-proof.txt rename to cbmc/proofs/scalar_signed_to_unsigned_q_16/cbmc-proof.txt diff --git a/cbmc/proofs/scalar_signed_to_unsigned_q_16/cbmc-viewer.json b/cbmc/proofs/scalar_signed_to_unsigned_q_16/cbmc-viewer.json new file mode 100644 index 000000000..f56a80b36 --- /dev/null +++ b/cbmc/proofs/scalar_signed_to_unsigned_q_16/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "scalar_signed_to_unsigned_q_16", + "proof-root": "cbmc/proofs" +} diff --git a/cbmc/proofs/coeff_signed_to_unsigned/coeff_signed_to_unsigned_harness.c b/cbmc/proofs/scalar_signed_to_unsigned_q_16/scalar_signed_to_unsigned_q_16_harness.c similarity index 72% rename from cbmc/proofs/coeff_signed_to_unsigned/coeff_signed_to_unsigned_harness.c rename to cbmc/proofs/scalar_signed_to_unsigned_q_16/scalar_signed_to_unsigned_q_16_harness.c index 9989182e8..1f95bad2d 100644 --- a/cbmc/proofs/coeff_signed_to_unsigned/coeff_signed_to_unsigned_harness.c +++ b/cbmc/proofs/scalar_signed_to_unsigned_q_16/scalar_signed_to_unsigned_q_16_harness.c @@ -6,8 +6,8 @@ */ /** - * @file coeff_signed_to_unsigned.c - * @brief Implements the proof harness for coeff_signed_to_unsigned function. + * @file scalar_signed_to_unsigned_q_16.c + * @brief Implements the proof harness for scalar_signed_to_unsigned_q_16 function. */ /* @@ -26,5 +26,5 @@ void harness(void) int16_t u; /* Contracts for this function are in poly.h */ - uint16_t d = coeff_signed_to_unsigned(u); + uint16_t d = scalar_signed_to_unsigned_q_16(u); } diff --git a/mlkem/poly.c b/mlkem/poly.c index 596a0ab73..288a20f4e 100644 --- a/mlkem/poly.c +++ b/mlkem/poly.c @@ -88,7 +88,7 @@ uint32_t scalar_decompress_q_32(uint32_t u) } /************************************************************ - * Name: coeff_signed_to_unsigned + * Name: scalar_signed_to_unsigned_q_16 * * Description: converts signed polynomial coefficient * from signed (-3328 .. 3328) form to @@ -105,7 +105,7 @@ uint32_t scalar_decompress_q_32(uint32_t u) * * Arguments: c: signed coefficient to be converted ************************************************************/ -uint16_t coeff_signed_to_unsigned (int16_t c) +uint16_t scalar_signed_to_unsigned_q_16 (int16_t c) { int32_t r = (int32_t) c; @@ -113,8 +113,8 @@ uint16_t coeff_signed_to_unsigned (int16_t c) 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"); + __CPROVER_assert(r >= 0, "scalar_signed_to_unsigned_q_16 result lower bound"); + __CPROVER_assert(r < KYBER_Q, "scalar_signed_to_unsigned_q_16 result upper bound"); // and therefore cast to uint16_t is safe. return (uint16_t) r; @@ -145,7 +145,7 @@ void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a) { // map to positive standard representatives // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function - int32_t u = (int32_t) coeff_signed_to_unsigned(a->coeffs[8 * i + j]); + int32_t u = (int32_t) scalar_signed_to_unsigned_q_16(a->coeffs[8 * i + j]); // REF-CHANGE: Hoist scalar compression into separate function t[j] = scalar_compress_q_16(u); } @@ -163,7 +163,7 @@ void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a) { // map to positive standard representatives // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function - int32_t u = (int32_t) coeff_signed_to_unsigned(a->coeffs[8 * i + j]); + int32_t u = (int32_t) scalar_signed_to_unsigned_q_16(a->coeffs[8 * i + j]); // REF-CHANGE: Hoist scalar compression into separate function t[j] = scalar_compress_q_32(u); } @@ -266,8 +266,8 @@ void poly_tobytes(uint8_t r[KYBER_POLYBYTES], const poly *a) { // map to positive standard representatives // 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]); + t0 = scalar_signed_to_unsigned_q_16(a->coeffs[2 * i]); + t1 = scalar_signed_to_unsigned_q_16(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); diff --git a/mlkem/poly.h b/mlkem/poly.h index 871576a88..c7737e320 100644 --- a/mlkem/poly.h +++ b/mlkem/poly.h @@ -15,10 +15,11 @@ typedef struct int16_t coeffs[KYBER_N]; } poly; -#define scalar_compress_q_16 KYBER_NAMESPACE(scalar_compress_q_16) -#define scalar_decompress_q_16 KYBER_NAMESPACE(scalar_decompress_q_16) -#define scalar_compress_q_32 KYBER_NAMESPACE(scalar_compress_q_32) -#define scalar_decompress_q_32 KYBER_NAMESPACE(scalar_decompress_q_32) +#define scalar_compress_q_16 KYBER_NAMESPACE(scalar_compress_q_16) +#define scalar_decompress_q_16 KYBER_NAMESPACE(scalar_decompress_q_16) +#define scalar_compress_q_32 KYBER_NAMESPACE(scalar_compress_q_32) +#define scalar_decompress_q_32 KYBER_NAMESPACE(scalar_decompress_q_32) +#define scalar_signed_to_unsigned_q_16 KYBER_NAMESPACE(scalar_signed_to_unsigned_q_16) uint32_t scalar_compress_q_16 (int32_t u) /* INDENT-OFF */ @@ -46,7 +47,7 @@ __CPROVER_requires(0 <= u && u < 32) __CPROVER_ensures(__CPROVER_return_value < KYBER_Q); /* INDENT-ON */ -uint16_t coeff_signed_to_unsigned (int16_t c) +uint16_t scalar_signed_to_unsigned_q_16 (int16_t c) /* *INDENT-OFF* */ __CPROVER_requires(c > -KYBER_Q) // c >= -3328 __CPROVER_requires(c < KYBER_Q) // c <= 3328 From 2c1b0b295b5bf2f5b5a330a9527d4b184709606a Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Tue, 2 Jul 2024 04:57:10 +0100 Subject: [PATCH 3/6] Add warning & TODO regarding potential introduction of branch scalar_signed_to_unsigned_q_16() uses the expression `(r < 0)` for the extraction of the sign-bit, which is prone to compilers turning them into a branch. Signed-off-by: Hanno Becker --- mlkem/poly.c | 1 + 1 file changed, 1 insertion(+) diff --git a/mlkem/poly.c b/mlkem/poly.c index 288a20f4e..458a09432 100644 --- a/mlkem/poly.c +++ b/mlkem/poly.c @@ -110,6 +110,7 @@ uint16_t scalar_signed_to_unsigned_q_16 (int16_t c) int32_t r = (int32_t) c; // Add Q if r is negative + // TODO, WARNING: This needs to be protected from the compiler introducing a branch. int32_t factor = (r < 0); // 1 if r < 0; 0 if r >= 0 r = r + (factor * KYBER_Q); From 433c714f48b541bdbb0616eec55ce1b389c9dba9 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 2 Jul 2024 10:41:10 +0100 Subject: [PATCH 4/6] Re-write and prove scalar_signed_to_unsigned_q_16() using cmov_int16() Signed-off-by: Rod Chapman --- .../proofs/scalar_signed_to_unsigned_q_16/Makefile | 1 + mlkem/poly.c | 14 +++++--------- mlkem/verify.c | 7 +++++++ 3 files changed, 13 insertions(+), 9 deletions(-) diff --git a/cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile b/cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile index 89ed71bdd..4736e3231 100644 --- a/cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile +++ b/cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile @@ -17,6 +17,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)scalar_signed_to_unsigned_q_16 USE_FUNCTION_CONTRACTS= diff --git a/mlkem/poly.c b/mlkem/poly.c index 458a09432..d10594a3d 100644 --- a/mlkem/poly.c +++ b/mlkem/poly.c @@ -107,18 +107,14 @@ uint32_t scalar_decompress_q_32(uint32_t u) ************************************************************/ uint16_t scalar_signed_to_unsigned_q_16 (int16_t c) { - int32_t r = (int32_t) c; + // Add Q if c is negative, but in constant time + cmov_int16(&c, c + KYBER_Q, c < 0); - // Add Q if r is negative - // TODO, WARNING: This needs to be protected from the compiler introducing a branch. - int32_t factor = (r < 0); // 1 if r < 0; 0 if r >= 0 - r = r + (factor * KYBER_Q); - - __CPROVER_assert(r >= 0, "scalar_signed_to_unsigned_q_16 result lower bound"); - __CPROVER_assert(r < KYBER_Q, "scalar_signed_to_unsigned_q_16 result upper bound"); + __CPROVER_assert(c >= 0, "scalar_signed_to_unsigned_q_16 result lower bound"); + __CPROVER_assert(c < KYBER_Q, "scalar_signed_to_unsigned_q_16 result upper bound"); // and therefore cast to uint16_t is safe. - return (uint16_t) r; + return (uint16_t) c; } /************************************************* diff --git a/mlkem/verify.c b/mlkem/verify.c index a4259ea1a..553b8d4ec 100644 --- a/mlkem/verify.c +++ b/mlkem/verify.c @@ -64,6 +64,13 @@ void cmov(uint8_t *r, const uint8_t *x, size_t len, uint8_t b) **************************************************/ void cmov_int16(int16_t *r, int16_t v, uint16_t b) { + +// CBMC issues false alarms here for the implicit conversions between +// uint16_t and int, so disable "conversion-check" here for now. +// Revisit this when proof of this unit with contracts is attempted. +#pragma CPROVER check push +#pragma CPROVER check disable "conversion" b = -b; *r ^= b & ((*r) ^ v); +#pragma CPROVER check pop } From e313e84ce4a0d86e8b72537b8236cb40ceadb6db Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 2 Jul 2024 10:53:59 +0100 Subject: [PATCH 5/6] Add verify.c to proof dependencies for this function. Signed-off-by: Rod Chapman --- cbmc/proofs/poly_compress/Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/cbmc/proofs/poly_compress/Makefile b/cbmc/proofs/poly_compress/Makefile index 1d52ea6b2..bbe4c8e52 100644 --- a/cbmc/proofs/poly_compress/Makefile +++ b/cbmc/proofs/poly_compress/Makefile @@ -17,6 +17,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c # UNWINDSET += $(KYBER_NAMESPACE)poly_compress.0:9 # UNWINDSET += $(KYBER_NAMESPACE)poly_compress.1:33 From 50255daf2c13d8cbd9e135f07ef4713a5bed7841 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 2 Jul 2024 11:10:39 +0100 Subject: [PATCH 6/6] Increase CBMC_OBJECT_BITS for this function. Signed-off-by: Rod Chapman --- cbmc/proofs/poly_compress/Makefile | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/cbmc/proofs/poly_compress/Makefile b/cbmc/proofs/poly_compress/Makefile index bbe4c8e52..3a55e17a9 100644 --- a/cbmc/proofs/poly_compress/Makefile +++ b/cbmc/proofs/poly_compress/Makefile @@ -25,13 +25,15 @@ PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c FUNCTION_NAME = $(KYBER_NAMESPACE)poly_compress USE_FUNCTION_CONTRACTS = $(KYBER_NAMESPACE)scalar_compress_q_16 $(KYBER_NAMESPACE)scalar_compress_q_32 - # 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 = 10 + # 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).