diff --git a/cbmc/proofs/poly_compress/Makefile b/cbmc/proofs/poly_compress/Makefile index 1d52ea6b2..3a55e17a9 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 @@ -24,13 +25,15 @@ PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.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). diff --git a/cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile b/cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile new file mode 100644 index 000000000..4736e3231 --- /dev/null +++ b/cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile @@ -0,0 +1,51 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = 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 = scalar_signed_to_unsigned_q_16 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +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= +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/scalar_signed_to_unsigned_q_16/README.md b/cbmc/proofs/scalar_signed_to_unsigned_q_16/README.md new file mode 100644 index 000000000..e12a8d51f --- /dev/null +++ b/cbmc/proofs/scalar_signed_to_unsigned_q_16/README.md @@ -0,0 +1,14 @@ +# SPDX-License-Identifier: Apache-2.0 + +scalar_signed_to_unsigned_q_16 proof +============== + +This directory contains a memory safety proof for scalar_signed_to_unsigned_q_16. + +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/scalar_signed_to_unsigned_q_16/cbmc-proof.txt b/cbmc/proofs/scalar_signed_to_unsigned_q_16/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/scalar_signed_to_unsigned_q_16/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/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/scalar_signed_to_unsigned_q_16/scalar_signed_to_unsigned_q_16_harness.c b/cbmc/proofs/scalar_signed_to_unsigned_q_16/scalar_signed_to_unsigned_q_16_harness.c new file mode 100644 index 000000000..1f95bad2d --- /dev/null +++ b/cbmc/proofs/scalar_signed_to_unsigned_q_16/scalar_signed_to_unsigned_q_16_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 scalar_signed_to_unsigned_q_16.c + * @brief Implements the proof harness for scalar_signed_to_unsigned_q_16 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 = scalar_signed_to_unsigned_q_16(u); +} diff --git a/mlkem/poly.c b/mlkem/poly.c index 58e3a7ff9..d10594a3d 100644 --- a/mlkem/poly.c +++ b/mlkem/poly.c @@ -87,6 +87,36 @@ uint32_t scalar_decompress_q_32(uint32_t u) return ((u * KYBER_Q) + 16) / 32; } +/************************************************************ + * Name: scalar_signed_to_unsigned_q_16 + * + * 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 scalar_signed_to_unsigned_q_16 (int16_t c) +{ + // Add Q if c is negative, but in constant time + cmov_int16(&c, c + KYBER_Q, c < 0); + + __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) c; +} + /************************************************* * Name: poly_compress * @@ -99,21 +129,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) 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); } @@ -130,8 +159,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) 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); } @@ -233,10 +262,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 = 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 48ff1efee..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,6 +47,15 @@ __CPROVER_requires(0 <= u && u < 32) __CPROVER_ensures(__CPROVER_return_value < KYBER_Q); /* INDENT-ON */ +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 +__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); 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 }