From d2b60942d53baf008307be34a7fd7df456d06396 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Sat, 1 Jun 2024 21:29:32 +0100 Subject: [PATCH] CBMC: Add specs and proofs for further (de)compression routines Signed-off-by: Hanno Becker --- cbmc/proofs/poly_compress/Makefile | 47 +++++++ cbmc/proofs/poly_compress/README.md | 14 ++ cbmc/proofs/poly_compress/cbmc-proof.txt | 3 + cbmc/proofs/poly_compress/cbmc-viewer.json | 7 + .../poly_compress/poly_compress_harness.c | 34 +++++ cbmc/proofs/poly_decompress/Makefile | 2 + cbmc/proofs/scalar_compress_q_16/Makefile | 41 ++++++ cbmc/proofs/scalar_compress_q_16/README.md | 14 ++ .../scalar_compress_q_16/cbmc-proof.txt | 3 + .../scalar_compress_q_16/cbmc-viewer.json | 7 + .../scalar_compress_q_16_harness.c | 32 +++++ cbmc/proofs/scalar_compress_q_32/Makefile | 41 ++++++ cbmc/proofs/scalar_compress_q_32/README.md | 14 ++ .../scalar_compress_q_32/cbmc-proof.txt | 3 + .../scalar_compress_q_32/cbmc-viewer.json | 7 + .../scalar_compress_q_32_harness.c | 32 +++++ cbmc/proofs/scalar_decompress_q_16/Makefile | 38 ++++++ cbmc/proofs/scalar_decompress_q_16/README.md | 14 ++ .../scalar_decompress_q_16/cbmc-proof.txt | 3 + .../scalar_decompress_q_16/cbmc-viewer.json | 7 + .../scalar_decompress_q_16_harness.c | 33 +++++ cbmc/proofs/scalar_decompress_q_32/Makefile | 38 ++++++ cbmc/proofs/scalar_decompress_q_32/README.md | 14 ++ .../scalar_decompress_q_32/cbmc-proof.txt | 3 + .../scalar_decompress_q_32/cbmc-viewer.json | 7 + .../scalar_decompress_q_32_harness.c | 33 +++++ mlkem/poly.c | 124 ++++++++++++++---- mlkem/poly.h | 10 ++ 28 files changed, 601 insertions(+), 24 deletions(-) create mode 100644 cbmc/proofs/poly_compress/Makefile create mode 100644 cbmc/proofs/poly_compress/README.md create mode 100644 cbmc/proofs/poly_compress/cbmc-proof.txt create mode 100644 cbmc/proofs/poly_compress/cbmc-viewer.json create mode 100644 cbmc/proofs/poly_compress/poly_compress_harness.c create mode 100644 cbmc/proofs/scalar_compress_q_16/Makefile create mode 100644 cbmc/proofs/scalar_compress_q_16/README.md create mode 100644 cbmc/proofs/scalar_compress_q_16/cbmc-proof.txt create mode 100644 cbmc/proofs/scalar_compress_q_16/cbmc-viewer.json create mode 100644 cbmc/proofs/scalar_compress_q_16/scalar_compress_q_16_harness.c create mode 100644 cbmc/proofs/scalar_compress_q_32/Makefile create mode 100644 cbmc/proofs/scalar_compress_q_32/README.md create mode 100644 cbmc/proofs/scalar_compress_q_32/cbmc-proof.txt create mode 100644 cbmc/proofs/scalar_compress_q_32/cbmc-viewer.json create mode 100644 cbmc/proofs/scalar_compress_q_32/scalar_compress_q_32_harness.c create mode 100644 cbmc/proofs/scalar_decompress_q_16/Makefile create mode 100644 cbmc/proofs/scalar_decompress_q_16/README.md create mode 100644 cbmc/proofs/scalar_decompress_q_16/cbmc-proof.txt create mode 100644 cbmc/proofs/scalar_decompress_q_16/cbmc-viewer.json create mode 100644 cbmc/proofs/scalar_decompress_q_16/scalar_decompress_q_16_harness.c create mode 100644 cbmc/proofs/scalar_decompress_q_32/Makefile create mode 100644 cbmc/proofs/scalar_decompress_q_32/README.md create mode 100644 cbmc/proofs/scalar_decompress_q_32/cbmc-proof.txt create mode 100644 cbmc/proofs/scalar_decompress_q_32/cbmc-viewer.json create mode 100644 cbmc/proofs/scalar_decompress_q_32/scalar_decompress_q_32_harness.c diff --git a/cbmc/proofs/poly_compress/Makefile b/cbmc/proofs/poly_compress/Makefile new file mode 100644 index 000000000..1d52ea6b2 --- /dev/null +++ b/cbmc/proofs/poly_compress/Makefile @@ -0,0 +1,47 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_compress_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 = poly_compress + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c + +# UNWINDSET += $(KYBER_NAMESPACE)poly_compress.0:9 +# UNWINDSET += $(KYBER_NAMESPACE)poly_compress.1:33 + +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 + +# 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/poly_compress/README.md b/cbmc/proofs/poly_compress/README.md new file mode 100644 index 000000000..69264ad55 --- /dev/null +++ b/cbmc/proofs/poly_compress/README.md @@ -0,0 +1,14 @@ +# SPDX-License-Identifier: Apache-2.0 + +poly_compress proof +============== + +This directory contains a memory safety proof for poly_compress. + +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/poly_compress/cbmc-proof.txt b/cbmc/proofs/poly_compress/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/poly_compress/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/poly_compress/cbmc-viewer.json b/cbmc/proofs/poly_compress/cbmc-viewer.json new file mode 100644 index 000000000..6d4fed048 --- /dev/null +++ b/cbmc/proofs/poly_compress/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "poly_compress", + "proof-root": "cbmc/proofs" +} diff --git a/cbmc/proofs/poly_compress/poly_compress_harness.c b/cbmc/proofs/poly_compress/poly_compress_harness.c new file mode 100644 index 000000000..53c48ea5e --- /dev/null +++ b/cbmc/proofs/poly_compress/poly_compress_harness.c @@ -0,0 +1,34 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +/* + * Insert copyright notice + */ + +/** + * @file poly_compress_harness.c + * @brief Implements the proof harness for poly_compress function. + */ +#include "poly.h" + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) { + poly r; + uint8_t a[KYBER_POLYCOMPRESSEDBYTES]; + + // *INDENT-OFF * + __CPROVER_assume(__CPROVER_forall { + unsigned i; (i < KYBER_N) ==> ( -KYBER_Q <= r.coeffs[i] && r.coeffs[i] < KYBER_Q ) + }); + // *INDENT-ON* + poly_compress(a, &r); +} diff --git a/cbmc/proofs/poly_decompress/Makefile b/cbmc/proofs/poly_decompress/Makefile index 8b9143bb6..5b3c2310c 100644 --- a/cbmc/proofs/poly_decompress/Makefile +++ b/cbmc/proofs/poly_decompress/Makefile @@ -28,6 +28,8 @@ endif FUNCTION_NAME = $(KYBER_NAMESPACE)poly_decompress +USE_FUNCTION_CONTRACTS = $(KYBER_NAMESPACE)scalar_decompress_q_16 + # TODO: I would like to comment this out to have CBMC validate the # function contract as annotated in the source, rather than being forced # to replicate it in the harness. But somehow this doesn't work...? diff --git a/cbmc/proofs/scalar_compress_q_16/Makefile b/cbmc/proofs/scalar_compress_q_16/Makefile new file mode 100644 index 000000000..dfed882fb --- /dev/null +++ b/cbmc/proofs/scalar_compress_q_16/Makefile @@ -0,0 +1,41 @@ +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY = harness +HARNESS_FILE = scalar_compress_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_compress_q_16 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c + +# Disable unsigned overflow check for Barret reduction +CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK = + +# 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_compress_q_16/README.md b/cbmc/proofs/scalar_compress_q_16/README.md new file mode 100644 index 000000000..754d2fc14 --- /dev/null +++ b/cbmc/proofs/scalar_compress_q_16/README.md @@ -0,0 +1,14 @@ +# SPDX-License-Identifier: Apache-2.0 + +scalar_compress_q_16 proof +============== + +This directory contains a memory safety proof for scalar_compress_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_compress_q_16/cbmc-proof.txt b/cbmc/proofs/scalar_compress_q_16/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/scalar_compress_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_compress_q_16/cbmc-viewer.json b/cbmc/proofs/scalar_compress_q_16/cbmc-viewer.json new file mode 100644 index 000000000..cef74efec --- /dev/null +++ b/cbmc/proofs/scalar_compress_q_16/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "scalar_compress_q_16", + "proof-root": "cbmc/proofs" +} diff --git a/cbmc/proofs/scalar_compress_q_16/scalar_compress_q_16_harness.c b/cbmc/proofs/scalar_compress_q_16/scalar_compress_q_16_harness.c new file mode 100644 index 000000000..30e0b2608 --- /dev/null +++ b/cbmc/proofs/scalar_compress_q_16/scalar_compress_q_16_harness.c @@ -0,0 +1,32 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +/* + * Insert copyright notice + */ + +/** + * @file scalar_compress_q_16_harness.c + * @brief Implements the proof harness for scalar_compress_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) { + int32_t u; + + __CPROVER_assume(0 <= u && u < KYBER_Q); + uint32_t d = scalar_compress_q_16(u); + __CPROVER_assert(d < 16, "compression bound failed"); + __CPROVER_assert(d == (((uint32_t) u * 16 + KYBER_Q / 2) / KYBER_Q) % 16, + "compression expression failed"); +} diff --git a/cbmc/proofs/scalar_compress_q_32/Makefile b/cbmc/proofs/scalar_compress_q_32/Makefile new file mode 100644 index 000000000..eae543a44 --- /dev/null +++ b/cbmc/proofs/scalar_compress_q_32/Makefile @@ -0,0 +1,41 @@ +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY = harness +HARNESS_FILE = scalar_compress_q_32_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_compress_q_32 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c + +# Disable unsigned overflow check for Barret reduction +CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK = + +# 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_compress_q_32/README.md b/cbmc/proofs/scalar_compress_q_32/README.md new file mode 100644 index 000000000..90bd43cd4 --- /dev/null +++ b/cbmc/proofs/scalar_compress_q_32/README.md @@ -0,0 +1,14 @@ +# SPDX-License-Identifier: Apache-2.0 + +scalar_compress_q_32 proof +============== + +This directory contains a memory safety proof for scalar_compress_q_32. + +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_compress_q_32/cbmc-proof.txt b/cbmc/proofs/scalar_compress_q_32/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/scalar_compress_q_32/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_compress_q_32/cbmc-viewer.json b/cbmc/proofs/scalar_compress_q_32/cbmc-viewer.json new file mode 100644 index 000000000..5ca96c07f --- /dev/null +++ b/cbmc/proofs/scalar_compress_q_32/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "scalar_compress_q_32", + "proof-root": "cbmc/proofs" +} diff --git a/cbmc/proofs/scalar_compress_q_32/scalar_compress_q_32_harness.c b/cbmc/proofs/scalar_compress_q_32/scalar_compress_q_32_harness.c new file mode 100644 index 000000000..bfd5ff20b --- /dev/null +++ b/cbmc/proofs/scalar_compress_q_32/scalar_compress_q_32_harness.c @@ -0,0 +1,32 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +/* + * Insert copyright notice + */ + +/** + * @file scalar_compress_q_32_harness.c + * @brief Implements the proof harness for scalar_compress_q_32 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) { + int32_t u; + + __CPROVER_assume(0 <= u && u < KYBER_Q); + uint32_t d = scalar_compress_q_32(u); + __CPROVER_assert(d < 32, "compression bound failed"); + __CPROVER_assert(d == (((uint32_t) u * 32 + KYBER_Q / 2) / KYBER_Q) % 32, + "compression expression failed"); +} diff --git a/cbmc/proofs/scalar_decompress_q_16/Makefile b/cbmc/proofs/scalar_decompress_q_16/Makefile new file mode 100644 index 000000000..240f534ba --- /dev/null +++ b/cbmc/proofs/scalar_decompress_q_16/Makefile @@ -0,0 +1,38 @@ +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY = harness +HARNESS_FILE = scalar_decompress_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_decompress_q_16 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c + +# 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_decompress_q_16/README.md b/cbmc/proofs/scalar_decompress_q_16/README.md new file mode 100644 index 000000000..6bf2b7789 --- /dev/null +++ b/cbmc/proofs/scalar_decompress_q_16/README.md @@ -0,0 +1,14 @@ +# SPDX-License-Identifier: Apache-2.0 + +scalar_decompress_q_16 proof +============== + +This directory contains a memory safety proof for scalar_decompress_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_decompress_q_16/cbmc-proof.txt b/cbmc/proofs/scalar_decompress_q_16/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/scalar_decompress_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_decompress_q_16/cbmc-viewer.json b/cbmc/proofs/scalar_decompress_q_16/cbmc-viewer.json new file mode 100644 index 000000000..6d9ce59ea --- /dev/null +++ b/cbmc/proofs/scalar_decompress_q_16/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "scalar_decompress_q_16", + "proof-root": "cbmc/proofs" +} diff --git a/cbmc/proofs/scalar_decompress_q_16/scalar_decompress_q_16_harness.c b/cbmc/proofs/scalar_decompress_q_16/scalar_decompress_q_16_harness.c new file mode 100644 index 000000000..73f1727b9 --- /dev/null +++ b/cbmc/proofs/scalar_decompress_q_16/scalar_decompress_q_16_harness.c @@ -0,0 +1,33 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +/* + * Insert copyright notice + */ + +/** + * @file scalar_decompress_q_16_harness.c + * @brief Implements the proof harness for scalar_decompress_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) { + // Check that decompression followed by compression is the identity + uint32_t c0, c1, d; + + __CPROVER_assume(c0 < 16); + d = scalar_decompress_q_16(c0); + __CPROVER_assert(d < KYBER_Q, "scalar_decompress_q_16 bound"); + c1 = scalar_compress_q_16(d); + __CPROVER_assert(c0 == c1, "scalar_compress_q_16 o scalar_decompress_q_16 != id"); +} diff --git a/cbmc/proofs/scalar_decompress_q_32/Makefile b/cbmc/proofs/scalar_decompress_q_32/Makefile new file mode 100644 index 000000000..e8790dc0c --- /dev/null +++ b/cbmc/proofs/scalar_decompress_q_32/Makefile @@ -0,0 +1,38 @@ +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY = harness +HARNESS_FILE = scalar_decompress_q_32_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_decompress_q_32 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c + +# 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_decompress_q_32/README.md b/cbmc/proofs/scalar_decompress_q_32/README.md new file mode 100644 index 000000000..97ca4c139 --- /dev/null +++ b/cbmc/proofs/scalar_decompress_q_32/README.md @@ -0,0 +1,14 @@ +# SPDX-License-Identifier: Apache-2.0 + +scalar_decompress_q_32 proof +============== + +This directory contains a memory safety proof for scalar_decompress_q_32. + +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_decompress_q_32/cbmc-proof.txt b/cbmc/proofs/scalar_decompress_q_32/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/scalar_decompress_q_32/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_decompress_q_32/cbmc-viewer.json b/cbmc/proofs/scalar_decompress_q_32/cbmc-viewer.json new file mode 100644 index 000000000..58f184aa7 --- /dev/null +++ b/cbmc/proofs/scalar_decompress_q_32/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "scalar_decompress_q_32", + "proof-root": "cbmc/proofs" +} diff --git a/cbmc/proofs/scalar_decompress_q_32/scalar_decompress_q_32_harness.c b/cbmc/proofs/scalar_decompress_q_32/scalar_decompress_q_32_harness.c new file mode 100644 index 000000000..4a5715fcd --- /dev/null +++ b/cbmc/proofs/scalar_decompress_q_32/scalar_decompress_q_32_harness.c @@ -0,0 +1,33 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +/* + * Insert copyright notice + */ + +/** + * @file scalar_decompress_q_32_harness.c + * @brief Implements the proof harness for scalar_decompress_q_32 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) { + // Check that decompression followed by compression is the identity + uint32_t c0, c1, d; + + __CPROVER_assume(c0 < 32); + d = scalar_decompress_q_32(c0); + __CPROVER_assert(d < KYBER_Q, "scalar_decompress_q_32 bound"); + c1 = scalar_compress_q_32(d); + __CPROVER_assert(c0 == c1, "scalar_compress_q_32 o scalar_decompress_q_32 != id"); +} diff --git a/mlkem/poly.c b/mlkem/poly.c index f436de908..d520e1d6a 100644 --- a/mlkem/poly.c +++ b/mlkem/poly.c @@ -8,6 +8,88 @@ #include "cbd.h" #include "symmetric.h" +/************************************************************ + * Name: scalar_compress_q_16 + * + * Description: Computes round(u * 16 / q) + * + * Arguments: - u: Unsigned canonical modulus modulo q + * to be compressed. + ************************************************************/ +uint32_t scalar_compress_q_16(int32_t u) +/* INDENT-OFF */ +__CPROVER_requires(0 <= u && u < KYBER_Q) +__CPROVER_ensures(__CPROVER_return_value < 16) +//__CPROVER_ensures(__CPROVER_return_value == (((uint32_t) u * 16 + KYBER_Q / 2) / KYBER_Q) % 16) +/* INDENT-ON */ +{ + uint32_t d0 = (uint32_t) u; + d0 <<= 4; + d0 += 1665; + d0 *= 80635; + d0 >>= 28; + d0 &= 0xF; + return d0; +} + +/************************************************************ + * Name: scalar_decompress_q_16 + * + * Description: Computes round(u * q / 16) + * + * Arguments: - u: Unsigned canonical modulus modulo 16 + * to be decompressed. + ************************************************************/ +uint32_t scalar_decompress_q_16(uint32_t u) +/* INDENT-OFF */ +__CPROVER_requires(0 <= u && u < 16) +__CPROVER_ensures(__CPROVER_return_value < KYBER_Q) +/* INDENT-ON */ +{ + return ((u * KYBER_Q) + 8) / 16; +} + +/************************************************************ + * Name: scalar_compress_q_32 + * + * Description: Computes round(u * 32 / q) + * + * Arguments: - u: Unsigned canonical modulus modulo q + * to be compressed. + ************************************************************/ +uint32_t scalar_compress_q_32(int32_t u) +/* INDENT-OFF */ +__CPROVER_requires(0 <= u && u < KYBER_Q) +__CPROVER_ensures(__CPROVER_return_value < 32) +//__CPROVER_ensures(__CPROVER_return_value == (((uint32_t) u * 32 + KYBER_Q / 2) / KYBER_Q) % 32) +/* INDENT-ON */ +{ + uint32_t d0 = (uint32_t) u; + d0 <<= 5; + d0 += 1664; + d0 *= 40318; + d0 >>= 27; + d0 &= 0x1f; + return d0; +} + +/************************************************************ + * Name: scalar_decompress_q_32 + * + * Description: Computes round(u * q / 32) + * + * Arguments: - u: Unsigned canonical modulus modulo 32 + * to be decompressed. + ************************************************************/ +uint32_t scalar_decompress_q_32(uint32_t u) +/* INDENT-OFF */ +__CPROVER_requires(0 <= u && u < 32) +__CPROVER_ensures(__CPROVER_return_value < KYBER_Q) +/* INDENT-ON */ +{ + return ((u * KYBER_Q) + 16) / 32; +} + /************************************************* * Name: poly_compress * @@ -24,18 +106,13 @@ void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a) { uint8_t t[8]; #if (KYBER_POLYCOMPRESSEDBYTES == 128) - for (i = 0; i < KYBER_N / 8; i++) { for (j = 0; j < 8; j++) { // map to positive standard representatives u = a->coeffs[8 * i + j]; u += (u >> 15) & KYBER_Q; - /* t[j] = ((((uint16_t)u << 4) + KYBER_Q/2)/KYBER_Q) & 15; */ - d0 = u << 4; - d0 += 1665; - d0 *= 80635; - d0 >>= 28; - t[j] = d0 & 0xf; + // REF-CHANGE: Hoist scalar compression into separate function + t[j] = scalar_compress_q_16(u); } r[0] = t[0] | (t[1] << 4); @@ -50,19 +127,17 @@ void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a) { // map to positive standard representatives u = a->coeffs[8 * i + j]; u += (u >> 15) & KYBER_Q; - /* t[j] = ((((uint32_t)u << 5) + KYBER_Q/2)/KYBER_Q) & 31; */ - d0 = u << 5; - d0 += 1664; - d0 *= 40318; - d0 >>= 27; - t[j] = d0 & 0x1f; + // REF-CHANGE: Hoist scalar compression into separate function + t[j] = scalar_compress_q_32(u); } - r[0] = (t[0] >> 0) | (t[1] << 5); - r[1] = (t[1] >> 3) | (t[2] << 2) | (t[3] << 7); - r[2] = (t[3] >> 1) | (t[4] << 4); - r[3] = (t[4] >> 4) | (t[5] << 1) | (t[6] << 6); - r[4] = (t[6] >> 2) | (t[7] << 3); + // REF-CHANGE: Explicitly truncate to avoid warning about + // implicit truncation in CBMC. + r[0] = 0xFF & ((t[0] >> 0) | (t[1] << 5)); + r[1] = 0xFF & ((t[1] >> 3) | (t[2] << 2) | (t[3] << 7)); + r[2] = 0xFF & ((t[3] >> 1) | (t[4] << 4)); + r[3] = 0xFF & ((t[4] >> 4) | (t[5] << 1) | (t[6] << 6)); + r[4] = 0xFF & ((t[6] >> 2) | (t[7] << 3)); r += 5; } #else @@ -90,10 +165,10 @@ void poly_decompress(poly *r, const uint8_t a[KYBER_POLYCOMPRESSEDBYTES]) __CPROVER_requires(__CPROVER_is_fresh(r, sizeof(*r))) __CPROVER_requires(__CPROVER_is_fresh(a, sizeof(KYBER_POLYCOMPRESSEDBYTES))) __CPROVER_ensures( - /* Output coefficients are unsigned canonical */ - __CPROVER_forall { - unsigned i; (i < KYBER_N) ==> ( 0 <= r->coeffs[i] && r->coeffs[i] < KYBER_Q ) - }) +/* Output coefficients are unsigned canonical */ +__CPROVER_forall { + unsigned i; (i < KYBER_N) ==> ( 0 <= r->coeffs[i] && r->coeffs[i] < KYBER_Q ) +}) // *INDENT-ON* /* --- End of CBMC contract --- */ { @@ -101,8 +176,9 @@ __CPROVER_ensures( #if (KYBER_POLYCOMPRESSEDBYTES == 128) for (i = 0; i < KYBER_N / 2; i++) { - r->coeffs[2 * i + 0] = (((uint16_t)(a[0] & 15) * KYBER_Q) + 8) >> 4; - r->coeffs[2 * i + 1] = (((uint16_t)(a[0] >> 4) * KYBER_Q) + 8) >> 4; + // REF-CHANGE: Hoist scalar decompression into separate function + r->coeffs[2 * i + 0] = scalar_decompress_q_16((a[0] >> 0) & 0xF); + r->coeffs[2 * i + 1] = scalar_decompress_q_16((a[0] >> 4) & 0xF); a += 1; } #elif (KYBER_POLYCOMPRESSEDBYTES == 160) diff --git a/mlkem/poly.h b/mlkem/poly.h index 43ec475b8..fb4731450 100644 --- a/mlkem/poly.h +++ b/mlkem/poly.h @@ -13,6 +13,16 @@ 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) + +uint32_t scalar_compress_q_16 (int32_t); +uint32_t scalar_decompress_q_16 (uint32_t); +uint32_t scalar_compress_q_32 (int32_t); +uint32_t scalar_decompress_q_32 (uint32_t); + #define poly_compress KYBER_NAMESPACE(poly_compress) void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a); #define poly_decompress KYBER_NAMESPACE(poly_decompress)